-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean
theorem lintegral_nnnorm_condExpL2_le (hs : MeasurableSet[m] s) (hμs : μ s ≠ ∞) (f : Lp ℝ 2 μ) :
    ∫⁻ x in s, ‖(condExpL2 ℝ ℝ hm f : α → ℝ) x‖₊ ∂μ ≤ ∫⁻ x in s, ‖f x‖₊ ∂μ

Proof state:
case refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) f)) μ := lpMeas.aeStronglyMeasurable ((condExpL2 ℝ ℝ hm) f)
g : α → ℝ := Exists.choose h_meas
hg_meas : StronglyMeasurable g
hg_eq : g =ᶠ[ae μ] ↑↑↑((condExpL2 ℝ ℝ hm) f)
hg_eq_restrict : g =ᶠ[ae (μ.restrict s)] ↑↑↑((condExpL2 ℝ ℝ hm) f)
hg_nnnorm_eq : (fun x => ↑‖g x‖₊) =ᶠ[ae (μ.restrict s)] fun x => ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊
⊢ IntegrableOn (↑↑f) s μ

Tactic:
exact integrableOn_Lp_of_measure_ne_top f fact_one_le_two_ennreal.elim hμs

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 μ)
h_meas : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) f)) μ := lpMeas.aeStronglyMeasurable ((condExpL2 ℝ ℝ hm) f)
g : α → ℝ := Exists.choose h_meas
hg_meas : StronglyMeasurable g
hg_eq : g =ᶠ[ae μ] ↑↑↑((condExpL2 ℝ ℝ hm) f)
hg_eq_restrict : g =ᶠ[ae (μ.restrict s)] ↑↑↑((condExpL2 ℝ ℝ hm) f)
⊢ ∫⁻ (x : α) in s, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊ ∂μ ≤ ∫⁻ (x : α) in s, ↑‖↑↑f x‖₊ ∂μ

Tactic:
have hg_nnnorm_eq : (fun x => (‖g x‖₊ : ℝ≥0∞)) =ᵐ[μ.restrict s] fun x =>
    (‖(condExpL2 ℝ ℝ hm f : α → ℝ) x‖₊ : ℝ≥0∞) := by
  refine hg_eq_restrict.mono fun x hx => ?_
  dsimp only
  simp_rw [hx]

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) f)) μ := lpMeas.aeStronglyMeasurable ((condExpL2 ℝ ℝ hm) f)
g : α → ℝ := Exists.choose h_meas
hg_meas : StronglyMeasurable g
hg_eq : g =ᶠ[ae μ] ↑↑↑((condExpL2 ℝ ℝ hm) f)
hg_eq_restrict : g =ᶠ[ae (μ.restrict s)] ↑↑↑((condExpL2 ℝ ℝ hm) f)
hg_nnnorm_eq : (fun x => ↑‖g x‖₊) =ᶠ[ae (μ.restrict s)] fun x => ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊
⊢ ∫⁻ (x : α) in s, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊ ∂μ ≤ ∫⁻ (x : α) in s, ↑‖↑↑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 μ)
h_meas : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) f)) μ := lpMeas.aeStronglyMeasurable ((condExpL2 ℝ ℝ hm) f)
g : α → ℝ := Exists.choose h_meas
hg_meas : StronglyMeasurable g
hg_eq : g =ᶠ[ae μ] ↑↑↑((condExpL2 ℝ ℝ hm) f)
⊢ ∫⁻ (x : α) in s, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊ ∂μ ≤ ∫⁻ (x : α) in s, ↑‖↑↑f x‖₊ ∂μ

Tactic:
have hg_eq_restrict : g =ᵐ[μ.restrict s] condExpL2 ℝ ℝ hm f := ae_restrict_of_ae hg_eq

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) f)) μ := lpMeas.aeStronglyMeasurable ((condExpL2 ℝ ℝ hm) f)
g : α → ℝ := Exists.choose h_meas
hg_meas : StronglyMeasurable g
hg_eq : g =ᶠ[ae μ] ↑↑↑((condExpL2 ℝ ℝ hm) f)
hg_eq_restrict : g =ᶠ[ae (μ.restrict s)] ↑↑↑((condExpL2 ℝ ℝ hm) f)
⊢ ∫⁻ (x : α) in s, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊ ∂μ ≤ ∫⁻ (x : α) in s, ↑‖↑↑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 μ)
⊢ ∫⁻ (x : α) in s, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊ ∂μ ≤ ∫⁻ (x : α) in s, ↑‖↑↑f x‖₊ ∂μ

Tactic:
let h_meas := lpMeas.aeStronglyMeasurable (condExpL2 ℝ ℝ hm f)

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) f)) μ := lpMeas.aeStronglyMeasurable ((condExpL2 ℝ ℝ hm) f)
⊢ ∫⁻ (x : α) in s, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊ ∂μ ≤ ∫⁻ (x : α) in s, ↑‖↑↑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 μ)
h_meas : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) f)) μ := lpMeas.aeStronglyMeasurable ((condExpL2 ℝ ℝ hm) f)
g : α → ℝ := Exists.choose h_meas
hg_meas : StronglyMeasurable g
hg_eq : g =ᶠ[ae μ] ↑↑↑((condExpL2 ℝ ℝ hm) f)
hg_eq_restrict : g =ᶠ[ae (μ.restrict s)] ↑↑↑((condExpL2 ℝ ℝ hm) f)
x : α
hx : g x = ↑↑↑((condExpL2 ℝ ℝ hm) f) x
⊢ ↑‖g x‖₊ = ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊

Tactic:
simp_rw [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 μ)
h_meas : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) f)) μ := lpMeas.aeStronglyMeasurable ((condExpL2 ℝ ℝ hm) f)
g : α → ℝ := Exists.choose h_meas
hg_meas : StronglyMeasurable g
hg_eq : g =ᶠ[ae μ] ↑↑↑((condExpL2 ℝ ℝ hm) f)
hg_eq_restrict : g =ᶠ[ae (μ.restrict s)] ↑↑↑((condExpL2 ℝ ℝ hm) f)
hg_nnnorm_eq : (fun x => ↑‖g x‖₊) =ᶠ[ae (μ.restrict s)] fun x => ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊
⊢ ∫⁻ (a : α) in s, ↑‖g a‖₊ ∂μ ≤ ∫⁻ (x : α) in s, ↑‖↑↑f x‖₊ ∂μ

Tactic:
refine lintegral_enorm_le_of_forall_fin_meas_integral_eq
  hm (Lp.stronglyMeasurable f) ?_ ?_ ?_ ?_ hs hμs

Result:
case refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) f)) μ := lpMeas.aeStronglyMeasurable ((condExpL2 ℝ ℝ hm) f)
g : α → ℝ := Exists.choose h_meas
hg_meas : StronglyMeasurable g
hg_eq : g =ᶠ[ae μ] ↑↑↑((condExpL2 ℝ ℝ hm) f)
hg_eq_restrict : g =ᶠ[ae (μ.restrict s)] ↑↑↑((condExpL2 ℝ ℝ hm) f)
hg_nnnorm_eq : (fun x => ↑‖g x‖₊) =ᶠ[ae (μ.restrict s)] fun x => ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊
⊢ IntegrableOn (↑↑f) s μ

case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) f)) μ := lpMeas.aeStronglyMeasurable ((condExpL2 ℝ ℝ hm) f)
g : α → ℝ := Exists.choose h_meas
hg_meas : StronglyMeasurable g
hg_eq : g =ᶠ[ae μ] ↑↑↑((condExpL2 ℝ ℝ hm) f)
hg_eq_restrict : g =ᶠ[ae (μ.restrict s)] ↑↑↑((condExpL2 ℝ ℝ hm) f)
hg_nnnorm_eq : (fun x => ↑‖g x‖₊) =ᶠ[ae (μ.restrict s)] fun x => ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊
⊢ StronglyMeasurable g

case refine_3
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) f)) μ := lpMeas.aeStronglyMeasurable ((condExpL2 ℝ ℝ hm) f)
g : α → ℝ := Exists.choose h_meas
hg_meas : StronglyMeasurable g
hg_eq : g =ᶠ[ae μ] ↑↑↑((condExpL2 ℝ ℝ hm) f)
hg_eq_restrict : g =ᶠ[ae (μ.restrict s)] ↑↑↑((condExpL2 ℝ ℝ hm) f)
hg_nnnorm_eq : (fun x => ↑‖g x‖₊) =ᶠ[ae (μ.restrict s)] fun x => ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊
⊢ IntegrableOn g s μ

case refine_4
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) f)) μ := lpMeas.aeStronglyMeasurable ((condExpL2 ℝ ℝ hm) f)
g : α → ℝ := Exists.choose h_meas
hg_meas : StronglyMeasurable g
hg_eq : g =ᶠ[ae μ] ↑↑↑((condExpL2 ℝ ℝ hm) f)
hg_eq_restrict : g =ᶠ[ae (μ.restrict s)] ↑↑↑((condExpL2 ℝ ℝ hm) f)
hg_nnnorm_eq : (fun x => ↑‖g x‖₊) =ᶠ[ae (μ.restrict s)] fun x => ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊
⊢ ∀ (t : Set α), MeasurableSet t → μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, ↑↑f x ∂μ