α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
⊢ ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
f : Fin n → α → β
hf : ∀ (i : Fin n), Memℒp (f i) p
⊢ UnifIntegrable f p μ
revert f
case zero
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
⊢ ∀ {f : Fin Nat.zero → α → β}, (∀ (i : Fin Nat.zero), Memℒp (f i) p) → UnifIntegrable f p μ

case succ
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
⊢ ∀ {f : Fin (Nat.succ n) → α → β}, (∀ (i : Fin (Nat.succ n)), Memℒp (f i) p) → UnifIntegrable f p μ
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
⊢ ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
induction' n with n h
case succ
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
⊢ ∃ δ x,
    ∀ (i : Fin (Nat.succ n)) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
case succ
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
⊢ ∀ {f : Fin (Nat.succ n) → α → β}, (∀ (i : Fin (Nat.succ n)), Memℒp (f i) p) → UnifIntegrable f p μ
intro f hfLp ε hε
case succ
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
⊢ ∃ δ x,
    ∀ (i : Fin (Nat.succ n)) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
case succ
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
⊢ ∃ δ x,
    ∀ (i : Fin (Nat.succ n)) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
let g : Fin n → α → β := fun k => f k
case succ
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
⊢ ∃ δ x,
    ∀ (i : Fin (Nat.succ n)) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
case succ
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
⊢ ∃ δ x,
    ∀ (i : Fin (Nat.succ n)) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
have hgLp : ∀ i, Memℒp (g i) p μ := fun i => hfLp i
case succ.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ x,
    ∀ (i : Fin (Nat.succ n)) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
case succ
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
⊢ ∃ δ x,
    ∀ (i : Fin (Nat.succ n)) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
obtain ⟨δ₁, hδ₁pos, hδ₁⟩ := h hgLp hε
case succ.intro.intro.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ x,
    ∀ (i : Fin (Nat.succ n)) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
case succ.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ x,
    ∀ (i : Fin (Nat.succ n)) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
obtain ⟨δ₂, hδ₂pos, hδ₂⟩ := (hfLp n).snorm_indicator_le μ hp_one hp_top hε
case succ.intro.intro.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
i : Fin (Nat.succ n)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
⊢ snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
case succ.intro.intro.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ x,
    ∀ (i : Fin (Nat.succ n)) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
refine' ⟨min δ₁ δ₂, lt_min hδ₁pos hδ₂pos, fun i s hs hμs => _⟩
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
i : Fin (Nat.succ n)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : ↑i < n
⊢ snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε

case neg
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
i : Fin (Nat.succ n)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : ¬↑i < n
⊢ snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
case succ.intro.intro.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
i : Fin (Nat.succ n)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
⊢ snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
by_cases hi : i.val < n
case zero
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
f : Fin Nat.zero → α → β
hf : ∀ (i : Fin Nat.zero), Memℒp (f i) p
⊢ UnifIntegrable f p μ
case zero
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
⊢ ∀ {f : Fin Nat.zero → α → β}, (∀ (i : Fin Nat.zero), Memℒp (f i) p) → UnifIntegrable f p μ
intro f hf
case zero
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
f : Fin Nat.zero → α → β
hf : ∀ (i : Fin Nat.zero), Memℒp (f i) p
this : Subsingleton (Fin Nat.zero)
⊢ UnifIntegrable f p μ
case zero
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
f : Fin Nat.zero → α → β
hf : ∀ (i : Fin Nat.zero), Memℒp (f i) p
⊢ UnifIntegrable f p μ
have : Subsingleton (Fin Nat.zero) := subsingleton_fin_zero
no goals
case zero
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
f : Fin Nat.zero → α → β
hf : ∀ (i : Fin Nat.zero), Memℒp (f i) p
this : Subsingleton (Fin Nat.zero)
⊢ UnifIntegrable f p μ
exact unifIntegrable_subsingleton μ hp_one hp_top hf
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
i : Fin (Nat.succ n)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : ↑i < n
⊢ snorm (Set.indicator s (g { val := ↑i, isLt := hi })) p μ ≤ ENNReal.ofReal ε

α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
i : Fin (Nat.succ n)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : ↑i < n
⊢ f i = g { val := ↑i, isLt := hi }
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
i : Fin (Nat.succ n)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : ↑i < n
⊢ snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
rw [(_ : f i = g ⟨i.val, hi⟩)]
no goals
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
i : Fin (Nat.succ n)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : ↑i < n
⊢ snorm (Set.indicator s (g { val := ↑i, isLt := hi })) p μ ≤ ENNReal.ofReal ε
exact hδ₁ _ s hs (le_trans hμs <| ENNReal.ofReal_le_ofReal <| min_le_left _ _)
no goals
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
i : Fin (Nat.succ n)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : ↑i < n
⊢ f i = g { val := ↑i, isLt := hi }
simp
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
i : Fin (Nat.succ n)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : ¬↑i < n
⊢ snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε

α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
i : Fin (Nat.succ n)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : ¬↑i < n
⊢ i = ↑n
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
i : Fin (Nat.succ n)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : ¬↑i < n
⊢ snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
rw [(_ : i = n)]
no goals
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
i : Fin (Nat.succ n)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : ¬↑i < n
⊢ snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
exact hδ₂ _ hs (le_trans hμs <| ENNReal.ofReal_le_ofReal <| min_le_right _ _)
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
i : Fin (Nat.succ n)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : ¬↑i < n
hi' : ↑i < Nat.succ n
⊢ i = ↑n
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
i : Fin (Nat.succ n)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : ¬↑i < n
⊢ i = ↑n
have hi' := Fin.is_lt i
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
i : Fin (Nat.succ n)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : ¬↑i < n
hi' : ↑i ≤ n
⊢ i = ↑n
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
i : Fin (Nat.succ n)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : ¬↑i < n
hi' : ↑i < Nat.succ n
⊢ i = ↑n
rw [Nat.lt_succ_iff] at hi'
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
i : Fin (Nat.succ n)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : n ≤ ↑i
hi' : ↑i ≤ n
⊢ i = ↑n
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
i : Fin (Nat.succ n)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : ¬↑i < n
hi' : ↑i ≤ n
⊢ i = ↑n
rw [not_lt] at hi
case h
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
i : Fin (Nat.succ n)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : n ≤ ↑i
hi' : ↑i ≤ n
⊢ ↑i = ↑↑n
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
i : Fin (Nat.succ n)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : n ≤ ↑i
hi' : ↑i ≤ n
⊢ i = ↑n
ext
case h
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
i : Fin (Nat.succ n)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : n ≤ ↑i
hi' : ↑i ≤ n
⊢ ↑↑n = ↑i
case h
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
i : Fin (Nat.succ n)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : n ≤ ↑i
hi' : ↑i ≤ n
⊢ ↑i = ↑↑n
symm
no goals
case h
α : Type u_2
β : Type u_1
ι : Type ?u.187575
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p) → UnifIntegrable f p μ
f : Fin (Nat.succ n) → α → β
hfLp : ∀ (i : Fin (Nat.succ n)), Memℒp (f i) p
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k => f ↑↑k
hgLp : ∀ (i : Fin n), Memℒp (g i) p
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => g i) i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₂ → snorm (Set.indicator s (f ↑n)) p μ ≤ ENNReal.ofReal ε
i : Fin (Nat.succ n)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : n ≤ ↑i
hi' : ↑i ≤ n
⊢ ↑↑n = ↑i
rw [Fin.coe_ofNat_eq_mod, le_antisymm hi' hi, Nat.mod_succ_eq_iff_lt, Nat.lt_succ]