-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean
theorem condExpL2_ae_eq_zero_of_ae_eq_zero (hs : MeasurableSet[m] s) (hμs : μ s ≠ ∞) {f : Lp ℝ 2 μ}
    (hf : f =ᵐ[μ.restrict s] 0) : condExpL2 ℝ ℝ hm f =ᵐ[μ.restrict s] (0 : α → ℝ)

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
⊢ ∫⁻ (x : α) in s, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊ ∂μ = 0

Tactic:
refine le_antisymm ?_ (zero_le _)

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
⊢ ∫⁻ (x : α) in s, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊ ∂μ ≤ 0

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
x : α
hx : ↑↑f x = 0 x
⊢ ↑‖0 x‖₊ = 0 x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
⊢ (fun x => ↑‖↑↑f x‖₊) =ᶠ[ae (μ.restrict s)] 0

Tactic:
refine hf.mono fun x hx => ?_

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
x : α
hx : ↑↑f x = 0 x
⊢ (fun x => ↑‖↑↑f x‖₊) x = 0 x

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
h_nnnorm_eq_zero : ∫⁻ (x : α) in s, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊ ∂μ = 0
⊢ ↑↑↑((condExpL2 ℝ ℝ hm) f) =ᶠ[ae (μ.restrict s)] 0

Tactic:
rw [lintegral_eq_zero_iff] at h_nnnorm_eq_zero

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
h_nnnorm_eq_zero : (fun x => ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊) =ᶠ[ae (μ.restrict s)] 0
⊢ ↑↑↑((condExpL2 ℝ ℝ hm) f) =ᶠ[ae (μ.restrict s)] 0

α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
h_nnnorm_eq_zero : ∫⁻ (x : α) in s, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊ ∂μ = 0
⊢ Measurable fun x => ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
h_nnnorm_eq_zero : (fun x => ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊) =ᶠ[ae (μ.restrict s)] 0
x : α
hx : ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊ = 0
⊢ ↑↑↑((condExpL2 ℝ ℝ hm) f) x = 0

Tactic:
rwa [ENNReal.coe_eq_zero, nnnorm_eq_zero] at hx

Result:
no goals

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
x : α
hx : ↑↑f x = 0 x
⊢ ↑‖↑↑f x‖₊ = 0 x

Tactic:
rw [hx]

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
x : α
hx : ↑↑f x = 0 x
⊢ ↑‖0 x‖₊ = 0 x

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
⊢ ∫⁻ (x : α) in s, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊ ∂μ ≤ 0

Tactic:
refine (lintegral_nnnorm_condExpL2_le hs hμs f).trans (le_of_eq ?_)

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
⊢ ∫⁻ (x : α) in s, ↑‖↑↑f x‖₊ ∂μ = 0

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
⊢ ∫⁻ (x : α) in s, ↑‖↑↑f x‖₊ ∂μ = 0

Tactic:
rw [lintegral_eq_zero_iff]

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
⊢ (fun x => ↑‖↑↑f x‖₊) =ᶠ[ae (μ.restrict s)] 0

α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
⊢ Measurable fun x => ↑‖↑↑f x‖₊

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
⊢ Measurable fun x => ↑‖↑↑f x‖₊

Tactic:
exact (Lp.stronglyMeasurable _).enorm

Result:
no goals

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
h_nnnorm_eq_zero : (fun x => ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊) =ᶠ[ae (μ.restrict s)] 0
x : α
hx : (fun x => ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊) x = 0 x
⊢ ↑↑↑((condExpL2 ℝ ℝ hm) f) x = 0 x

Tactic:
dsimp only at hx

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
h_nnnorm_eq_zero : (fun x => ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊) =ᶠ[ae (μ.restrict s)] 0
x : α
hx : ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊ = 0 x
⊢ ↑↑↑((condExpL2 ℝ ℝ hm) f) x = 0 x

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
h_nnnorm_eq_zero : ∫⁻ (x : α) in s, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊ ∂μ = 0
⊢ Measurable ↑↑↑((condExpL2 ℝ ℝ hm) f)

Tactic:
exact (Lp.stronglyMeasurable _).measurable

Result:
no goals

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
x : α
hx : ↑↑f x = 0 x
⊢ (fun x => ↑‖↑↑f x‖₊) x = 0 x

Tactic:
dsimp only

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
x : α
hx : ↑↑f x = 0 x
⊢ ↑‖↑↑f x‖₊ = 0 x

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
h_nnnorm_eq_zero : (fun x => ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊) =ᶠ[ae (μ.restrict s)] 0
⊢ ↑↑↑((condExpL2 ℝ ℝ hm) f) =ᶠ[ae (μ.restrict s)] 0

Tactic:
refine h_nnnorm_eq_zero.mono fun x hx => ?_

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
h_nnnorm_eq_zero : (fun x => ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊) =ᶠ[ae (μ.restrict s)] 0
x : α
hx : (fun x => ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊) x = 0 x
⊢ ↑↑↑((condExpL2 ℝ ℝ hm) f) x = 0 x

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
h_nnnorm_eq_zero : (fun x => ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊) =ᶠ[ae (μ.restrict s)] 0
x : α
hx : ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊ = 0 x
⊢ ↑↑↑((condExpL2 ℝ ℝ hm) f) x = 0 x

Tactic:
rw [Pi.zero_apply] at hx ⊢

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
h_nnnorm_eq_zero : (fun x => ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊) =ᶠ[ae (μ.restrict s)] 0
x : α
hx : ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊ = 0
⊢ ↑↑↑((condExpL2 ℝ ℝ hm) f) x = 0