-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
theorem condExp_bot' [hμ : NeZero μ] (f : α → E) :
    μ[f|⊥] = fun _ => (μ Set.univ).toReal⁻¹ • ∫ x, f x ∂μ

Proof state:
case pos.intro
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable (μ[f|⊥])
c : E
h_eq : μ[f|⊥] = fun x => c
⊢ (fun x => c) = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
have h_integral : ∫ x, (μ[f|⊥]) x ∂μ = ∫ x, f x ∂μ := integral_condExp bot_le

Result:
case pos.intro
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable (μ[f|⊥])
c : E
h_eq : μ[f|⊥] = fun x => c
h_integral : ∫ (x : α), (μ[f|⊥]) x ∂μ = ∫ (x : α), f x ∂μ
⊢ (fun x => c) = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

Proof state:
case pos.intro
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable (μ[f|⊥])
c : E
h_eq : μ[f|⊥] = fun x => c
h_integral : (μ Set.univ).toReal • c = ∫ (x : α), f x ∂μ
⊢ (μ Set.univ).toReal ≠ 0

Tactic:
rw [Ne, ENNReal.toReal_eq_zero_iff, not_or]

Result:
case pos.intro
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable (μ[f|⊥])
c : E
h_eq : μ[f|⊥] = fun x => c
h_integral : (μ Set.univ).toReal • c = ∫ (x : α), f x ∂μ
⊢ ¬μ Set.univ = 0 ∧ ¬μ Set.univ = ⊤

Proof state:
case neg
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : ¬IsFiniteMeasure μ
h : ¬SigmaFinite (μ.trim ⋯)
⊢ μ[f|⊥] = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
rw [not_isFiniteMeasure_iff] at hμ_finite

Result:
case neg
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : μ Set.univ = ⊤
h : ¬SigmaFinite (μ.trim ⋯)
⊢ μ[f|⊥] = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

Proof state:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
⊢ μ[f|⊥] = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
by_cases hμ_finite : IsFiniteMeasure μ

Result:
case pos
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
⊢ μ[f|⊥] = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

case neg
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : ¬IsFiniteMeasure μ
⊢ μ[f|⊥] = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

Proof state:
case pos.intro
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable (μ[f|⊥])
c : E
h_eq : μ[f|⊥] = fun x => c
⊢ μ[f|⊥] = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
rw [h_eq]

Result:
case pos.intro
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable (μ[f|⊥])
c : E
h_eq : μ[f|⊥] = fun x => c
⊢ (fun x => c) = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

Proof state:
case neg
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : μ Set.univ = ⊤
h : ¬SigmaFinite (μ.trim ⋯)
⊢ 0 = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
simp only [hμ_finite, ENNReal.top_toReal, inv_zero, zero_smul]

Result:
case neg
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : μ Set.univ = ⊤
h : ¬SigmaFinite (μ.trim ⋯)
⊢ 0 = fun x => 0

Proof state:
case pos
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable (μ[f|⊥])
⊢ μ[f|⊥] = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
obtain ⟨c, h_eq⟩ := stronglyMeasurable_bot_iff.mp h_meas

Result:
case pos.intro
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable (μ[f|⊥])
c : E
h_eq : μ[f|⊥] = fun x => c
⊢ μ[f|⊥] = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

Proof state:
case neg
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : μ Set.univ = ⊤
h : ¬SigmaFinite (μ.trim ⋯)
⊢ 0 = fun x => 0

Tactic:
rfl

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : ¬IsFiniteMeasure μ
⊢ μ[f|⊥] = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
have h : ¬SigmaFinite (μ.trim bot_le) := by rwa [sigmaFinite_trim_bot_iff]

Result:
case neg
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : ¬IsFiniteMeasure μ
h : ¬SigmaFinite (μ.trim ⋯)
⊢ μ[f|⊥] = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

Proof state:
case pos
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
⊢ μ[f|⊥] = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
have h_meas : StronglyMeasurable[⊥] (μ[f|⊥]) := stronglyMeasurable_condExp

Result:
case pos
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable (μ[f|⊥])
⊢ μ[f|⊥] = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

Proof state:
case pos.intro
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable (μ[f|⊥])
c : E
h_eq : μ[f|⊥] = fun x => c
h_integral : ∫ (x : α), (μ[f|⊥]) x ∂μ = ∫ (x : α), f x ∂μ
⊢ (fun x => c) = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
simp_rw [h_eq, integral_const] at h_integral

Result:
case pos.intro
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable (μ[f|⊥])
c : E
h_eq : μ[f|⊥] = fun x => c
h_integral : (μ Set.univ).toReal • c = ∫ (x : α), f x ∂μ
⊢ (fun x => c) = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ