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

Proof state:
α : 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
⊢ eLpNorm (μ[f|m]) 2 μ ≤ eLpNorm f 2 μ

Tactic:
by_cases hm : m ≤ m₀

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₀
⊢ 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₀
⊢ 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)
⊢ eLpNorm (μ[f|m]) 2 μ ≤ eLpNorm f 2 μ

Tactic:
rw [condExp_of_not_sigmaFinite hm hfμ]

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)
⊢ eLpNorm 0 2 μ ≤ eLpNorm f 2 μ

Proof state:
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 μ

Tactic:
simp [hf]

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₀
⊢ 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₀
⊢ 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₀
⊢ 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₀
⊢ 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₀
⊢ eLpNorm (μ[f|m]) 2 μ ≤ eLpNorm f 2 μ

Tactic:
by_cases hfμ : SigmaFinite (μ.trim hm)

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)
⊢ 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)
⊢ 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 μ

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 (μ[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)
⊢ 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)
⊢ eLpNorm (μ[f|m]) 2 μ ≤ eLpNorm f 2 μ