-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
lemma condExp_mono (hf : Integrable f μ) (hg : Integrable g μ) (hfg : f ≤ᵐ[μ] g) :
    μ[f|m] ≤ᵐ[μ] μ[g|m]

Proof state:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ 0 ≤ᶠ[ae μ] 0

Tactic:
rfl

Result:
no goals

Proof state:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ μ[f|m] ≤ᶠ[ae μ] μ[g|m]

Tactic:
exact (condExp_ae_eq_condExpL1 hm _).trans_le
  ((condExpL1_mono hf hg hfg).trans_eq (condExp_ae_eq_condExpL1 hm _).symm)

Result:
no goals

Proof state:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
hm : m ≤ m₀
⊢ μ[f|m] ≤ᶠ[ae μ] μ[g|m]

Tactic:
by_cases hμm : SigmaFinite (μ.trim hm)

Result:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ μ[f|m] ≤ᶠ[ae μ] μ[g|m]

case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f|m] ≤ᶠ[ae μ] μ[g|m]

Proof state:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
hm : m ≤ m₀
⊢ μ[f|m] ≤ᶠ[ae μ] μ[g|m]

case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
hm : ¬m ≤ m₀
⊢ μ[f|m] ≤ᶠ[ae μ] μ[g|m]

Tactic:
swap

Result:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
hm : ¬m ≤ m₀
⊢ μ[f|m] ≤ᶠ[ae μ] μ[g|m]

case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
hm : m ≤ m₀
⊢ μ[f|m] ≤ᶠ[ae μ] μ[g|m]

Proof state:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
hm : ¬m ≤ m₀
⊢ 0 ≤ᶠ[ae μ] 0

Tactic:
rfl

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f|m] ≤ᶠ[ae μ] μ[g|m]

Tactic:
simp_rw [condExp_of_not_sigmaFinite hm hμm]

Result:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ 0 ≤ᶠ[ae μ] 0

Proof state:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ μ[f|m] ≤ᶠ[ae μ] μ[g|m]

case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f|m] ≤ᶠ[ae μ] μ[g|m]

Tactic:
swap

Result:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f|m] ≤ᶠ[ae μ] μ[g|m]

case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ μ[f|m] ≤ᶠ[ae μ] μ[g|m]

Proof state:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
⊢ μ[f|m] ≤ᶠ[ae μ] μ[g|m]

Tactic:
by_cases hm : m ≤ m₀

Result:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
hm : m ≤ m₀
⊢ μ[f|m] ≤ᶠ[ae μ] μ[g|m]

case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
hm : ¬m ≤ m₀
⊢ μ[f|m] ≤ᶠ[ae μ] μ[g|m]

Proof state:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
hm : ¬m ≤ m₀
⊢ μ[f|m] ≤ᶠ[ae μ] μ[g|m]

Tactic:
simp_rw [condExp_of_not_le hm]

Result:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
hm : ¬m ≤ m₀
⊢ 0 ≤ᶠ[ae μ] 0