awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet.{u_1} (α := α) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h :
  ∀ (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
n : ι
this :
  (μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ HPow.hPow (β := ℝ) (eLpNorm μ[g | ℱ n] 1 μ) 1 / (↑C : ℝ≥0∞)
⊢ eLpNorm μ[g | ℱ n] 1 μ ≤ eLpNorm g 1 μ

Tactic:
exact eLpNorm_one_condExp_le_eLpNorm _

Premises used: MeasureTheory.eLpNorm_one_condExp_le_eLpNorm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet.{u_1} (α := α) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h :
  ∀ (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
⊢ ∀ (n : ι), (μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ ENNReal.ofReal δ

Tactic:
have : ∀ n, μ {x : α | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ := by
    intro n
    have : C ^ ENNReal.toReal 1 * μ {x | ENNReal.ofNNReal C ≤ ‖μ[g|ℱ n] x‖₊} ≤
        eLpNorm μ[g | ℱ n] 1 μ ^ ENNReal.toReal 1 := by
      rw [ENNReal.toReal_one, ENNReal.rpow_one]
      convert!
        mul_meas_ge_le_pow_eLpNorm μ one_ne_zero ENNReal.one_ne_top
          (stronglyMeasurable_condExp.mono (hℱ n)).aestronglyMeasurable C
      · rw [ENNReal.toReal_one, ENNReal.rpow_one, enorm_eq_nnnorm]
    rw [ENNReal.toReal_one, ENNReal.rpow_one, mul_comm, ←
      ENNReal.le_div_iff_mul_le (Or.inl (ENNReal.coe_ne_zero.2 hCpos.ne'))
        (Or.inl ENNReal.coe_lt_top.ne)] at this
    simp_rw [ENNReal.coe_le_coe] at this
    refine this.trans ?_
    rw [ENNReal.div_le_iff_le_mul (Or.inl (ENNReal.coe_ne_zero.2 hCpos.ne'))
        (Or.inl ENNReal.coe_lt_top.ne),
      hC, NNReal.inv_mk, ENNReal.coe_mul, ENNReal.coe_toNNReal hg.eLpNorm_lt_top.ne, ← mul_assoc, ←
      ENNReal.ofReal_eq_coe_nnreal, ← ENNReal.ofReal_mul hδ.le, mul_inv_cancel₀ hδ.ne',
      ENNReal.ofReal_one, one_mul, ENNReal.rpow_one]
    exact eLpNorm_one_condExp_le_eLpNorm _
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet.{u_1} (α := α) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h :
  ∀ (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
this : ∀ (n : ι), (μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ ENNReal.ofReal δ
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ i] x‖₊} μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε

Tactic:
⟨C, fun n => le_trans ?_ (h {x : α | C ≤ ‖(μ[g|ℱ n]) x‖₊} (hmeas n C) (this n))⟩

Premises used: NNNorm.nnnorm, setOf, LE.le, MeasureTheory.condExp, Exists.intro, le_trans
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet.{u_1} (α := α) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h :
  ∀ (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
this : ∀ (n : ι), (μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ ENNReal.ofReal δ
neg :
  ∀ (n : ι),
    eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} μ[g | ℱ n]) 1 μ ≤
      eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} g) 1 μ
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ i] x‖₊} μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨C, fun n => le_trans ?_ (h {x : α | C ≤ ‖(μ[g|ℱ n]) x‖₊} (hmeas n C) (this n))⟩
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet.{u_1} (α := α) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h :
  ∀ (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
this : ∀ (n : ι), (μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ ENNReal.ofReal δ
n : ι
⊢ MeasurableSet.{u_1} (α := α) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊}

Tactic:
have hmeasℱ : MeasurableSet[ℱ n] {x : α | C ≤ ‖(μ[g|ℱ n]) x‖₊} :=
    @measurableSet_le _ _ _ _ _ (ℱ n) _ _ _ _ _ measurable_const
      (@Measurable.nnnorm _ _ _ _ _ (ℱ n) _ stronglyMeasurable_condExp.measurable)
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet.{u_1} (α := α) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h :
  ∀ (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
this : ∀ (n : ι), (μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ ENNReal.ofReal δ
n : ι
hmeasℱ : MeasurableSet.{u_1} (α := α) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊}
neg :
  eLpNorm μ[Set.indicator {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} g | ℱ n] 1 μ ≤
    eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} g) 1 μ
⊢ eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} μ[g | ℱ n]) 1 μ ≤
    eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} g) 1 μ

Tactic:
rw [← eLpNorm_congr_ae (condExp_indicator hint hmeasℱ)]

Premises used: MeasureTheory.condExp_indicator, MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet.{u_1} (α := α) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h :
  ∀ (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
this : ∀ (n : ι), (μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ ENNReal.ofReal δ
n : ι
hmeasℱ : MeasurableSet.{u_1} (α := α) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊}
⊢ eLpNorm μ[Set.indicator {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} g | ℱ n] 1 μ ≤
    eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} g) 1 μ

Tactic:
eLpNorm_one_condExp_le_eLpNorm _

Premises used: MeasureTheory.eLpNorm_one_condExp_le_eLpNorm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet.{u_1} (α := α) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h :
  ∀ (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
this : ∀ (n : ι), (μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ ENNReal.ofReal δ
n : ι
hmeasℱ : MeasurableSet.{u_1} (α := α) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊}
⊢ eLpNorm μ[Set.indicator {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} g | ℱ n] 1 μ ≤
    eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} g) 1 μ

Tactic:
exact eLpNorm_one_condExp_le_eLpNorm _

Premises used: MeasureTheory.eLpNorm_one_condExp_le_eLpNorm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') x ∂μ) 0
obtain :
  ∀ (g : α → E') (hg_sm : FinStronglyMeasurable g (μ.trim hm))
    (hfg : (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] g),
    (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0
⊢ (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0

Tactic:
obtain ⟨g, hg_sm, hfg⟩ := lpMeas.ae_fin_strongly_measurable' hm f hp_ne_zero hp_ne_top

Premises used: MeasureTheory.lpMeas.ae_fin_strongly_measurable'
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') x ∂μ) 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] g
⊢ (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0

Tactic:
hfg.trans ?_

Premises used: Filter.EventuallyEq.trans
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') x ∂μ) 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] g
refine : g =ᶠ[ae μ] 0
⊢ (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0

Tactic:
refine hfg.trans ?_

Premises used: Filter.EventuallyEq.trans
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') x ∂μ) 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] g
⊢ g =ᶠ[ae μ] 0

Tactic:
ae_eq_zero_of_forall_setIntegral_eq_of_finStronglyMeasurable_trim hm ?_ ?_ hg_sm

Premises used: MeasureTheory.ae_eq_zero_of_forall_setIntegral_eq_of_finStronglyMeasurable_trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') x ∂μ) 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] g
refine_1 :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
refine_2 :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, g x ∂μ) 0
⊢ g =ᶠ[ae μ] 0

Tactic:
refine ae_eq_zero_of_forall_setIntegral_eq_of_finStronglyMeasurable_trim hm ?_ ?_ hg_sm

Premises used: MeasureTheory.ae_eq_zero_of_forall_setIntegral_eq_of_finStronglyMeasurable_trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') x ∂μ) 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae (μ.restrict s)] g

Tactic:
have hfg_restrict : f =ᵐ[μ.restrict s] g := ae_restrict_of_ae hfg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') x ∂μ) 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg_restrict : (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae (μ.restrict s)] g
refine_1 : Integrable (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') (μ.restrict s)
⊢ IntegrableOn g s μ

Tactic:
rw [IntegrableOn, integrable_congr hfg_restrict.symm]

Premises used: MeasureTheory.integrable_congr, MeasureTheory.IntegrableOn, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') x ∂μ) 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg_restrict : (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae (μ.restrict s)] g
⊢ Integrable (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') (μ.restrict s)

Tactic:
hf_int_finite s hs hμs

Premises used: MeasureTheory.IntegrableOn
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') x ∂μ) 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg_restrict : (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae (μ.restrict s)] g
⊢ Integrable (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') (μ.restrict s)

Tactic:
exact hf_int_finite s hs hμs
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') x ∂μ) 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg_restrict : (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae (μ.restrict s)] g
refine_2 : Eq.{u_2 + 1} (α := E') (∫ (a : α) in s, (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') a ∂μ) 0
⊢ Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, g x ∂μ) 0

Tactic:
rw [integral_congr_ae hfg_restrict.symm]

Premises used: MeasureTheory.integral_congr_ae, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') x ∂μ) 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg_restrict : (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae (μ.restrict s)] g
⊢ Eq.{u_2 + 1} (α := E') (∫ (a : α) in s, (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') a ∂μ) 0

Tactic:
hf_zero s hs hμs