-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
lemma eLpNorm_condExp_le : eLpNorm (μ[f | m]) 2 μ ≤ eLpNorm f 2 μ

Proof state:
case pos.inr
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
hf : eLpNorm f 2 μ ≠ ⊤
⊢ eLpNorm (μ[f|m]) 2 μ ≤ eLpNorm f 2 μ

Tactic:
replace hf : MemLp f 2 μ := ⟨hfi.1, Ne.lt_top' fun a ↦ hf (id (Eq.symm a))⟩

Result:
case pos.inr
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
hf : MemLp f 2 μ
⊢ eLpNorm (μ[f|m]) 2 μ ≤ eLpNorm f 2 μ

Proof state:
case pos.inr
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
hf : MemLp f 2 μ
⊢ eLpNorm (μ[f|m]) 2 μ ≤ eLpNorm f 2 μ

Tactic:
rw [← eLpNorm_congr_ae (hf.condExpL2_ae_eq_condExp' (𝕜 := ℝ) hm hfi)]

Result:
case pos.inr
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
hf : MemLp f 2 μ
⊢ eLpNorm (↑↑↑((condExpL2 E ℝ hm) (MemLp.toLp f hf))) 2 μ ≤ eLpNorm f 2 μ

Proof state:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hm : ¬m ≤ m₀
⊢ eLpNorm (μ[f|m]) 2 μ ≤ eLpNorm f 2 μ

Tactic:
simp [condExp_of_not_le hm]

Result:
no goals

Proof state:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
⊢ eLpNorm (μ[f|m]) 2 μ ≤ eLpNorm f 2 μ

Tactic:
obtain hf | hf := eq_or_ne (eLpNorm f 2 μ) ∞

Result:
case pos.inl
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
hf : eLpNorm f 2 μ = ⊤
⊢ eLpNorm (μ[f|m]) 2 μ ≤ eLpNorm f 2 μ

case pos.inr
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
hf : eLpNorm f 2 μ ≠ ⊤
⊢ eLpNorm (μ[f|m]) 2 μ ≤ eLpNorm f 2 μ

Proof state:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : ¬Integrable f μ
⊢ eLpNorm 0 2 μ ≤ eLpNorm f 2 μ

Tactic:
simp

Result:
no goals

Proof state:
case pos.inr
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
hf : MemLp f 2 μ
⊢ eLpNorm (↑↑(MemLp.toLp f hf)) 2 μ ≤ eLpNorm f 2 μ

Tactic:
rw [eLpNorm_congr_ae hf.coeFn_toLp]

Result:
no goals

Proof state:
case pos.inr
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
hf : MemLp f 2 μ
⊢ eLpNorm (↑↑↑((condExpL2 E ℝ hm) (MemLp.toLp f hf))) 2 μ ≤ eLpNorm f 2 μ

Tactic:
refine le_trans (eLpNorm_condExpL2_le hm _) ?_

Result:
case pos.inr
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
hf : MemLp f 2 μ
⊢ eLpNorm (↑↑(MemLp.toLp f hf)) 2 μ ≤ eLpNorm f 2 μ

Proof state:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : ¬Integrable f μ
⊢ eLpNorm (μ[f|m]) 2 μ ≤ eLpNorm f 2 μ

Tactic:
rw [condExp_of_not_integrable hfi]

Result:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : ¬Integrable f μ
⊢ eLpNorm 0 2 μ ≤ eLpNorm f 2 μ

Proof state:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hm : m ≤ m₀
hfμ : ¬SigmaFinite (μ.trim hm)
⊢ eLpNorm 0 2 μ ≤ eLpNorm f 2 μ

Tactic:
simp

Result:
no goals

Proof state:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
⊢ eLpNorm (μ[f|m]) 2 μ ≤ eLpNorm f 2 μ

case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : ¬Integrable f μ
⊢ eLpNorm (μ[f|m]) 2 μ ≤ eLpNorm f 2 μ

Tactic:
swap

Result:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : ¬Integrable f μ
⊢ eLpNorm (μ[f|m]) 2 μ ≤ eLpNorm f 2 μ

case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
⊢ eLpNorm (μ[f|m]) 2 μ ≤ eLpNorm f 2 μ

Proof state:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
⊢ eLpNorm (μ[f|m]) 2 μ ≤ eLpNorm f 2 μ

Tactic:
by_cases hfi : Integrable f μ

Result:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
⊢ eLpNorm (μ[f|m]) 2 μ ≤ eLpNorm f 2 μ

case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : ¬Integrable f μ
⊢ eLpNorm (μ[f|m]) 2 μ ≤ eLpNorm f 2 μ