[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
⊢ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ = ∫⁻ (a : α), edist (f a) 0 ∂μ
[PROOFSTEP]
simp only [edist_eq_coe_nnnorm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∫⁻ (a : α), edist (f a) 0 ∂μ
[PROOFSTEP]
simp only [ofReal_norm_eq_coe_nnnorm, edist_eq_coe_nnnorm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
⊢ ∫⁻ (a : α), edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), edist (f a) (h a) ∂μ + ∫⁻ (a : α), edist (g a) (h a) ∂μ
[PROOFSTEP]
rw [← lintegral_add_left' (hf.edist hh)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
⊢ ∫⁻ (a : α), edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), edist (f a) (h a) + edist (g a) (h a) ∂μ
[PROOFSTEP]
refine' lintegral_mono fun a => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
a : α
⊢ edist (f a) (g a) ≤ edist (f a) (h a) + edist (g a) (h a)
[PROOFSTEP]
apply edist_triangle_right
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
⊢ ∫⁻ (x : α), ↑‖0‖₊ ∂μ = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
⊢ ∫⁻ (a : α), ↑‖(-f) a‖₊ ∂μ = ∫⁻ (a : α), ↑‖f a‖₊ ∂μ
[PROOFSTEP]
simp only [Pi.neg_apply, nnnorm_neg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
⊢ HasFiniteIntegral f ↔ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ < ⊤
[PROOFSTEP]
simp only [HasFiniteIntegral, ofReal_norm_eq_coe_nnnorm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
⊢ HasFiniteIntegral f ↔ ∫⁻ (a : α), edist (f a) 0 ∂μ < ⊤
[PROOFSTEP]
simp only [hasFiniteIntegral_iff_norm, edist_dist, dist_zero_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
h : 0 ≤ᵐ[μ] f
⊢ HasFiniteIntegral f ↔ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ⊤
[PROOFSTEP]
rw [HasFiniteIntegral, lintegral_nnnorm_eq_of_ae_nonneg h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0
⊢ (HasFiniteIntegral fun x => ↑(f x)) ↔ ∫⁻ (a : α), ↑(f a) ∂μ < ⊤
[PROOFSTEP]
simp [hasFiniteIntegral_iff_norm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
g : α → γ
hg : HasFiniteIntegral g
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖
⊢ HasFiniteIntegral f
[PROOFSTEP]
simp only [hasFiniteIntegral_iff_norm] at *
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
g : α → γ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖
hg : ∫⁻ (a : α), ENNReal.ofReal ‖g a‖ ∂μ < ⊤
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ < ⊤
[PROOFSTEP]
calc
  (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ) ≤ ∫⁻ a : α, ENNReal.ofReal ‖g a‖ ∂μ :=
    lintegral_mono_ae (h.mono fun a h => ofReal_le_ofReal h)
  _ < ∞ := hg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
c : β
⊢ (HasFiniteIntegral fun x => c) ↔ c = 0 ∨ ↑↑μ univ < ⊤
[PROOFSTEP]
simp [HasFiniteIntegral, lintegral_const, lt_top_iff_ne_top, ENNReal.mul_eq_top, or_iff_not_imp_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hμ : HasFiniteIntegral f
hν : HasFiniteIntegral f
⊢ HasFiniteIntegral f
[PROOFSTEP]
simp only [HasFiniteIntegral, lintegral_add_measure] at *
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hμ : ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤
hν : ∫⁻ (a : α), ↑‖f a‖₊ ∂ν < ⊤
⊢ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ + ∫⁻ (a : α), ↑‖f a‖₊ ∂ν < ⊤
[PROOFSTEP]
exact add_lt_top.2 ⟨hμ, hν⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
h : HasFiniteIntegral f
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ HasFiniteIntegral f
[PROOFSTEP]
simp only [HasFiniteIntegral, lintegral_smul_measure] at *
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
c : ℝ≥0∞
hc : c ≠ ⊤
h : ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤
⊢ c * ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤
[PROOFSTEP]
exact mul_lt_top hc h.ne
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m✝ : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
m : MeasurableSpace α
f : α → β
⊢ HasFiniteIntegral f
[PROOFSTEP]
simp only [HasFiniteIntegral, lintegral_zero_measure, WithTop.zero_lt_top]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
⊢ HasFiniteIntegral fun x => 0
[PROOFSTEP]
simp [HasFiniteIntegral]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hfi : HasFiniteIntegral f
⊢ HasFiniteIntegral (-f)
[PROOFSTEP]
simpa [HasFiniteIntegral] using hfi
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hfi : HasFiniteIntegral f
⊢ HasFiniteIntegral fun a => ‖f a‖
[PROOFSTEP]
have eq : (fun a => (nnnorm ‖f a‖ : ℝ≥0∞)) = fun a => (‖f a‖₊ : ℝ≥0∞) :=
  by
  funext
  rw [nnnorm_norm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hfi : HasFiniteIntegral f
⊢ (fun a => ↑‖‖f a‖‖₊) = fun a => ↑‖f a‖₊
[PROOFSTEP]
funext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hfi : HasFiniteIntegral f
x✝ : α
⊢ ↑‖‖f x✝‖‖₊ = ↑‖f x✝‖₊
[PROOFSTEP]
rw [nnnorm_norm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hfi : HasFiniteIntegral f
eq : (fun a => ↑‖‖f a‖‖₊) = fun a => ↑‖f a‖₊
⊢ HasFiniteIntegral fun a => ‖f a‖
[PROOFSTEP]
rwa [HasFiniteIntegral, eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
⊢ HasFiniteIntegral fun x => ENNReal.toReal (f x)
[PROOFSTEP]
have : ∀ x, (‖(f x).toReal‖₊ : ℝ≥0∞) = ENNReal.some ⟨(f x).toReal, ENNReal.toReal_nonneg⟩ :=
  by
  intro x
  rw [Real.nnnorm_of_nonneg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
⊢ ∀ (x : α), ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
x : α
⊢ ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
[PROOFSTEP]
rw [Real.nnnorm_of_nonneg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
this :
  ∀ (x : α), ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
⊢ HasFiniteIntegral fun x => ENNReal.toReal (f x)
[PROOFSTEP]
simp_rw [HasFiniteIntegral, this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
this :
  ∀ (x : α), ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
⊢ ∫⁻ (a : α), ↑{ val := ENNReal.toReal (f a), property := (_ : 0 ≤ ENNReal.toReal (f a)) } ∂μ < ⊤
[PROOFSTEP]
refine' lt_of_le_of_lt (lintegral_mono fun x => _) (lt_top_iff_ne_top.2 hf)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
this :
  ∀ (x : α), ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
x : α
⊢ ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) } ≤ f x
[PROOFSTEP]
by_cases hfx : f x = ∞
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
this :
  ∀ (x : α), ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
x : α
hfx : f x = ⊤
⊢ ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) } ≤ f x
[PROOFSTEP]
simp [hfx]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
this :
  ∀ (x : α), ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
x : α
hfx : ¬f x = ⊤
⊢ ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) } ≤ f x
[PROOFSTEP]
lift f x to ℝ≥0 using hfx with fx h
[GOAL]
case neg.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
this :
  ∀ (x : α), ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
x : α
fx : ℝ≥0
h : ↑fx = f x
⊢ ↑{ val := ENNReal.toReal ↑fx, property := (_ : (fun r => 0 ≤ r) (ENNReal.toReal ↑fx)) } ≤ ↑fx
[PROOFSTEP]
simp [← h]
[GOAL]
case neg.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
this :
  ∀ (x : α), ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
x : α
fx : ℝ≥0
h : ↑fx = f x
⊢ { val := ↑fx, property := (_ : (fun r => 0 ≤ r) ↑fx) } ≤ fx
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
hfi : HasFiniteIntegral f
⊢ IsFiniteMeasure (Measure.withDensity μ fun x => ENNReal.ofReal (f x))
[PROOFSTEP]
refine' isFiniteMeasure_withDensity ((lintegral_mono fun x => _).trans_lt hfi).ne
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
hfi : HasFiniteIntegral f
x : α
⊢ ENNReal.ofReal (f x) ≤ ↑‖f x‖₊
[PROOFSTEP]
exact Real.ofReal_le_ennnorm (f x)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F : ℕ → α → β
f : α → β
bound : α → ℝ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
⊢ ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
[PROOFSTEP]
have F_le_bound := all_ae_ofReal_F_le_bound h_bound
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F : ℕ → α → β
f : α → β
bound : α → ℝ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
F_le_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
⊢ ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
[PROOFSTEP]
rw [← ae_all_iff] at F_le_bound 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F : ℕ → α → β
f : α → β
bound : α → ℝ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
F_le_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)
⊢ ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
[PROOFSTEP]
apply F_le_bound.mp ((all_ae_tendsto_ofReal_norm h_lim).mono _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F : ℕ → α → β
f : α → β
bound : α → ℝ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
F_le_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)
⊢ ∀ (x : α),
    Tendsto (fun n => ENNReal.ofReal ‖F n x‖) atTop (𝓝 (ENNReal.ofReal ‖f x‖)) →
      (∀ (i : ℕ), ENNReal.ofReal ‖F i x‖ ≤ ENNReal.ofReal (bound x)) → ENNReal.ofReal ‖f x‖ ≤ ENNReal.ofReal (bound x)
[PROOFSTEP]
intro a tendsto_norm F_le_bound
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F : ℕ → α → β
f : α → β
bound : α → ℝ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
F_le_bound✝ : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)
a : α
tendsto_norm : Tendsto (fun n => ENNReal.ofReal ‖F n a‖) atTop (𝓝 (ENNReal.ofReal ‖f a‖))
F_le_bound : ∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)
⊢ ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
[PROOFSTEP]
exact le_of_tendsto' tendsto_norm F_le_bound
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
⊢ HasFiniteIntegral f
[PROOFSTEP]
rw [hasFiniteIntegral_iff_norm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ < ⊤
[PROOFSTEP]
calc
  (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ) ≤ ∫⁻ a, ENNReal.ofReal (bound a) ∂μ :=
    lintegral_mono_ae <| all_ae_ofReal_f_le_bound h_bound h_lim
  _ < ∞ := by
    rw [← hasFiniteIntegral_iff_ofReal]
    · exact bound_hasFiniteIntegral
    exact (h_bound 0).mono fun a h => le_trans (norm_nonneg _) h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
⊢ ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ < ⊤
[PROOFSTEP]
rw [← hasFiniteIntegral_iff_ofReal]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
⊢ HasFiniteIntegral fun a => bound a
[PROOFSTEP]
exact bound_hasFiniteIntegral
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
⊢ 0 ≤ᵐ[μ] fun a => bound a
[PROOFSTEP]
exact (h_bound 0).mono fun a h => le_trans (norm_nonneg _) h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
⊢ Tendsto (fun n => ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 0)
[PROOFSTEP]
have f_measurable : AEStronglyMeasurable f μ := aestronglyMeasurable_of_tendsto_ae _ F_measurable h_lim
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
⊢ Tendsto (fun n => ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 0)
[PROOFSTEP]
let b a :=
  2 *
    ENNReal.ofReal
      (bound a)
        /- `‖F n a‖ ≤ bound a` and `F n a --> f a` implies `‖f a‖ ≤ bound a`, and thus by the
            triangle inequality, have `‖F n a - f a‖ ≤ 2 * (bound a)`. -/
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
⊢ Tendsto (fun n => ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 0)
[PROOFSTEP]
have hb : ∀ n, ∀ᵐ a ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a :=
  by
  intro n
  filter_upwards [all_ae_ofReal_F_le_bound h_bound n, all_ae_ofReal_f_le_bound h_bound h_lim] with a h₁ h₂
  calc
    ENNReal.ofReal ‖F n a - f a‖ ≤ ENNReal.ofReal ‖F n a‖ + ENNReal.ofReal ‖f a‖ :=
      by
      rw [← ENNReal.ofReal_add]
      apply ofReal_le_ofReal
      · {apply norm_sub_le
      };
      · {exact norm_nonneg _
      };
      · {exact norm_nonneg _
      }
    _ ≤ ENNReal.ofReal (bound a) + ENNReal.ofReal (bound a) := (add_le_add h₁ h₂)
    _ = b a := by
      rw [← two_mul]
        -- On the other hand, `F n a --> f a` implies that `‖F n a - f a‖ --> 0`
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
⊢ ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
[PROOFSTEP]
intro n
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
n : ℕ
⊢ ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
[PROOFSTEP]
filter_upwards [all_ae_ofReal_F_le_bound h_bound n, all_ae_ofReal_f_le_bound h_bound h_lim] with a h₁ h₂
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ ENNReal.ofReal ‖F n a - f a‖ ≤ 2 * ENNReal.ofReal (bound a)
[PROOFSTEP]
calc
  ENNReal.ofReal ‖F n a - f a‖ ≤ ENNReal.ofReal ‖F n a‖ + ENNReal.ofReal ‖f a‖ :=
    by
    rw [← ENNReal.ofReal_add]
    apply ofReal_le_ofReal
    · {apply norm_sub_le
    };
    · {exact norm_nonneg _
    };
    · {exact norm_nonneg _
    }
  _ ≤ ENNReal.ofReal (bound a) + ENNReal.ofReal (bound a) := (add_le_add h₁ h₂)
  _ = b a := by
    rw [← two_mul]
      -- On the other hand, `F n a --> f a` implies that `‖F n a - f a‖ --> 0`
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ ENNReal.ofReal ‖F n a - f a‖ ≤ ENNReal.ofReal ‖F n a‖ + ENNReal.ofReal ‖f a‖
[PROOFSTEP]
rw [← ENNReal.ofReal_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ ENNReal.ofReal ‖F n a - f a‖ ≤ ENNReal.ofReal (‖F n a‖ + ‖f a‖)
case hp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ 0 ≤ ‖F n a‖
case hq
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ 0 ≤ ‖f a‖
[PROOFSTEP]
apply ofReal_le_ofReal
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ ‖F n a - f a‖ ≤ ‖F n a‖ + ‖f a‖
[PROOFSTEP]
{apply norm_sub_le
}
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ ‖F n a - f a‖ ≤ ‖F n a‖ + ‖f a‖
[PROOFSTEP]
apply norm_sub_le
[GOAL]
case hp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ 0 ≤ ‖F n a‖
[PROOFSTEP]
{exact norm_nonneg _
}
[GOAL]
case hp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ 0 ≤ ‖F n a‖
[PROOFSTEP]
exact norm_nonneg _
[GOAL]
case hq
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ 0 ≤ ‖f a‖
[PROOFSTEP]
{exact norm_nonneg _
}
[GOAL]
case hq
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ 0 ≤ ‖f a‖
[PROOFSTEP]
exact norm_nonneg _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ ENNReal.ofReal (bound a) + ENNReal.ofReal (bound a) = b a
[PROOFSTEP]
rw [← two_mul]
  -- On the other hand, `F n a --> f a` implies that `‖F n a - f a‖ --> 0`
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
⊢ Tendsto (fun n => ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 0)
[PROOFSTEP]
have h : ∀ᵐ a ∂μ, Tendsto (fun n => ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0) :=
  by
  rw [← ENNReal.ofReal_zero]
  refine' h_lim.mono fun a h => (continuous_ofReal.tendsto _).comp _
  rwa [← tendsto_iff_norm_tendsto_zero]
    /- Therefore, by the dominated convergence theorem for nonnegative integration, have
        ` ∫ ‖f a - F n a‖ --> 0 ` -/
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n => ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
[PROOFSTEP]
rw [← ENNReal.ofReal_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n => ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 (ENNReal.ofReal 0))
[PROOFSTEP]
refine' h_lim.mono fun a h => (continuous_ofReal.tendsto _).comp _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
a : α
h : Tendsto (fun n => F n a) atTop (𝓝 (f a))
⊢ Tendsto (fun n => ‖F n a - f a‖) atTop (𝓝 0)
[PROOFSTEP]
rwa [← tendsto_iff_norm_tendsto_zero]
  /- Therefore, by the dominated convergence theorem for nonnegative integration, have
      ` ∫ ‖f a - F n a‖ --> 0 ` -/
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ Tendsto (fun n => ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 0)
[PROOFSTEP]
suffices h : Tendsto (fun n => ∫⁻ a, ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 (∫⁻ _ : α, 0 ∂μ))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h✝ : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
h : Tendsto (fun n => ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 (∫⁻ (x : α), 0 ∂μ))
⊢ Tendsto (fun n => ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 0)
[PROOFSTEP]
rwa [lintegral_zero] at h 
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ Tendsto (fun n => ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 (∫⁻ (x : α), 0 ∂μ))
[PROOFSTEP]
refine'
  tendsto_lintegral_of_dominated_convergence' _ _ hb _
    _
      -- Show `λa, ‖f a - F n a‖` is almost everywhere measurable for all `n`
[GOAL]
case h.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ ∀ (n : ℕ), AEMeasurable fun a => ENNReal.ofReal ‖F n a - f a‖
[PROOFSTEP]
exact fun n => measurable_ofReal.comp_aemeasurable ((F_measurable n).sub f_measurable).norm.aemeasurable
[GOAL]
case h.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ ∫⁻ (a : α), b a ∂μ ≠ ⊤
[PROOFSTEP]
rw [hasFiniteIntegral_iff_ofReal] at bound_hasFiniteIntegral 
[GOAL]
case h.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ < ⊤
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ ∫⁻ (a : α), b a ∂μ ≠ ⊤
[PROOFSTEP]
calc
  ∫⁻ a, b a ∂μ = 2 * ∫⁻ a, ENNReal.ofReal (bound a) ∂μ :=
    by
    rw [lintegral_const_mul']
    exact coe_ne_top
  _ ≠ ∞ := mul_ne_top coe_ne_top bound_hasFiniteIntegral.ne
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ < ⊤
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ ∫⁻ (a : α), b a ∂μ = 2 * ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ
[PROOFSTEP]
rw [lintegral_const_mul']
[GOAL]
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ < ⊤
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ 2 ≠ ⊤
[PROOFSTEP]
exact coe_ne_top
[GOAL]
case h.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ 0 ≤ᵐ[μ] bound
[PROOFSTEP]
filter_upwards [h_bound 0] with _ h using le_trans (norm_nonneg _) h
[GOAL]
case h.refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
F✝ : ℕ → α → β
f✝ : α → β
bound✝ : α → ℝ
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a => 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n => ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
[PROOFSTEP]
exact h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
hf : HasFiniteIntegral f
x : α
⊢ ‖max (f x) 0‖ ≤ ‖f x‖
[PROOFSTEP]
simp [abs_le, le_abs_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
hf : HasFiniteIntegral f
x : α
⊢ ‖min (f x) 0‖ ≤ ‖f x‖
[PROOFSTEP]
simp [abs_le, neg_le, neg_le_abs_self, abs_eq_max_neg, le_total]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
⊢ HasFiniteIntegral f → HasFiniteIntegral (c • f)
[PROOFSTEP]
simp only [HasFiniteIntegral]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
⊢ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤ → ∫⁻ (a : α), ↑‖(c • f) a‖₊ ∂μ < ⊤
[PROOFSTEP]
intro hfi
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤
⊢ ∫⁻ (a : α), ↑‖(c • f) a‖₊ ∂μ < ⊤
[PROOFSTEP]
calc
  (∫⁻ a : α, ‖c • f a‖₊ ∂μ) ≤ ∫⁻ a : α, ‖c‖₊ * ‖f a‖₊ ∂μ :=
    by
    refine' lintegral_mono _
    intro i
    exact_mod_cast (nnnorm_smul_le c (f i))
  _ < ∞ := by
    rw [lintegral_const_mul']
    exacts [mul_lt_top coe_ne_top hfi.ne, coe_ne_top]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤
⊢ ∫⁻ (a : α), ↑‖c • f a‖₊ ∂μ ≤ ∫⁻ (a : α), ↑‖c‖₊ * ↑‖f a‖₊ ∂μ
[PROOFSTEP]
refine' lintegral_mono _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤
⊢ (fun a => ↑‖c • f a‖₊) ≤ fun a => ↑‖c‖₊ * ↑‖f a‖₊
[PROOFSTEP]
intro i
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤
i : α
⊢ (fun a => ↑‖c • f a‖₊) i ≤ (fun a => ↑‖c‖₊ * ↑‖f a‖₊) i
[PROOFSTEP]
exact_mod_cast (nnnorm_smul_le c (f i))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤
⊢ ∫⁻ (a : α), ↑‖c‖₊ * ↑‖f a‖₊ ∂μ < ⊤
[PROOFSTEP]
rw [lintegral_const_mul']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤
⊢ ↑‖c‖₊ * ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤
⊢ ↑‖c‖₊ ≠ ⊤
[PROOFSTEP]
exacts [mul_lt_top coe_ne_top hfi.ne, coe_ne_top]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
hc : IsUnit c
f : α → β
⊢ HasFiniteIntegral (c • f) ↔ HasFiniteIntegral f
[PROOFSTEP]
obtain ⟨c, rfl⟩ := hc
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → β
c : 𝕜ˣ
⊢ HasFiniteIntegral (↑c • f) ↔ HasFiniteIntegral f
[PROOFSTEP]
constructor
[GOAL]
case intro.mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → β
c : 𝕜ˣ
⊢ HasFiniteIntegral (↑c • f) → HasFiniteIntegral f
[PROOFSTEP]
intro h
[GOAL]
case intro.mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → β
c : 𝕜ˣ
h : HasFiniteIntegral (↑c • f)
⊢ HasFiniteIntegral f
[PROOFSTEP]
simpa only [smul_smul, Units.inv_mul, one_smul] using h.smul ((c⁻¹ : 𝕜ˣ) : 𝕜)
[GOAL]
case intro.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → β
c : 𝕜ˣ
⊢ HasFiniteIntegral f → HasFiniteIntegral (↑c • f)
[PROOFSTEP]
exact HasFiniteIntegral.smul _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
⊢ Memℒp f 1 ↔ Integrable f
[PROOFSTEP]
simp_rw [Integrable, HasFiniteIntegral, Memℒp, snorm_one_eq_lintegral_nnnorm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
c : β
⊢ (Integrable fun x => c) ↔ c = 0 ∨ ↑↑μ univ < ⊤
[PROOFSTEP]
have : AEStronglyMeasurable (fun _ : α => c) μ := aestronglyMeasurable_const
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
c : β
this : AEStronglyMeasurable (fun x => c) μ
⊢ (Integrable fun x => c) ↔ c = 0 ∨ ↑↑μ univ < ⊤
[PROOFSTEP]
rw [Integrable, and_iff_right this, hasFiniteIntegral_const_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
p : ℝ≥0∞
hf : Memℒp f p
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
⊢ Integrable fun x => ‖f x‖ ^ ENNReal.toReal p
[PROOFSTEP]
rw [← memℒp_one_iff_integrable]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
p : ℝ≥0∞
hf : Memℒp f p
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
⊢ Memℒp (fun x => ‖f x‖ ^ ENNReal.toReal p) 1
[PROOFSTEP]
exact hf.norm_rpow hp_ne_zero hp_ne_top
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : Memℒp f p
⊢ Integrable fun x => ‖f x‖ ^ ENNReal.toReal p
[PROOFSTEP]
by_cases h_zero : p = 0
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : Memℒp f p
h_zero : p = 0
⊢ Integrable fun x => ‖f x‖ ^ ENNReal.toReal p
[PROOFSTEP]
simp [h_zero, integrable_const]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : Memℒp f p
h_zero : ¬p = 0
⊢ Integrable fun x => ‖f x‖ ^ ENNReal.toReal p
[PROOFSTEP]
by_cases h_top : p = ∞
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : Memℒp f p
h_zero : ¬p = 0
h_top : p = ⊤
⊢ Integrable fun x => ‖f x‖ ^ ENNReal.toReal p
[PROOFSTEP]
simp [h_top, integrable_const]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : Memℒp f p
h_zero : ¬p = 0
h_top : ¬p = ⊤
⊢ Integrable fun x => ‖f x‖ ^ ENNReal.toReal p
[PROOFSTEP]
exact hf.integrable_norm_rpow h_zero h_top
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → β
hf : Integrable f
⊢ Integrable f
[PROOFSTEP]
rw [← memℒp_one_iff_integrable] at hf ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → β
hf : Memℒp f 1
⊢ Memℒp f 1
[PROOFSTEP]
exact hf.of_measure_le_smul c hc hμ'_le
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hμ : Integrable f
hν : Integrable f
⊢ Integrable f
[PROOFSTEP]
simp_rw [← memℒp_one_iff_integrable] at hμ hν ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hμ : Memℒp f 1
hν : Memℒp f 1
⊢ Memℒp f 1
[PROOFSTEP]
refine' ⟨hμ.aestronglyMeasurable.add_measure hν.aestronglyMeasurable, _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hμ : Memℒp f 1
hν : Memℒp f 1
⊢ snorm f 1 (μ + ν) < ⊤
[PROOFSTEP]
rw [snorm_one_add_measure, ENNReal.add_lt_top]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hμ : Memℒp f 1
hν : Memℒp f 1
⊢ snorm f 1 μ < ⊤ ∧ snorm f 1 ν < ⊤
[PROOFSTEP]
exact ⟨hμ.snorm_lt_top, hν.snorm_lt_top⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
h : Integrable f
⊢ Integrable f
[PROOFSTEP]
rw [← memℒp_one_iff_integrable] at h ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
h : Memℒp f 1
⊢ Memℒp f 1
[PROOFSTEP]
exact h.left_of_add_measure
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
h : Integrable f
⊢ Integrable f
[PROOFSTEP]
rw [← memℒp_one_iff_integrable] at h ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
h : Memℒp f 1
⊢ Memℒp f 1
[PROOFSTEP]
exact h.right_of_add_measure
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m✝ : MeasurableSpace α
μ✝ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
ι : Type u_5
m : MeasurableSpace α
f : α → β
μ : ι → Measure α
s : Finset ι
⊢ Integrable f ↔ ∀ (i : ι), i ∈ s → Integrable f
[PROOFSTEP]
induction s using Finset.induction_on
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m✝ : MeasurableSpace α
μ✝ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
ι : Type u_5
m : MeasurableSpace α
f : α → β
μ : ι → Measure α
⊢ Integrable f ↔ ∀ (i : ι), i ∈ ∅ → Integrable f
[PROOFSTEP]
simp [*]
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m✝ : MeasurableSpace α
μ✝ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
ι : Type u_5
m : MeasurableSpace α
f : α → β
μ : ι → Measure α
a✝² : ι
s✝ : Finset ι
a✝¹ : ¬a✝² ∈ s✝
a✝ : Integrable f ↔ ∀ (i : ι), i ∈ s✝ → Integrable f
⊢ Integrable f ↔ ∀ (i : ι), i ∈ insert a✝² s✝ → Integrable f
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
h : Integrable f
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ Integrable f
[PROOFSTEP]
rw [← memℒp_one_iff_integrable] at h ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
h : Memℒp f 1
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ Memℒp f 1
[PROOFSTEP]
exact h.smul_measure hc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
c : ℝ≥0∞
h₁ : c ≠ 0
h₂ : c ≠ ⊤
h : Integrable f
⊢ Integrable f
[PROOFSTEP]
simpa only [smul_smul, ENNReal.inv_mul_cancel h₁ h₂, one_smul] using h.smul_measure (ENNReal.inv_ne_top.2 h₁)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
c : ℝ≥0∞
h₁ : c ≠ 0
h₂ : c ≠ ⊤
⊢ c⁻¹ ≠ 0
[PROOFSTEP]
simpa using h₂
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
c : ℝ≥0∞
h₁ : c ≠ 0
h₂ : c ≠ ⊤
⊢ c⁻¹ ≠ ⊤
[PROOFSTEP]
simpa using h₁
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
h : Integrable f
⊢ Integrable f
[PROOFSTEP]
rcases eq_or_ne μ 0 with (rfl | hne)
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
h : Integrable f
⊢ Integrable f
[PROOFSTEP]
rwa [smul_zero]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
h : Integrable f
hne : μ ≠ 0
⊢ Integrable f
[PROOFSTEP]
apply h.smul_measure
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
h : Integrable f
hne : μ ≠ 0
⊢ (↑↑μ univ)⁻¹ ≠ ⊤
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
inst✝ : IsFiniteMeasure μ
f : α → β
h : μ = 0
⊢ Integrable f ↔ Integrable f
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → δ
g : δ → β
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f
⊢ Integrable g ↔ Integrable (g ∘ f)
[PROOFSTEP]
simp_rw [← memℒp_one_iff_integrable]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → δ
g : δ → β
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f
⊢ Memℒp g 1 ↔ Memℒp (g ∘ f) 1
[PROOFSTEP]
exact memℒp_map_measure_iff hg hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → δ
hf : MeasurableEmbedding f
g : δ → β
⊢ Integrable g ↔ Integrable (g ∘ f)
[PROOFSTEP]
simp_rw [← memℒp_one_iff_integrable]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → δ
hf : MeasurableEmbedding f
g : δ → β
⊢ Memℒp g 1 ↔ Memℒp (g ∘ f) 1
[PROOFSTEP]
exact hf.memℒp_map_measure_iff
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α ≃ᵐ δ
g : δ → β
⊢ Integrable g ↔ Integrable (g ∘ ↑f)
[PROOFSTEP]
simp_rw [← memℒp_one_iff_integrable]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α ≃ᵐ δ
g : δ → β
⊢ Memℒp g 1 ↔ Memℒp (g ∘ ↑f) 1
[PROOFSTEP]
exact f.memℒp_map_measure_iff
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν✝ : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
ν : Measure δ
g : δ → β
f : α → δ
hf : MeasurePreserving f
hg : AEStronglyMeasurable g ν
⊢ Integrable (g ∘ f) ↔ Integrable g
[PROOFSTEP]
rw [← hf.map_eq] at hg ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν✝ : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
ν : Measure δ
g : δ → β
f : α → δ
hf : MeasurePreserving f
hg : AEStronglyMeasurable g (Measure.map f μ)
⊢ Integrable (g ∘ f) ↔ Integrable g
[PROOFSTEP]
exact (integrable_map_measure hg hf.measurable.aemeasurable).symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : α → β
hf : Integrable f
hg : Integrable g
⊢ ∫⁻ (a : α), edist (f a) (OfNat.ofNat 0 a) ∂μ < ⊤ ∧ ∫⁻ (a : α), edist (g a) (OfNat.ofNat 0 a) ∂μ < ⊤
[PROOFSTEP]
simp_rw [Pi.zero_apply, ← hasFiniteIntegral_iff_edist]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : α → β
hf : Integrable f
hg : Integrable g
⊢ (HasFiniteIntegral fun a => f a) ∧ HasFiniteIntegral fun a => g a
[PROOFSTEP]
exact ⟨hf.hasFiniteIntegral, hg.hasFiniteIntegral⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
⊢ Integrable fun x => 0
[PROOFSTEP]
simp [Integrable, aestronglyMeasurable_const]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : α → β
hf : Integrable f
hg : Integrable g
a : α
⊢ ↑‖f a + g a‖₊ ≤ ↑‖f a‖₊ + ↑‖g a‖₊
[PROOFSTEP]
exact_mod_cast nnnorm_add_le _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
ι : Type u_5
s : Finset ι
f : ι → α → β
hf : ∀ (i : ι), i ∈ s → Integrable (f i)
⊢ Integrable fun a => ∑ i in s, f i a
[PROOFSTEP]
simpa only [← Finset.sum_apply] using integrable_finset_sum' s hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : α → β
hf : Integrable f
hg : Integrable g
⊢ Integrable (f - g)
[PROOFSTEP]
simpa only [sub_eq_add_neg] using hf.add hg.neg
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β✝
inst✝¹ : NormedAddCommGroup γ
β : Type u_5
inst✝ : NormedLatticeAddCommGroup β
f g : α → β
hf : Integrable f
hg : Integrable g
⊢ Integrable (f ⊓ g)
[PROOFSTEP]
rw [← memℒp_one_iff_integrable] at hf hg ⊢
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β✝
inst✝¹ : NormedAddCommGroup γ
β : Type u_5
inst✝ : NormedLatticeAddCommGroup β
f g : α → β
hf : Memℒp f 1
hg : Memℒp g 1
⊢ Memℒp (f ⊓ g) 1
[PROOFSTEP]
exact hf.inf hg
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β✝
inst✝¹ : NormedAddCommGroup γ
β : Type u_5
inst✝ : NormedLatticeAddCommGroup β
f g : α → β
hf : Integrable f
hg : Integrable g
⊢ Integrable (f ⊔ g)
[PROOFSTEP]
rw [← memℒp_one_iff_integrable] at hf hg ⊢
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β✝
inst✝¹ : NormedAddCommGroup γ
β : Type u_5
inst✝ : NormedLatticeAddCommGroup β
f g : α → β
hf : Memℒp f 1
hg : Memℒp g 1
⊢ Memℒp (f ⊔ g) 1
[PROOFSTEP]
exact hf.sup hg
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β✝
inst✝¹ : NormedAddCommGroup γ
β : Type u_5
inst✝ : NormedLatticeAddCommGroup β
f : α → β
hf : Integrable f
⊢ Integrable fun a => |f a|
[PROOFSTEP]
rw [← memℒp_one_iff_integrable] at hf ⊢
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β✝
inst✝¹ : NormedAddCommGroup γ
β : Type u_5
inst✝ : NormedLatticeAddCommGroup β
f : α → β
hf : Memℒp f 1
⊢ Memℒp (fun a => |f a|) 1
[PROOFSTEP]
exact hf.abs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_5
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hfbdd : ∃ C, ∀ (x : α), ‖f x‖ ≤ C
⊢ Integrable fun x => f x * g x
[PROOFSTEP]
cases' isEmpty_or_nonempty α with hα hα
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_5
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hfbdd : ∃ C, ∀ (x : α), ‖f x‖ ≤ C
hα : IsEmpty α
⊢ Integrable fun x => f x * g x
[PROOFSTEP]
rw [μ.eq_zero_of_isEmpty]
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_5
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hfbdd : ∃ C, ∀ (x : α), ‖f x‖ ≤ C
hα : IsEmpty α
⊢ Integrable fun x => f x * g x
[PROOFSTEP]
exact integrable_zero_measure
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_5
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hfbdd : ∃ C, ∀ (x : α), ‖f x‖ ≤ C
hα : Nonempty α
⊢ Integrable fun x => f x * g x
[PROOFSTEP]
refine' ⟨hm.mul hint.1, _⟩
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_5
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hfbdd : ∃ C, ∀ (x : α), ‖f x‖ ≤ C
hα : Nonempty α
⊢ HasFiniteIntegral fun x => f x * g x
[PROOFSTEP]
obtain ⟨C, hC⟩ := hfbdd
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_5
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
⊢ HasFiniteIntegral fun x => f x * g x
[PROOFSTEP]
have hCnonneg : 0 ≤ C := le_trans (norm_nonneg _) (hC hα.some)
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_5
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
⊢ HasFiniteIntegral fun x => f x * g x
[PROOFSTEP]
have : (fun x => ‖f x * g x‖₊) ≤ fun x => ⟨C, hCnonneg⟩ * ‖g x‖₊ :=
  by
  intro x
  simp only [nnnorm_mul]
  exact mul_le_mul_of_nonneg_right (hC x) (zero_le _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_5
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
⊢ (fun x => ‖f x * g x‖₊) ≤ fun x => { val := C, property := hCnonneg } * ‖g x‖₊
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_5
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
x : α
⊢ (fun x => ‖f x * g x‖₊) x ≤ (fun x => { val := C, property := hCnonneg } * ‖g x‖₊) x
[PROOFSTEP]
simp only [nnnorm_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_5
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
x : α
⊢ ‖f x‖₊ * ‖g x‖₊ ≤ { val := C, property := hCnonneg } * ‖g x‖₊
[PROOFSTEP]
exact mul_le_mul_of_nonneg_right (hC x) (zero_le _)
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_5
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
this : (fun x => ‖f x * g x‖₊) ≤ fun x => { val := C, property := hCnonneg } * ‖g x‖₊
⊢ HasFiniteIntegral fun x => f x * g x
[PROOFSTEP]
refine' lt_of_le_of_lt (lintegral_mono_nnreal this) _
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_5
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
this : (fun x => ‖f x * g x‖₊) ≤ fun x => { val := C, property := hCnonneg } * ‖g x‖₊
⊢ ∫⁻ (a : α), ↑({ val := C, property := hCnonneg } * ‖g a‖₊) ∂μ < ⊤
[PROOFSTEP]
simp only [ENNReal.coe_mul]
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_5
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
this : (fun x => ‖f x * g x‖₊) ≤ fun x => { val := C, property := hCnonneg } * ‖g x‖₊
⊢ ∫⁻ (a : α), ↑{ val := C, property := hCnonneg } * ↑‖g a‖₊ ∂μ < ⊤
[PROOFSTEP]
rw [lintegral_const_mul' _ _ ENNReal.coe_ne_top]
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_5
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
this : (fun x => ‖f x * g x‖₊) ≤ fun x => { val := C, property := hCnonneg } * ‖g x‖₊
⊢ ↑{ val := C, property := hCnonneg } * ∫⁻ (a : α), ↑‖g a‖₊ ∂μ < ⊤
[PROOFSTEP]
exact ENNReal.mul_lt_top ENNReal.coe_ne_top (ne_of_lt hint.2)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
f : α → β
hf : Integrable f
g : α → 𝕜
g_ae_strongly_measurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤
⊢ Integrable fun x => g x • f x
[PROOFSTEP]
rw [← memℒp_one_iff_integrable] at *
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
f : α → β
hf : Memℒp f 1
g : α → 𝕜
g_ae_strongly_measurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤
⊢ Memℒp (fun x => g x • f x) 1
[PROOFSTEP]
refine' ⟨g_ae_strongly_measurable.smul hf.1, _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
f : α → β
hf : Memℒp f 1
g : α → 𝕜
g_ae_strongly_measurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤
⊢ snorm (fun x => g x • f x) 1 μ < ⊤
[PROOFSTEP]
have h : (1 : ℝ≥0∞) / 1 = 1 / ∞ + 1 / 1 := by norm_num
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
f : α → β
hf : Memℒp f 1
g : α → 𝕜
g_ae_strongly_measurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤
⊢ 1 / 1 = 1 / ⊤ + 1 / 1
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
f : α → β
hf : Memℒp f 1
g : α → 𝕜
g_ae_strongly_measurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤
h : 1 / 1 = 1 / ⊤ + 1 / 1
⊢ snorm (fun x => g x • f x) 1 μ < ⊤
[PROOFSTEP]
have hg' : snorm g ∞ μ ≠ ∞ := by rwa [snorm_exponent_top]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
f : α → β
hf : Memℒp f 1
g : α → 𝕜
g_ae_strongly_measurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤
h : 1 / 1 = 1 / ⊤ + 1 / 1
⊢ snorm g ⊤ μ ≠ ⊤
[PROOFSTEP]
rwa [snorm_exponent_top]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
f : α → β
hf : Memℒp f 1
g : α → 𝕜
g_ae_strongly_measurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤
h : 1 / 1 = 1 / ⊤ + 1 / 1
hg' : snorm g ⊤ μ ≠ ⊤
⊢ snorm (fun x => g x • f x) 1 μ < ⊤
[PROOFSTEP]
calc
  snorm (fun x : α => g x • f x) 1 μ ≤ _ := MeasureTheory.snorm_smul_le_mul_snorm hf.1 g_ae_strongly_measurable h
  _ < ∞ := ENNReal.mul_lt_top hg' hf.2.ne
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : Integrable f
g : α → β
g_ae_strongly_measurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤
⊢ Integrable fun x => f x • g x
[PROOFSTEP]
rw [← memℒp_one_iff_integrable] at *
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : Memℒp f 1
g : α → β
g_ae_strongly_measurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤
⊢ Memℒp (fun x => f x • g x) 1
[PROOFSTEP]
refine' ⟨hf.1.smul g_ae_strongly_measurable, _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : Memℒp f 1
g : α → β
g_ae_strongly_measurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤
⊢ snorm (fun x => f x • g x) 1 μ < ⊤
[PROOFSTEP]
have h : (1 : ℝ≥0∞) / 1 = 1 / 1 + 1 / ∞ := by norm_num
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : Memℒp f 1
g : α → β
g_ae_strongly_measurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤
⊢ 1 / 1 = 1 / 1 + 1 / ⊤
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : Memℒp f 1
g : α → β
g_ae_strongly_measurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤
h : 1 / 1 = 1 / 1 + 1 / ⊤
⊢ snorm (fun x => f x • g x) 1 μ < ⊤
[PROOFSTEP]
have hg' : snorm g ∞ μ ≠ ∞ := by rwa [snorm_exponent_top]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : Memℒp f 1
g : α → β
g_ae_strongly_measurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤
h : 1 / 1 = 1 / 1 + 1 / ⊤
⊢ snorm g ⊤ μ ≠ ⊤
[PROOFSTEP]
rwa [snorm_exponent_top]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → 𝕜
hf : Memℒp f 1
g : α → β
g_ae_strongly_measurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤
h : 1 / 1 = 1 / 1 + 1 / ⊤
hg' : snorm g ⊤ μ ≠ ⊤
⊢ snorm (fun x => f x • g x) 1 μ < ⊤
[PROOFSTEP]
calc
  snorm (fun x : α => f x • g x) 1 μ ≤ _ := MeasureTheory.snorm_smul_le_mul_snorm g_ae_strongly_measurable hf.1 h
  _ < ∞ := ENNReal.mul_lt_top hf.2.ne hg'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : AEStronglyMeasurable f μ
⊢ (Integrable fun a => ‖f a‖) ↔ Integrable f
[PROOFSTEP]
simp_rw [Integrable, and_iff_right hf, and_iff_right hf.norm, hasFiniteIntegral_norm_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f₀ f₁ : α → β
g : α → ℝ
hf₁_m : AEStronglyMeasurable f₁ μ
hf₀_i : Integrable f₀
hg_i : Integrable g
h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a
⊢ ∀ᵐ (a : α) ∂μ, ‖f₁ a‖ ≤ ‖f₀ a‖ + g a
[PROOFSTEP]
apply h.mono
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f₀ f₁ : α → β
g : α → ℝ
hf₁_m : AEStronglyMeasurable f₁ μ
hf₀_i : Integrable f₀
hg_i : Integrable g
h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a
⊢ ∀ (x : α), ‖f₀ x - f₁ x‖ ≤ g x → ‖f₁ x‖ ≤ ‖f₀ x‖ + g x
[PROOFSTEP]
intro a ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f₀ f₁ : α → β
g : α → ℝ
hf₁_m : AEStronglyMeasurable f₁ μ
hf₀_i : Integrable f₀
hg_i : Integrable g
h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a
a : α
ha : ‖f₀ a - f₁ a‖ ≤ g a
⊢ ‖f₁ a‖ ≤ ‖f₀ a‖ + g a
[PROOFSTEP]
calc
  ‖f₁ a‖ ≤ ‖f₀ a‖ + ‖f₀ a - f₁ a‖ := norm_le_insert _ _
  _ ≤ ‖f₀ a‖ + g a := add_le_add_left ha _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
ε : ℝ
hε : 0 < ε
⊢ ↑↑μ {x | ε ≤ ‖f x‖} < ⊤
[PROOFSTEP]
rw [show {x | ε ≤ ‖f x‖} = {x | ENNReal.ofReal ε ≤ ‖f x‖₊} by
    simp only [ENNReal.ofReal, Real.toNNReal_le_iff_le_coe, ENNReal.coe_le_coe, coe_nnnorm]]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
ε : ℝ
hε : 0 < ε
⊢ {x | ε ≤ ‖f x‖} = {x | ENNReal.ofReal ε ≤ ↑‖f x‖₊}
[PROOFSTEP]
simp only [ENNReal.ofReal, Real.toNNReal_le_iff_le_coe, ENNReal.coe_le_coe, coe_nnnorm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
ε : ℝ
hε : 0 < ε
⊢ ↑↑μ {x | ENNReal.ofReal ε ≤ ↑‖f x‖₊} < ⊤
[PROOFSTEP]
refine' (meas_ge_le_mul_pow_snorm μ one_ne_zero ENNReal.one_ne_top hf.1 _).trans_lt _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
ε : ℝ
hε : 0 < ε
⊢ ENNReal.ofReal ε ≠ 0
[PROOFSTEP]
simpa only [Ne.def, ENNReal.ofReal_eq_zero, not_le] using hε
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
ε : ℝ
hε : 0 < ε
⊢ (ENNReal.ofReal ε)⁻¹ ^ ENNReal.toReal 1 * snorm f 1 μ ^ ENNReal.toReal 1 < ⊤
[PROOFSTEP]
apply ENNReal.mul_lt_top
[GOAL]
case refine'_2.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
ε : ℝ
hε : 0 < ε
⊢ (ENNReal.ofReal ε)⁻¹ ^ ENNReal.toReal 1 ≠ ⊤
[PROOFSTEP]
simpa only [ENNReal.one_toReal, ENNReal.rpow_one, Ne.def, ENNReal.inv_eq_top, ENNReal.ofReal_eq_zero, not_le] using hε
[GOAL]
case refine'_2.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
ε : ℝ
hε : 0 < ε
⊢ snorm f 1 μ ^ ENNReal.toReal 1 ≠ ⊤
[PROOFSTEP]
simpa only [ENNReal.one_toReal, ENNReal.rpow_one] using (memℒp_one_iff_integrable.2 hf).snorm_ne_top
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
K K' : ℝ≥0
f : α → β
g : β → γ
hg : LipschitzWith K g
hg' : AntilipschitzWith K' g
g0 : g 0 = 0
⊢ Integrable (g ∘ f) ↔ Integrable f
[PROOFSTEP]
simp [← memℒp_one_iff_integrable, hg.memℒp_comp_iff_of_antilipschitz hg' g0]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
hf : Integrable f
⊢ Integrable fun x => ↑(Real.toNNReal (f x))
[PROOFSTEP]
refine' ⟨hf.aestronglyMeasurable.aemeasurable.real_toNNReal.coe_nnreal_real.aestronglyMeasurable, _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
hf : Integrable f
⊢ HasFiniteIntegral fun x => ↑(Real.toNNReal (f x))
[PROOFSTEP]
rw [hasFiniteIntegral_iff_norm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
hf : Integrable f
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖↑(Real.toNNReal (f a))‖ ∂μ < ⊤
[PROOFSTEP]
refine' lt_of_le_of_lt _ ((hasFiniteIntegral_iff_norm _).1 hf.hasFiniteIntegral)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
hf : Integrable f
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖↑(Real.toNNReal (f a))‖ ∂μ ≤ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ
[PROOFSTEP]
apply lintegral_mono
[GOAL]
case hfg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
hf : Integrable f
⊢ (fun a => ENNReal.ofReal ‖↑(Real.toNNReal (f a))‖) ≤ fun a => ENNReal.ofReal ‖f a‖
[PROOFSTEP]
intro x
[GOAL]
case hfg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
hf : Integrable f
x : α
⊢ (fun a => ENNReal.ofReal ‖↑(Real.toNNReal (f a))‖) x ≤ (fun a => ENNReal.ofReal ‖f a‖) x
[PROOFSTEP]
simp [ENNReal.ofReal_le_ofReal, abs_le, le_abs_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
⊢ (fun x => ENNReal.ofReal (ENNReal.toReal (f x))) =ᵐ[μ] f
[PROOFSTEP]
filter_upwards [hf]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
⊢ ∀ (a : α), f a < ⊤ → ENNReal.ofReal (ENNReal.toReal (f a)) = f a
[PROOFSTEP]
intro x hx
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
x : α
hx : f x < ⊤
⊢ ENNReal.ofReal (ENNReal.toReal (f x)) = f x
[PROOFSTEP]
simp only [hx.ne, ofReal_toReal, Ne.def, not_false_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
⊢ (fun x => ↑(ENNReal.toNNReal (f x))) =ᵐ[μ] f
[PROOFSTEP]
filter_upwards [hf]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
⊢ ∀ (a : α), f a < ⊤ → ↑(ENNReal.toNNReal (f a)) = f a
[PROOFSTEP]
intro x hx
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
x : α
hx : f x < ⊤
⊢ ↑(ENNReal.toNNReal (f x)) = f x
[PROOFSTEP]
simp only [hx.ne, Ne.def, not_false_iff, coe_toNNReal]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ Integrable g ↔ Integrable fun x => ↑(f x) • g x
[PROOFSTEP]
by_cases H : AEStronglyMeasurable (fun x : α => (f x : ℝ) • g x) μ
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ Integrable g ↔ Integrable fun x => ↑(f x) • g x
[PROOFSTEP]
simp only [Integrable, aestronglyMeasurable_withDensity_iff hf, HasFiniteIntegral, H, true_and_iff]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ (∫⁻ (a : α), ↑‖g a‖₊ ∂Measure.withDensity μ fun x => ↑(f x)) < ⊤ ↔ ∫⁻ (a : α), ↑‖↑(f a) • g a‖₊ ∂μ < ⊤
[PROOFSTEP]
rw [lintegral_withDensity_eq_lintegral_mul₀' hf.coe_nnreal_ennreal.aemeasurable]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ ∫⁻ (a : α), ((fun x => ↑(f x)) * fun a => ↑‖g a‖₊) a ∂μ < ⊤ ↔ ∫⁻ (a : α), ↑‖↑(f a) • g a‖₊ ∂μ < ⊤
[PROOFSTEP]
rw [iff_iff_eq]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ (∫⁻ (a : α), ((fun x => ↑(f x)) * fun a => ↑‖g a‖₊) a ∂μ < ⊤) = (∫⁻ (a : α), ↑‖↑(f a) • g a‖₊ ∂μ < ⊤)
[PROOFSTEP]
congr
[GOAL]
case pos.e_a.e_f
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ (fun a => ((fun x => ↑(f x)) * fun a => ↑‖g a‖₊) a) = fun a => ↑‖↑(f a) • g a‖₊
[PROOFSTEP]
ext1 x
[GOAL]
case pos.e_a.e_f.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
x : α
⊢ ((fun x => ↑(f x)) * fun a => ↑‖g a‖₊) x = ↑‖↑(f x) • g x‖₊
[PROOFSTEP]
simp only [nnnorm_smul, NNReal.nnnorm_eq, coe_mul, Pi.mul_apply]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ AEMeasurable fun a => ↑‖g a‖₊
[PROOFSTEP]
rw [aemeasurable_withDensity_ennreal_iff hf]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ AEMeasurable fun x => ↑(f x) * ↑‖g x‖₊
[PROOFSTEP]
convert H.ennnorm using 1
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ (fun x => ↑(f x) * ↑‖g x‖₊) = fun a => ↑‖↑(f a) • g a‖₊
[PROOFSTEP]
ext1 x
[GOAL]
case h.e'_5.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
x : α
⊢ ↑(f x) * ↑‖g x‖₊ = ↑‖↑(f x) • g x‖₊
[PROOFSTEP]
simp only [nnnorm_smul, NNReal.nnnorm_eq, coe_mul]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : ¬AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ Integrable g ↔ Integrable fun x => ↑(f x) • g x
[PROOFSTEP]
simp only [Integrable, aestronglyMeasurable_withDensity_iff hf, H, false_and_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → E
⊢ Integrable g ↔ Integrable fun x => ENNReal.toReal (f x) • g x
[PROOFSTEP]
rw [← withDensity_congr_ae (coe_toNNReal_ae_eq hflt), integrable_withDensity_iff_integrable_smul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → E
⊢ (Integrable fun x => ENNReal.toNNReal (f x) • g x) ↔ Integrable fun x => ENNReal.toReal (f x) • g x
[PROOFSTEP]
rfl
[GOAL]
case hf
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → E
⊢ Measurable fun x => ENNReal.toNNReal (f x)
[PROOFSTEP]
exact hf.ennreal_toNNReal
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
⊢ Integrable g ↔ Integrable g
[PROOFSTEP]
suffices (fun x => (f x : ℝ≥0∞)) =ᵐ[μ] (fun x => (hf.mk f x : ℝ≥0)) by rw [withDensity_congr_ae this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
this : (fun x => ↑(f x)) =ᵐ[μ] fun x => ↑(AEMeasurable.mk f hf x)
⊢ Integrable g ↔ Integrable g
[PROOFSTEP]
rw [withDensity_congr_ae this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
⊢ (fun x => ↑(f x)) =ᵐ[μ] fun x => ↑(AEMeasurable.mk f hf x)
[PROOFSTEP]
filter_upwards [hf.ae_eq_mk] with x hx
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ ↑(f x) = ↑(AEMeasurable.mk f hf x)
[PROOFSTEP]
simp [hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
⊢ (Integrable fun x => ↑(AEMeasurable.mk f hf x) • g x) ↔ Integrable fun x => ↑(f x) • g x
[PROOFSTEP]
apply integrable_congr
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
⊢ (fun x => ↑(AEMeasurable.mk f hf x) • g x) =ᵐ[μ] fun x => ↑(f x) • g x
[PROOFSTEP]
filter_upwards [hf.ae_eq_mk] with x hx
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ ↑(AEMeasurable.mk f hf x) • g x = ↑(f x) • g x
[PROOFSTEP]
simp [hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ
⊢ Integrable g ↔ Integrable fun x => g x * ENNReal.toReal (f x)
[PROOFSTEP]
have : (fun x => g x * (f x).toReal) = fun x => (f x).toReal • g x := by simp [mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ
⊢ (fun x => g x * ENNReal.toReal (f x)) = fun x => ENNReal.toReal (f x) • g x
[PROOFSTEP]
simp [mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ
this : (fun x => g x * ENNReal.toReal (f x)) = fun x => ENNReal.toReal (f x) • g x
⊢ Integrable g ↔ Integrable fun x => g x * ENNReal.toReal (f x)
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ
this : (fun x => g x * ENNReal.toReal (f x)) = fun x => ENNReal.toReal (f x) • g x
⊢ Integrable g ↔ Integrable fun x => ENNReal.toReal (f x) • g x
[PROOFSTEP]
exact integrable_withDensity_iff_integrable_smul' hf hflt
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
⊢ ∀ (x y : { x // x ∈ Lp E 1 }),
    (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) (x + y) =
      (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) x +
        (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) y
[PROOFSTEP]
intro u v
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u v : { x // x ∈ Lp E 1 }
⊢ (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) (u + v) =
    (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) u +
      (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) v
[PROOFSTEP]
ext1
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u v : { x // x ∈ Lp E 1 }
⊢ ↑↑((fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) (u + v)) =ᵐ[μ]
    ↑↑((fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) u +
          (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) v)
[PROOFSTEP]
filter_upwards [(memℒ1_smul_of_L1_withDensity f_meas u).coeFn_toLp, (memℒ1_smul_of_L1_withDensity f_meas v).coeFn_toLp,
  (memℒ1_smul_of_L1_withDensity f_meas (u + v)).coeFn_toLp,
  Lp.coeFn_add ((memℒ1_smul_of_L1_withDensity f_meas u).toLp _) ((memℒ1_smul_of_L1_withDensity f_meas v).toLp _),
  (ae_withDensity_iff f_meas.coe_nnreal_ennreal).1 (Lp.coeFn_add u v)]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u v : { x // x ∈ Lp E 1 }
⊢ ∀ (a : α),
    ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) a = f a • ↑↑u a →
      ↑↑(Memℒp.toLp (fun x => f x • ↑↑v x) (_ : Memℒp (fun x => f x • ↑↑v x) 1)) a = f a • ↑↑v a →
        ↑↑(Memℒp.toLp (fun x => f x • ↑↑(u + v) x) (_ : Memℒp (fun x => f x • ↑↑(u + v) x) 1)) a = f a • ↑↑(u + v) a →
          ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1) +
                      Memℒp.toLp (fun x => f x • ↑↑v x) (_ : Memℒp (fun x => f x • ↑↑v x) 1))
                a =
              (↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) +
                  ↑↑(Memℒp.toLp (fun x => f x • ↑↑v x) (_ : Memℒp (fun x => f x • ↑↑v x) 1)))
                a →
            (↑(f a) ≠ 0 → ↑↑(u + v) a = (↑↑u + ↑↑v) a) →
              ↑↑(Memℒp.toLp (fun x => f x • ↑↑(u + v) x) (_ : Memℒp (fun x => f x • ↑↑(u + v) x) 1)) a =
                ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1) +
                        Memℒp.toLp (fun x => f x • ↑↑v x) (_ : Memℒp (fun x => f x • ↑↑v x) 1))
                  a
[PROOFSTEP]
intro x hu hv huv h' h''
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u v : { x // x ∈ Lp E 1 }
x : α
hu : ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) x = f x • ↑↑u x
hv : ↑↑(Memℒp.toLp (fun x => f x • ↑↑v x) (_ : Memℒp (fun x => f x • ↑↑v x) 1)) x = f x • ↑↑v x
huv : ↑↑(Memℒp.toLp (fun x => f x • ↑↑(u + v) x) (_ : Memℒp (fun x => f x • ↑↑(u + v) x) 1)) x = f x • ↑↑(u + v) x
h' :
  ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1) +
            Memℒp.toLp (fun x => f x • ↑↑v x) (_ : Memℒp (fun x => f x • ↑↑v x) 1))
      x =
    (↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) +
        ↑↑(Memℒp.toLp (fun x => f x • ↑↑v x) (_ : Memℒp (fun x => f x • ↑↑v x) 1)))
      x
h'' : ↑(f x) ≠ 0 → ↑↑(u + v) x = (↑↑u + ↑↑v) x
⊢ ↑↑(Memℒp.toLp (fun x => f x • ↑↑(u + v) x) (_ : Memℒp (fun x => f x • ↑↑(u + v) x) 1)) x =
    ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1) +
            Memℒp.toLp (fun x => f x • ↑↑v x) (_ : Memℒp (fun x => f x • ↑↑v x) 1))
      x
[PROOFSTEP]
rw [huv, h', Pi.add_apply, hu, hv]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u v : { x // x ∈ Lp E 1 }
x : α
hu : ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) x = f x • ↑↑u x
hv : ↑↑(Memℒp.toLp (fun x => f x • ↑↑v x) (_ : Memℒp (fun x => f x • ↑↑v x) 1)) x = f x • ↑↑v x
huv : ↑↑(Memℒp.toLp (fun x => f x • ↑↑(u + v) x) (_ : Memℒp (fun x => f x • ↑↑(u + v) x) 1)) x = f x • ↑↑(u + v) x
h' :
  ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1) +
            Memℒp.toLp (fun x => f x • ↑↑v x) (_ : Memℒp (fun x => f x • ↑↑v x) 1))
      x =
    (↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) +
        ↑↑(Memℒp.toLp (fun x => f x • ↑↑v x) (_ : Memℒp (fun x => f x • ↑↑v x) 1)))
      x
h'' : ↑(f x) ≠ 0 → ↑↑(u + v) x = (↑↑u + ↑↑v) x
⊢ f x • ↑↑(u + v) x = f x • ↑↑u x + f x • ↑↑v x
[PROOFSTEP]
rcases eq_or_ne (f x) 0 with (hx | hx)
[GOAL]
case h.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u v : { x // x ∈ Lp E 1 }
x : α
hu : ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) x = f x • ↑↑u x
hv : ↑↑(Memℒp.toLp (fun x => f x • ↑↑v x) (_ : Memℒp (fun x => f x • ↑↑v x) 1)) x = f x • ↑↑v x
huv : ↑↑(Memℒp.toLp (fun x => f x • ↑↑(u + v) x) (_ : Memℒp (fun x => f x • ↑↑(u + v) x) 1)) x = f x • ↑↑(u + v) x
h' :
  ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1) +
            Memℒp.toLp (fun x => f x • ↑↑v x) (_ : Memℒp (fun x => f x • ↑↑v x) 1))
      x =
    (↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) +
        ↑↑(Memℒp.toLp (fun x => f x • ↑↑v x) (_ : Memℒp (fun x => f x • ↑↑v x) 1)))
      x
h'' : ↑(f x) ≠ 0 → ↑↑(u + v) x = (↑↑u + ↑↑v) x
hx : f x = 0
⊢ f x • ↑↑(u + v) x = f x • ↑↑u x + f x • ↑↑v x
[PROOFSTEP]
simp only [hx, zero_smul, add_zero]
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u v : { x // x ∈ Lp E 1 }
x : α
hu : ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) x = f x • ↑↑u x
hv : ↑↑(Memℒp.toLp (fun x => f x • ↑↑v x) (_ : Memℒp (fun x => f x • ↑↑v x) 1)) x = f x • ↑↑v x
huv : ↑↑(Memℒp.toLp (fun x => f x • ↑↑(u + v) x) (_ : Memℒp (fun x => f x • ↑↑(u + v) x) 1)) x = f x • ↑↑(u + v) x
h' :
  ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1) +
            Memℒp.toLp (fun x => f x • ↑↑v x) (_ : Memℒp (fun x => f x • ↑↑v x) 1))
      x =
    (↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) +
        ↑↑(Memℒp.toLp (fun x => f x • ↑↑v x) (_ : Memℒp (fun x => f x • ↑↑v x) 1)))
      x
h'' : ↑(f x) ≠ 0 → ↑↑(u + v) x = (↑↑u + ↑↑v) x
hx : f x ≠ 0
⊢ f x • ↑↑(u + v) x = f x • ↑↑u x + f x • ↑↑v x
[PROOFSTEP]
rw [h'' _, Pi.add_apply, smul_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u v : { x // x ∈ Lp E 1 }
x : α
hu : ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) x = f x • ↑↑u x
hv : ↑↑(Memℒp.toLp (fun x => f x • ↑↑v x) (_ : Memℒp (fun x => f x • ↑↑v x) 1)) x = f x • ↑↑v x
huv : ↑↑(Memℒp.toLp (fun x => f x • ↑↑(u + v) x) (_ : Memℒp (fun x => f x • ↑↑(u + v) x) 1)) x = f x • ↑↑(u + v) x
h' :
  ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1) +
            Memℒp.toLp (fun x => f x • ↑↑v x) (_ : Memℒp (fun x => f x • ↑↑v x) 1))
      x =
    (↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) +
        ↑↑(Memℒp.toLp (fun x => f x • ↑↑v x) (_ : Memℒp (fun x => f x • ↑↑v x) 1)))
      x
h'' : ↑(f x) ≠ 0 → ↑↑(u + v) x = (↑↑u + ↑↑v) x
hx : f x ≠ 0
⊢ ↑(f x) ≠ 0
[PROOFSTEP]
simpa only [Ne.def, ENNReal.coe_eq_zero] using hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
⊢ ∀ (r : ℝ) (x : { x // x ∈ Lp E 1 }),
    AddHom.toFun
        { toFun := fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1),
          map_add' :=
            (_ :
              ∀ (u v : { x // x ∈ Lp E 1 }),
                (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) (u + v) =
                  (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) u +
                    (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) v) }
        (r • x) =
      ↑(RingHom.id ℝ) r •
        AddHom.toFun
          { toFun := fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1),
            map_add' :=
              (_ :
                ∀ (u v : { x // x ∈ Lp E 1 }),
                  (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) (u + v) =
                    (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) u +
                      (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) v) }
          x
[PROOFSTEP]
intro r u
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
r : ℝ
u : { x // x ∈ Lp E 1 }
⊢ AddHom.toFun
      { toFun := fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1),
        map_add' :=
          (_ :
            ∀ (u v : { x // x ∈ Lp E 1 }),
              (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) (u + v) =
                (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) u +
                  (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) v) }
      (r • u) =
    ↑(RingHom.id ℝ) r •
      AddHom.toFun
        { toFun := fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1),
          map_add' :=
            (_ :
              ∀ (u v : { x // x ∈ Lp E 1 }),
                (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) (u + v) =
                  (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) u +
                    (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) v) }
        u
[PROOFSTEP]
ext1
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
r : ℝ
u : { x // x ∈ Lp E 1 }
⊢ ↑↑(AddHom.toFun
          { toFun := fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1),
            map_add' :=
              (_ :
                ∀ (u v : { x // x ∈ Lp E 1 }),
                  (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) (u + v) =
                    (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) u +
                      (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) v) }
          (r • u)) =ᵐ[μ]
    ↑↑(↑(RingHom.id ℝ) r •
          AddHom.toFun
            { toFun := fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1),
              map_add' :=
                (_ :
                  ∀ (u v : { x // x ∈ Lp E 1 }),
                    (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) (u + v) =
                      (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) u +
                        (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) v) }
            u)
[PROOFSTEP]
filter_upwards [(ae_withDensity_iff f_meas.coe_nnreal_ennreal).1 (Lp.coeFn_smul r u),
  (memℒ1_smul_of_L1_withDensity f_meas (r • u)).coeFn_toLp,
  Lp.coeFn_smul r ((memℒ1_smul_of_L1_withDensity f_meas u).toLp _), (memℒ1_smul_of_L1_withDensity f_meas u).coeFn_toLp]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
r : ℝ
u : { x // x ∈ Lp E 1 }
⊢ ∀ (a : α),
    (↑(f a) ≠ 0 → ↑↑(r • u) a = (r • ↑↑u) a) →
      ↑↑(Memℒp.toLp (fun x => f x • ↑↑(r • u) x) (_ : Memℒp (fun x => f x • ↑↑(r • u) x) 1)) a = f a • ↑↑(r • u) a →
        ↑↑(r • Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) a =
            (r • ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1))) a →
          ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) a = f a • ↑↑u a →
            ↑↑(Memℒp.toLp (fun x => f x • ↑↑(r • u) x) (_ : Memℒp (fun x => f x • ↑↑(r • u) x) 1)) a =
              ↑↑(↑(RingHom.id ℝ) r • Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) a
[PROOFSTEP]
intro x h h' h'' h'''
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
r : ℝ
u : { x // x ∈ Lp E 1 }
x : α
h : ↑(f x) ≠ 0 → ↑↑(r • u) x = (r • ↑↑u) x
h' : ↑↑(Memℒp.toLp (fun x => f x • ↑↑(r • u) x) (_ : Memℒp (fun x => f x • ↑↑(r • u) x) 1)) x = f x • ↑↑(r • u) x
h'' :
  ↑↑(r • Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) x =
    (r • ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1))) x
h''' : ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) x = f x • ↑↑u x
⊢ ↑↑(Memℒp.toLp (fun x => f x • ↑↑(r • u) x) (_ : Memℒp (fun x => f x • ↑↑(r • u) x) 1)) x =
    ↑↑(↑(RingHom.id ℝ) r • Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) x
[PROOFSTEP]
rw [RingHom.id_apply, h', h'', Pi.smul_apply, h''']
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
r : ℝ
u : { x // x ∈ Lp E 1 }
x : α
h : ↑(f x) ≠ 0 → ↑↑(r • u) x = (r • ↑↑u) x
h' : ↑↑(Memℒp.toLp (fun x => f x • ↑↑(r • u) x) (_ : Memℒp (fun x => f x • ↑↑(r • u) x) 1)) x = f x • ↑↑(r • u) x
h'' :
  ↑↑(r • Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) x =
    (r • ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1))) x
h''' : ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) x = f x • ↑↑u x
⊢ f x • ↑↑(r • u) x = r • f x • ↑↑u x
[PROOFSTEP]
rcases eq_or_ne (f x) 0 with (hx | hx)
[GOAL]
case h.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
r : ℝ
u : { x // x ∈ Lp E 1 }
x : α
h : ↑(f x) ≠ 0 → ↑↑(r • u) x = (r • ↑↑u) x
h' : ↑↑(Memℒp.toLp (fun x => f x • ↑↑(r • u) x) (_ : Memℒp (fun x => f x • ↑↑(r • u) x) 1)) x = f x • ↑↑(r • u) x
h'' :
  ↑↑(r • Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) x =
    (r • ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1))) x
h''' : ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) x = f x • ↑↑u x
hx : f x = 0
⊢ f x • ↑↑(r • u) x = r • f x • ↑↑u x
[PROOFSTEP]
simp only [hx, zero_smul, smul_zero]
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
r : ℝ
u : { x // x ∈ Lp E 1 }
x : α
h : ↑(f x) ≠ 0 → ↑↑(r • u) x = (r • ↑↑u) x
h' : ↑↑(Memℒp.toLp (fun x => f x • ↑↑(r • u) x) (_ : Memℒp (fun x => f x • ↑↑(r • u) x) 1)) x = f x • ↑↑(r • u) x
h'' :
  ↑↑(r • Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) x =
    (r • ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1))) x
h''' : ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) x = f x • ↑↑u x
hx : f x ≠ 0
⊢ f x • ↑↑(r • u) x = r • f x • ↑↑u x
[PROOFSTEP]
rw [h _, smul_comm, Pi.smul_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
r : ℝ
u : { x // x ∈ Lp E 1 }
x : α
h : ↑(f x) ≠ 0 → ↑↑(r • u) x = (r • ↑↑u) x
h' : ↑↑(Memℒp.toLp (fun x => f x • ↑↑(r • u) x) (_ : Memℒp (fun x => f x • ↑↑(r • u) x) 1)) x = f x • ↑↑(r • u) x
h'' :
  ↑↑(r • Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) x =
    (r • ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1))) x
h''' : ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) x = f x • ↑↑u x
hx : f x ≠ 0
⊢ ↑(f x) ≠ 0
[PROOFSTEP]
simpa only [Ne.def, ENNReal.coe_eq_zero] using hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
⊢ ∀ (x : { x // x ∈ Lp E 1 }),
    ‖↑{
              toAddHom :=
                { toFun := fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1),
                  map_add' :=
                    (_ :
                      ∀ (u v : { x // x ∈ Lp E 1 }),
                        (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) (u + v) =
                          (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) u +
                            (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) v) },
              map_smul' :=
                (_ :
                  ∀ (r : ℝ) (u : { x // x ∈ Lp E 1 }),
                    AddHom.toFun
                        { toFun := fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1),
                          map_add' :=
                            (_ :
                              ∀ (u v : { x // x ∈ Lp E 1 }),
                                (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1))
                                    (u + v) =
                                  (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) u +
                                    (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1))
                                      v) }
                        (r • u) =
                      ↑(RingHom.id ℝ) r •
                        AddHom.toFun
                          { toFun := fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1),
                            map_add' :=
                              (_ :
                                ∀ (u v : { x // x ∈ Lp E 1 }),
                                  (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1))
                                      (u + v) =
                                    (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1))
                                        u +
                                      (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1))
                                        v) }
                          u) }
          x‖ =
      ‖x‖
[PROOFSTEP]
intro u
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : { x // x ∈ Lp E 1 }
⊢ ‖↑{
            toAddHom :=
              { toFun := fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1),
                map_add' :=
                  (_ :
                    ∀ (u v : { x // x ∈ Lp E 1 }),
                      (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) (u + v) =
                        (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) u +
                          (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) v) },
            map_smul' :=
              (_ :
                ∀ (r : ℝ) (u : { x // x ∈ Lp E 1 }),
                  AddHom.toFun
                      { toFun := fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1),
                        map_add' :=
                          (_ :
                            ∀ (u v : { x // x ∈ Lp E 1 }),
                              (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1))
                                  (u + v) =
                                (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) u +
                                  (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) v) }
                      (r • u) =
                    ↑(RingHom.id ℝ) r •
                      AddHom.toFun
                        { toFun := fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1),
                          map_add' :=
                            (_ :
                              ∀ (u v : { x // x ∈ Lp E 1 }),
                                (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1))
                                    (u + v) =
                                  (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) u +
                                    (fun u => Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1))
                                      v) }
                        u) }
        u‖ =
    ‖u‖
[PROOFSTEP]
simp only [snorm, LinearMap.coe_mk, AddHom.coe_mk (M := Lp E 1 (μ.withDensity fun x => f x)) (N := Lp E 1 μ),
  Lp.norm_toLp, one_ne_zero, ENNReal.one_ne_top, ENNReal.one_toReal, if_false, snorm', ENNReal.rpow_one, _root_.div_one,
  Lp.norm_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : { x // x ∈ Lp E 1 }
⊢ ENNReal.toReal (∫⁻ (a : α), ↑‖↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) a‖₊ ∂μ) =
    ENNReal.toReal (∫⁻ (a : α), ↑‖↑↑u a‖₊ ∂Measure.withDensity μ fun x => ↑(f x))
[PROOFSTEP]
rw [lintegral_withDensity_eq_lintegral_mul_non_measurable _ f_meas.coe_nnreal_ennreal
    (Filter.eventually_of_forall fun x => ENNReal.coe_lt_top)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : { x // x ∈ Lp E 1 }
⊢ ENNReal.toReal (∫⁻ (a : α), ↑‖↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) a‖₊ ∂μ) =
    ENNReal.toReal (∫⁻ (a : α), ((fun x => ↑(f x)) * fun a => ↑‖↑↑u a‖₊) a ∂μ)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : { x // x ∈ Lp E 1 }
⊢ ∫⁻ (a : α), ↑‖↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) a‖₊ ∂μ =
    ∫⁻ (a : α), ((fun x => ↑(f x)) * fun a => ↑‖↑↑u a‖₊) a ∂μ
[PROOFSTEP]
apply lintegral_congr_ae
[GOAL]
case e_a.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : { x // x ∈ Lp E 1 }
⊢ (fun a => ↑‖↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) a‖₊) =ᵐ[μ] fun a =>
    ((fun x => ↑(f x)) * fun a => ↑‖↑↑u a‖₊) a
[PROOFSTEP]
filter_upwards [(memℒ1_smul_of_L1_withDensity f_meas u).coeFn_toLp] with x hx
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : { x // x ∈ Lp E 1 }
x : α
hx : ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) x = f x • ↑↑u x
⊢ ↑‖↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) x‖₊ =
    ((fun x => ↑(f x)) * fun a => ↑‖↑↑u a‖₊) x
[PROOFSTEP]
rw [hx, Pi.mul_apply]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : { x // x ∈ Lp E 1 }
x : α
hx : ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) x = f x • ↑↑u x
⊢ ↑‖f x • ↑↑u x‖₊ = ↑(f x) * ↑‖↑↑u x‖₊
[PROOFSTEP]
change (‖(f x : ℝ) • u x‖₊ : ℝ≥0∞) = (f x : ℝ≥0∞) * (‖u x‖₊ : ℝ≥0∞)
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : { x // x ∈ Lp E 1 }
x : α
hx : ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) x = f x • ↑↑u x
⊢ ↑‖↑(f x) • ↑↑u x‖₊ = ↑(f x) * ↑‖↑↑u x‖₊
[PROOFSTEP]
simp only [nnnorm_smul, NNReal.nnnorm_eq, ENNReal.coe_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hfm : AEMeasurable f
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
⊢ Memℒp (fun x => ENNReal.toReal (f x)) 1
[PROOFSTEP]
rw [Memℒp, snorm_one_eq_lintegral_nnnorm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hfm : AEMeasurable f
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
⊢ AEStronglyMeasurable (fun x => ENNReal.toReal (f x)) μ ∧ ∫⁻ (x : α), ↑‖ENNReal.toReal (f x)‖₊ ∂μ < ⊤
[PROOFSTEP]
exact ⟨(AEMeasurable.ennreal_toReal hfm).aestronglyMeasurable, hasFiniteIntegral_toReal_of_lintegral_ne_top hfi⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → β
φ : α → 𝕜
hf : Integrable f
hφ : Memℒp φ ⊤
⊢ Integrable (φ • f)
[PROOFSTEP]
rw [← memℒp_one_iff_integrable] at hf ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → β
φ : α → 𝕜
hf : Memℒp f 1
hφ : Memℒp φ ⊤
⊢ Memℒp (φ • f) 1
[PROOFSTEP]
exact Memℒp.smul_of_top_right hf hφ
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → β
φ : α → 𝕜
hφ : Integrable φ
hf : Memℒp f ⊤
⊢ Integrable (φ • f)
[PROOFSTEP]
rw [← memℒp_one_iff_integrable] at hφ ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → β
φ : α → 𝕜
hφ : Memℒp φ 1
hf : Memℒp f ⊤
⊢ Memℒp (φ • f) 1
[PROOFSTEP]
exact Memℒp.smul_of_top_left hf hφ
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁶ : MeasurableSpace δ
inst✝⁵ : NormedAddCommGroup β
inst✝⁴ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
⊢ (Integrable fun x => f x • c) ↔ Integrable f
[PROOFSTEP]
simp_rw [Integrable, aestronglyMeasurable_smul_const_iff (f := f) hc, and_congr_right_iff, HasFiniteIntegral,
  nnnorm_smul, ENNReal.coe_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁶ : MeasurableSpace δ
inst✝⁵ : NormedAddCommGroup β
inst✝⁴ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
⊢ AEStronglyMeasurable f μ → (∫⁻ (a : α), ↑‖f a‖₊ * ↑‖c‖₊ ∂μ < ⊤ ↔ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤)
[PROOFSTEP]
intro _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁶ : MeasurableSpace δ
inst✝⁵ : NormedAddCommGroup β
inst✝⁴ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
a✝ : AEStronglyMeasurable f μ
⊢ ∫⁻ (a : α), ↑‖f a‖₊ * ↑‖c‖₊ ∂μ < ⊤ ↔ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤
[PROOFSTEP]
rw [lintegral_mul_const' _ _ ENNReal.coe_ne_top, ENNReal.mul_lt_top_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁶ : MeasurableSpace δ
inst✝⁵ : NormedAddCommGroup β
inst✝⁴ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
a✝ : AEStronglyMeasurable f μ
⊢ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤ ∧ ↑‖c‖₊ < ⊤ ∨ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ = 0 ∨ ↑‖c‖₊ = 0 ↔ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤
[PROOFSTEP]
have : ∀ x : ℝ≥0∞, x = 0 → x < ∞ := by simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁶ : MeasurableSpace δ
inst✝⁵ : NormedAddCommGroup β
inst✝⁴ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
a✝ : AEStronglyMeasurable f μ
⊢ ∀ (x : ℝ≥0∞), x = 0 → x < ⊤
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁶ : MeasurableSpace δ
inst✝⁵ : NormedAddCommGroup β
inst✝⁴ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
a✝ : AEStronglyMeasurable f μ
this : ∀ (x : ℝ≥0∞), x = 0 → x < ⊤
⊢ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤ ∧ ↑‖c‖₊ < ⊤ ∨ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ = 0 ∨ ↑‖c‖₊ = 0 ↔ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤
[PROOFSTEP]
simp [hc, or_iff_left_of_imp (this _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝ : NormedRing 𝕜
f✝ f g : α → 𝕜
c : ℝ
hg : Integrable g
hf : AEStronglyMeasurable f μ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
⊢ Integrable fun x => f x * g x
[PROOFSTEP]
refine' Integrable.mono' (hg.norm.smul c) (hf.mul hg.1) _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝ : NormedRing 𝕜
f✝ f g : α → 𝕜
c : ℝ
hg : Integrable g
hf : AEStronglyMeasurable f μ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
⊢ ∀ᵐ (a : α) ∂μ, ‖f a * g a‖ ≤ (c • fun a => ‖g a‖) a
[PROOFSTEP]
filter_upwards [hf_bound] with x hx
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝ : NormedRing 𝕜
f✝ f g : α → 𝕜
c : ℝ
hg : Integrable g
hf : AEStronglyMeasurable f μ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
x : α
hx : ‖f x‖ ≤ c
⊢ ‖f x * g x‖ ≤ (c • fun a => ‖g a‖) x
[PROOFSTEP]
rw [Pi.smul_apply, smul_eq_mul]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝ : NormedRing 𝕜
f✝ f g : α → 𝕜
c : ℝ
hg : Integrable g
hf : AEStronglyMeasurable f μ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
x : α
hx : ‖f x‖ ≤ c
⊢ ‖f x * g x‖ ≤ c * ‖g x‖
[PROOFSTEP]
exact (norm_mul_le _ _).trans (mul_le_mul_of_nonneg_right hx (norm_nonneg _))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝ : NormedDivisionRing 𝕜
f✝ f : α → 𝕜
h : Integrable f
c : 𝕜
⊢ Integrable fun x => f x / c
[PROOFSTEP]
simp_rw [div_eq_mul_inv, h.mul_const]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝ : IsROrC 𝕜
f✝ : α → 𝕜
f : α → ℝ
hf : Integrable f
⊢ Integrable fun x => ↑(f x)
[PROOFSTEP]
rw [← memℒp_one_iff_integrable] at hf ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝ : IsROrC 𝕜
f✝ : α → 𝕜
f : α → ℝ
hf : Memℒp f 1
⊢ Memℒp (fun x => ↑(f x)) 1
[PROOFSTEP]
exact hf.ofReal
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝ : IsROrC 𝕜
f : α → 𝕜
⊢ ((Integrable fun x => ↑IsROrC.re (f x)) ∧ Integrable fun x => ↑IsROrC.im (f x)) ↔ Integrable f
[PROOFSTEP]
simp_rw [← memℒp_one_iff_integrable]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝ : IsROrC 𝕜
f : α → 𝕜
⊢ Memℒp (fun x => ↑IsROrC.re (f x)) 1 ∧ Memℒp (fun x => ↑IsROrC.im (f x)) 1 ↔ Memℒp f 1
[PROOFSTEP]
exact memℒp_re_im_iff
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝ : IsROrC 𝕜
f : α → 𝕜
hf : Integrable f
⊢ Integrable fun x => ↑IsROrC.re (f x)
[PROOFSTEP]
rw [← memℒp_one_iff_integrable] at hf ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝ : IsROrC 𝕜
f : α → 𝕜
hf : Memℒp f 1
⊢ Memℒp (fun x => ↑IsROrC.re (f x)) 1
[PROOFSTEP]
exact hf.re
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝ : IsROrC 𝕜
f : α → 𝕜
hf : Integrable f
⊢ Integrable fun x => ↑IsROrC.im (f x)
[PROOFSTEP]
rw [← memℒp_one_iff_integrable] at hf ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_5
inst✝ : IsROrC 𝕜
f : α → 𝕜
hf : Memℒp f 1
⊢ Memℒp (fun x => ↑IsROrC.im (f x)) 1
[PROOFSTEP]
exact hf.im
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
H : Type u_5
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f
hf : StronglyMeasurable f
⊢ Integrable f
[PROOFSTEP]
refine' ⟨hf.aestronglyMeasurable, _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
H : Type u_5
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f
hf : StronglyMeasurable f
⊢ HasFiniteIntegral f
[PROOFSTEP]
rw [HasFiniteIntegral, lintegral_trim hm _]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
H : Type u_5
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f
hf : StronglyMeasurable f
⊢ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ' < ⊤
[PROOFSTEP]
exact hf_int.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
H : Type u_5
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f
hf : StronglyMeasurable f
⊢ Measurable fun a => ↑‖f a‖₊
[PROOFSTEP]
exact @StronglyMeasurable.ennnorm _ m _ _ f hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
H : Type u_5
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f
⊢ Integrable f
[PROOFSTEP]
obtain ⟨hf_meas_ae, hf⟩ := hf_int
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
H : Type u_5
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_meas_ae : AEStronglyMeasurable f (Measure.trim μ' hm)
hf : HasFiniteIntegral f
⊢ Integrable f
[PROOFSTEP]
refine' ⟨aestronglyMeasurable_of_aestronglyMeasurable_trim hm hf_meas_ae, _⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
H : Type u_5
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_meas_ae : AEStronglyMeasurable f (Measure.trim μ' hm)
hf : HasFiniteIntegral f
⊢ HasFiniteIntegral f
[PROOFSTEP]
rw [HasFiniteIntegral] at hf ⊢
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
H : Type u_5
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_meas_ae : AEStronglyMeasurable f (Measure.trim μ' hm)
hf : ∫⁻ (a : α), ↑‖f a‖₊ ∂Measure.trim μ' hm < ⊤
⊢ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ' < ⊤
[PROOFSTEP]
rwa [lintegral_trim_ae hm _] at hf 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
H : Type u_5
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_meas_ae : AEStronglyMeasurable f (Measure.trim μ' hm)
hf : ∫⁻ (a : α), ↑‖f a‖₊ ∂Measure.trim μ' hm < ⊤
⊢ AEMeasurable fun a => ↑‖f a‖₊
[PROOFSTEP]
exact AEStronglyMeasurable.ennnorm hf_meas_ae
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_5
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite μ
C : ℝ≥0∞
hC : C < ⊤
f : α → E
hf_meas : AEStronglyMeasurable f μ
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → ∫⁻ (x : α) in s, ↑‖f x‖₊ ∂μ ≤ C
⊢ SigmaFinite (Measure.trim μ (_ : m ≤ m))
[PROOFSTEP]
rwa [@trim_eq_self _ m]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : AEStronglyMeasurable f μ
⊢ Integrable (mk f hf) ↔ MeasureTheory.Integrable f
[PROOFSTEP]
simp [Integrable]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : AEStronglyMeasurable f μ
⊢ MeasureTheory.Integrable ↑(mk f hf) ↔ MeasureTheory.Integrable f
[PROOFSTEP]
apply integrable_congr
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : AEStronglyMeasurable f μ
⊢ ↑(mk f hf) =ᵐ[μ] f
[PROOFSTEP]
exact coeFn_mk f hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α →ₘ[μ] β
⊢ MeasureTheory.Integrable ↑f ↔ Integrable f
[PROOFSTEP]
rw [← integrable_mk, mk_coeFn]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α →ₘ[μ] β
⊢ Integrable f ↔ f ∈ Lp β 1
[PROOFSTEP]
rw [← integrable_coeFn, ← memℒp_one_iff_integrable, Lp.mem_Lp_iff_memℒp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : α →ₘ[μ] β
⊢ Integrable f → Integrable g → Integrable (f + g)
[PROOFSTEP]
refine' induction_on₂ f g fun f hf g hg hfi hgi => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f✝ g✝ : α →ₘ[μ] β
f : α → β
hf : AEStronglyMeasurable f μ
g : α → β
hg : AEStronglyMeasurable g μ
hfi : Integrable (mk f hf)
hgi : Integrable (mk g hg)
⊢ Integrable (mk f hf + mk g hg)
[PROOFSTEP]
simp only [integrable_mk, mk_add_mk] at hfi hgi ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f✝ g✝ : α →ₘ[μ] β
f : α → β
hf : AEStronglyMeasurable f μ
g : α → β
hg : AEStronglyMeasurable g μ
hfi : MeasureTheory.Integrable f
hgi : MeasureTheory.Integrable g
⊢ MeasureTheory.Integrable (f + g)
[PROOFSTEP]
exact hfi.add hgi
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : { x // x ∈ Lp β 1 }
⊢ Integrable ↑↑f
[PROOFSTEP]
rw [← memℒp_one_iff_integrable]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : { x // x ∈ Lp β 1 }
⊢ Memℒp (↑↑f) 1
[PROOFSTEP]
exact Lp.memℒp f
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ edist f g = ∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ
[PROOFSTEP]
simp [Lp.edist_def, snorm, snorm']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ ∫⁻ (a : α), ↑‖↑↑f a - ↑↑g a‖₊ ∂μ = ∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ
[PROOFSTEP]
simp [edist_eq_coe_nnnorm_sub]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ dist f g = ENNReal.toReal (∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ)
[PROOFSTEP]
simp [Lp.dist_def, snorm, snorm']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ ENNReal.toReal (∫⁻ (a : α), ↑‖↑↑f a - ↑↑g a‖₊ ∂μ) = ENNReal.toReal (∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ)
[PROOFSTEP]
simp [edist_eq_coe_nnnorm_sub]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : { x // x ∈ Lp β 1 }
⊢ ‖f‖ = ENNReal.toReal (∫⁻ (a : α), ↑‖↑↑f a‖₊ ∂μ)
[PROOFSTEP]
simp [Lp.norm_def, snorm, snorm']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ ‖f - g‖ = ENNReal.toReal (∫⁻ (x : α), ↑‖↑↑f x - ↑↑g x‖₊ ∂μ)
[PROOFSTEP]
rw [norm_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ ENNReal.toReal (∫⁻ (a : α), ↑‖↑↑(f - g) a‖₊ ∂μ) = ENNReal.toReal (∫⁻ (x : α), ↑‖↑↑f x - ↑↑g x‖₊ ∂μ)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ ∫⁻ (a : α), ↑‖↑↑(f - g) a‖₊ ∂μ = ∫⁻ (x : α), ↑‖↑↑f x - ↑↑g x‖₊ ∂μ
[PROOFSTEP]
rw [lintegral_congr_ae]
[GOAL]
case e_a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ (fun a => ↑‖↑↑(f - g) a‖₊) =ᵐ[μ] fun a => ↑‖↑↑f a - ↑↑g a‖₊
[PROOFSTEP]
filter_upwards [Lp.coeFn_sub f g] with _ ha
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
a✝ : α
ha : ↑↑(f - g) a✝ = (↑↑f - ↑↑g) a✝
⊢ ↑‖↑↑(f - g) a✝‖₊ = ↑‖↑↑f a✝ - ↑↑g a✝‖₊
[PROOFSTEP]
simp only [ha, Pi.sub_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : { x // x ∈ Lp β 1 }
⊢ ENNReal.ofReal ‖f‖ = ∫⁻ (x : α), ↑‖↑↑f x‖₊ ∂μ
[PROOFSTEP]
rw [norm_def, ENNReal.ofReal_toReal]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : { x // x ∈ Lp β 1 }
⊢ ∫⁻ (a : α), ↑‖↑↑f a‖₊ ∂μ ≠ ⊤
[PROOFSTEP]
exact ne_of_lt (hasFiniteIntegral_coeFn f)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ ENNReal.ofReal ‖f - g‖ = ∫⁻ (x : α), ↑‖↑↑f x - ↑↑g x‖₊ ∂μ
[PROOFSTEP]
simp_rw [ofReal_norm_eq_lintegral, ← edist_eq_coe_nnnorm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ ∫⁻ (x : α), edist (↑↑(f - g) x) 0 ∂μ = ∫⁻ (x : α), edist (↑↑f x - ↑↑g x) 0 ∂μ
[PROOFSTEP]
apply lintegral_congr_ae
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ (fun a => edist (↑↑(f - g) a) 0) =ᵐ[μ] fun a => edist (↑↑f a - ↑↑g a) 0
[PROOFSTEP]
filter_upwards [Lp.coeFn_sub f g] with _ ha
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
a✝ : α
ha : ↑↑(f - g) a✝ = (↑↑f - ↑↑g) a✝
⊢ edist (↑↑(f - g) a✝) 0 = edist (↑↑f a✝ - ↑↑g a✝) 0
[PROOFSTEP]
simp only [ha, Pi.sub_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : { x // x ∈ Lp β 1 }
hf : Integrable ↑↑f
⊢ toL1 (↑↑f) hf = f
[PROOFSTEP]
simp [Integrable.toL1]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
⊢ ‖toL1 f hf‖ = ENNReal.toReal (∫⁻ (a : α), edist (f a) 0 ∂μ)
[PROOFSTEP]
simp [toL1, snorm, snorm']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
⊢ ENNReal.toReal (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) = ENNReal.toReal (∫⁻ (a : α), edist (f a) 0 ∂μ)
[PROOFSTEP]
simp [edist_eq_coe_nnnorm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
⊢ ‖toL1 f hf‖ = ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ)
[PROOFSTEP]
rw [norm_toL1, lintegral_norm_eq_lintegral_edist]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : α → β
hf : Integrable f
hg : Integrable g
⊢ edist (toL1 f hf) (toL1 g hg) = ∫⁻ (a : α), edist (f a) (g a) ∂μ
[PROOFSTEP]
simp [Integrable.toL1, snorm, snorm']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : α → β
hf : Integrable f
hg : Integrable g
⊢ ∫⁻ (a : α), ↑‖f a - g a‖₊ ∂μ = ∫⁻ (a : α), edist (f a) (g a) ∂μ
[PROOFSTEP]
simp [edist_eq_coe_nnnorm_sub]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
⊢ edist (toL1 f hf) 0 = ∫⁻ (a : α), edist (f a) 0 ∂μ
[PROOFSTEP]
simp [Integrable.toL1, snorm, snorm']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
⊢ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ = ∫⁻ (a : α), edist (f a) 0 ∂μ
[PROOFSTEP]
simp [edist_eq_coe_nnnorm]
