α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
⊢ UnifIntegrable f p μ
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
⊢ UnifIntegrable f p μ
have hpzero := (lt_of_lt_of_le zero_lt_one hp).ne.symm
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ↑↑μ Set.univ = 0
⊢ UnifIntegrable f p μ

case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
⊢ UnifIntegrable f p μ
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
⊢ UnifIntegrable f p μ
by_cases hμ : μ Set.univ = 0
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
⊢ ∃ δ x,
    ∀ (i : ι) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
⊢ UnifIntegrable f p μ
intro ε hε
case neg.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
⊢ ∃ δ x,
    ∀ (i : ι) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
⊢ ∃ δ x,
    ∀ (i : ι) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
obtain ⟨C, hCpos, hC⟩ := h (ε / 2) (half_pos hε)
case neg.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
⊢ snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
case neg.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
⊢ ∃ δ x,
    ∀ (i : ι) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
refine' ⟨(ε / (2 * C)) ^ ENNReal.toReal p,
  Real.rpow_pos_of_pos (div_pos hε (mul_pos two_pos (NNReal.coe_pos.2 hCpos))) _,
  fun i s hs hμs => _⟩
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ↑↑μ s = 0
⊢ snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε

case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
case neg.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
⊢ snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
by_cases hμs' : μ s = 0
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : μ = 0
⊢ UnifIntegrable f p μ
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ↑↑μ Set.univ = 0
⊢ UnifIntegrable f p μ
rw [Measure.measure_univ_eq_zero] at hμ
no goals
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : μ = 0
⊢ UnifIntegrable f p μ
exact hμ.symm ▸ unifIntegrable_zero_meas
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ↑↑μ s = 0
⊢ 0 ≤ ENNReal.ofReal ε
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ↑↑μ s = 0
⊢ snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
rw [(snorm_eq_zero_iff ((hf i).indicator hs).aestronglyMeasurable hpzero).2
    (indicator_meas_zero hμs')]
no goals
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ↑↑μ s = 0
⊢ 0 ≤ ENNReal.ofReal ε
norm_num
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ snorm (Set.indicator s (f i)) p μ =
    snorm (Set.indicator (s ∩ {x | C ≤ ‖f i x‖₊}) (f i) + Set.indicator (s ∩ {x | ‖f i x‖₊ < C}) (f i)) p μ
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ snorm (Set.indicator s (f i)) p μ ≤
    snorm (Set.indicator (s ∩ {x | C ≤ ‖f i x‖₊}) (f i)) p μ + snorm (Set.indicator (s ∩ {x | ‖f i x‖₊ < C}) (f i)) p μ
refine' le_trans (Eq.le _) (snorm_add_le
  (StronglyMeasurable.aestronglyMeasurable
    ((hf i).indicator (hs.inter (stronglyMeasurable_const.measurableSet_le (hf i).nnnorm))))
  (StronglyMeasurable.aestronglyMeasurable
    ((hf i).indicator (hs.inter ((hf i).nnnorm.measurableSet_lt stronglyMeasurable_const))))
  hp)
case e_f
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ Set.indicator s (f i) = Set.indicator (s ∩ {x | C ≤ ‖f i x‖₊}) (f i) + Set.indicator (s ∩ {x | ‖f i x‖₊ < C}) (f i)
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ snorm (Set.indicator s (f i)) p μ =
    snorm (Set.indicator (s ∩ {x | C ≤ ‖f i x‖₊}) (f i) + Set.indicator (s ∩ {x | ‖f i x‖₊ < C}) (f i)) p μ
congr
case e_f
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ Set.indicator s (f i) = fun x =>
    Set.indicator (s ∩ {x | C ≤ ‖f i x‖₊}) (f i) x + Set.indicator (s ∩ {x | ‖f i x‖₊ < C}) (f i) x
case e_f
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ Set.indicator s (f i) = Set.indicator (s ∩ {x | C ≤ ‖f i x‖₊}) (f i) + Set.indicator (s ∩ {x | ‖f i x‖₊ < C}) (f i)
change _ = fun x => (s ∩ { x : α | C ≤ ‖f i x‖₊ }).indicator (f i) x +
  (s ∩ { x : α | ‖f i x‖₊ < C }).indicator (f i) x
case e_f
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ Set.indicator s (f i) = Set.indicator (s ∩ {x | C ≤ ‖f i x‖₊} ∪ s ∩ {x | ‖f i x‖₊ < C}) (f i)

case e_f.h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ Disjoint (s ∩ {x | C ≤ ‖f i x‖₊}) (s ∩ {x | ‖f i x‖₊ < C})
case e_f
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ Set.indicator s (f i) = fun x =>
    Set.indicator (s ∩ {x | C ≤ ‖f i x‖₊}) (f i) x + Set.indicator (s ∩ {x | ‖f i x‖₊ < C}) (f i) x
rw [← Set.indicator_union_of_disjoint]
case e_f
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ Set.indicator s (f i) = Set.indicator (s ∩ {x | C ≤ ‖f i x‖₊} ∪ s ∩ {x | ‖f i x‖₊ < C}) (f i)
case e_f
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ Set.indicator s (f i) = Set.indicator (s ∩ {x | C ≤ ‖f i x‖₊} ∪ s ∩ {x | ‖f i x‖₊ < C}) (f i)
congr
no goals
case e_f
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ Set.indicator s (f i) = Set.indicator (s ∩ {x | C ≤ ‖f i x‖₊} ∪ s ∩ {x | ‖f i x‖₊ < C}) (f i)
rw [← Set.inter_union_distrib_left, (by ext; simp [le_or_lt] :
    { x : α | C ≤ ‖f i x‖₊ } ∪ { x : α | ‖f i x‖₊ < C } = Set.univ),
  Set.inter_univ]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
x✝ : α
⊢ x✝ ∈ {x | C ≤ ‖f i x‖₊} ∪ {x | ‖f i x‖₊ < C} ↔ x✝ ∈ Set.univ
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ {x | C ≤ ‖f i x‖₊} ∪ {x | ‖f i x‖₊ < C} = Set.univ
ext
no goals
case h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
x✝ : α
⊢ x✝ ∈ {x | C ≤ ‖f i x‖₊} ∪ {x | ‖f i x‖₊ < C} ↔ x✝ ∈ Set.univ
simp [le_or_lt]
case e_f.h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ Disjoint {x | C ≤ ‖f i x‖₊} {x | ‖f i x‖₊ < C}
case e_f.h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ Disjoint (s ∩ {x | C ≤ ‖f i x‖₊}) (s ∩ {x | ‖f i x‖₊ < C})
refine' (Disjoint.inf_right' _ _).inf_left' _
case e_f.h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ {x | C ≤ ‖f i x‖₊} ⊓ {x | ‖f i x‖₊ < C} ≤ ⊥
case e_f.h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ Disjoint {x | C ≤ ‖f i x‖₊} {x | ‖f i x‖₊ < C}
rw [disjoint_iff_inf_le]
case e_f.h.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
x : α
hx₁ : x ∈ {x | C ≤ ‖f i x‖₊}
hx₂ : x ∈ {x | ‖f i x‖₊ < C}
⊢ x ∈ ⊥
case e_f.h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ {x | C ≤ ‖f i x‖₊} ⊓ {x | ‖f i x‖₊ < C} ≤ ⊥
rintro x ⟨hx₁, hx₂⟩
case e_f.h.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
x : α
hx₁ : C ≤ ‖f i x‖₊
hx₂ : ‖f i x‖₊ < C
⊢ x ∈ ⊥
case e_f.h.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
x : α
hx₁ : x ∈ {x | C ≤ ‖f i x‖₊}
hx₂ : x ∈ {x | ‖f i x‖₊ < C}
⊢ x ∈ ⊥
rw [Set.mem_setOf_eq] at hx₁ hx₂
no goals
case e_f.h.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
x : α
hx₁ : C ≤ ‖f i x‖₊
hx₂ : ‖f i x‖₊ < C
⊢ x ∈ ⊥
exact False.elim (hx₂.ne (eq_of_le_of_not_lt hx₁ (not_lt.2 hx₂.le)).symm)
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ snorm (Set.indicator (s ∩ {x | ‖f i x‖₊ < C}) (f i)) p μ ≤ ↑C * ↑↑μ s ^ (1 / ENNReal.toReal p)
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ snorm (Set.indicator (s ∩ {x | C ≤ ‖f i x‖₊}) (f i)) p μ + snorm (Set.indicator (s ∩ {x | ‖f i x‖₊ < C}) (f i)) p μ ≤
    snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ + ↑C * ↑↑μ s ^ (1 / ENNReal.toReal p)
refine' add_le_add
  (snorm_mono fun x => norm_indicator_le_of_subset (Set.inter_subset_right _ _) _ _) _
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ snorm (Set.indicator s (Set.indicator {x | ‖f i x‖₊ < C} (f i))) p μ ≤ ↑C * ↑↑μ s ^ (1 / ENNReal.toReal p)
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ snorm (Set.indicator (s ∩ {x | ‖f i x‖₊ < C}) (f i)) p μ ≤ ↑C * ↑↑μ s ^ (1 / ENNReal.toReal p)
rw [← Set.indicator_indicator]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ snorm (Set.indicator {x | ‖f i x‖₊ < C} (f i)) p (Measure.restrict μ s) ≤ ↑C * ↑↑μ s ^ (1 / ENNReal.toReal p)
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ snorm (Set.indicator s (Set.indicator {x | ‖f i x‖₊ < C} (f i))) p μ ≤ ↑C * ↑↑μ s ^ (1 / ENNReal.toReal p)
rw [snorm_indicator_eq_snorm_restrict hs]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
this : ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖Set.indicator {x | ‖f i x‖₊ < C} (f i) x‖ ≤ ↑C
⊢ snorm (Set.indicator {x | ‖f i x‖₊ < C} (f i)) p (Measure.restrict μ s) ≤ ↑C * ↑↑μ s ^ (1 / ENNReal.toReal p)
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ snorm (Set.indicator {x | ‖f i x‖₊ < C} (f i)) p (Measure.restrict μ s) ≤ ↑C * ↑↑μ s ^ (1 / ENNReal.toReal p)
have : ∀ᵐ x ∂μ.restrict s, ‖{ x : α | ‖f i x‖₊ < C }.indicator (f i) x‖ ≤ C := by
  refine' ae_of_all _ _
  simp_rw [norm_indicator_eq_indicator_norm]
  exact Set.indicator_le' (fun x (hx : _ < _) => hx.le) fun _ _ => NNReal.coe_nonneg _
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
this : ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖Set.indicator {x | ‖f i x‖₊ < C} (f i) x‖ ≤ ↑C
⊢ ↑↑(Measure.restrict μ s) Set.univ ^ (ENNReal.toReal p)⁻¹ * ENNReal.ofReal ↑C ≤ ↑C * ↑↑μ s ^ (1 / ENNReal.toReal p)
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
this : ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖Set.indicator {x | ‖f i x‖₊ < C} (f i) x‖ ≤ ↑C
⊢ snorm (Set.indicator {x | ‖f i x‖₊ < C} (f i)) p (Measure.restrict μ s) ≤ ↑C * ↑↑μ s ^ (1 / ENNReal.toReal p)
refine' le_trans (snorm_le_of_ae_bound this) _
no goals
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
this : ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖Set.indicator {x | ‖f i x‖₊ < C} (f i) x‖ ≤ ↑C
⊢ ↑↑(Measure.restrict μ s) Set.univ ^ (ENNReal.toReal p)⁻¹ * ENNReal.ofReal ↑C ≤ ↑C * ↑↑μ s ^ (1 / ENNReal.toReal p)
rw [mul_comm, Measure.restrict_apply' hs, Set.univ_inter, ENNReal.ofReal_coe_nnreal, one_div]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ ∀ (a : α), ‖Set.indicator {x | ‖f i x‖₊ < C} (f i) a‖ ≤ ↑C
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖Set.indicator {x | ‖f i x‖₊ < C} (f i) x‖ ≤ ↑C
refine' ae_of_all _ _
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ ∀ (a : α), Set.indicator {x | ‖f i x‖₊ < C} (fun a => ‖f i a‖) a ≤ ↑C
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ ∀ (a : α), ‖Set.indicator {x | ‖f i x‖₊ < C} (f i) a‖ ≤ ↑C
simp_rw [norm_indicator_eq_indicator_norm]
no goals
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ ∀ (a : α), Set.indicator {x | ‖f i x‖₊ < C} (fun a => ‖f i a‖) a ≤ ↑C
exact Set.indicator_le' (fun x (hx : _ < _) => hx.le) fun _ _ => NNReal.coe_nonneg _
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ ↑↑μ s ^ (1 / ENNReal.toReal p) ≤ ENNReal.ofReal (ε / (2 * ↑C))
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ + ↑C * ↑↑μ s ^ (1 / ENNReal.toReal p) ≤
    ENNReal.ofReal (ε / 2) + ↑C * ENNReal.ofReal (ε / (2 * ↑C))
refine' add_le_add (hC i) (mul_le_mul_left' _ _)
no goals
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ ↑↑μ s ^ (1 / ENNReal.toReal p) ≤ ENNReal.ofReal (ε / (2 * ↑C))
rwa [ENNReal.rpow_one_div_le_iff (ENNReal.toReal_pos hpzero hp'),
  ENNReal.ofReal_rpow_of_pos (div_pos hε (mul_pos two_pos (NNReal.coe_pos.2 hCpos)))]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ ↑C * ENNReal.ofReal (ε / (2 * ↑C)) ≤ ENNReal.ofReal (ε / 2)
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ ENNReal.ofReal (ε / 2) + ↑C * ENNReal.ofReal (ε / (2 * ↑C)) ≤ ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2)
refine' add_le_add_left _ _
no goals
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ ↑C * ENNReal.ofReal (ε / (2 * ↑C)) ≤ ENNReal.ofReal (ε / 2)
rw [← ENNReal.ofReal_coe_nnreal, ← ENNReal.ofReal_mul (NNReal.coe_nonneg _), ← div_div,
  mul_div_cancel' _ (NNReal.coe_pos.2 hCpos).ne.symm]
no goals
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬↑↑μ Set.univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ ENNReal.toReal p)
hμs' : ¬↑↑μ s = 0
⊢ ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2) ≤ ENNReal.ofReal ε
rw [← ENNReal.ofReal_add (half_pos hε).le (half_pos hε).le, add_halves]