awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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 : ι
⊢ HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ ENNReal.toReal 1)
      ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑C : ℝ≥0∞) ≤ (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞)} : ℝ≥0∞) ≤
    eLpNorm μ[g | ℱ n] 1 μ ^ ENNReal.toReal 1
have rw : HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑C : ℝ≥0∞) ≤ (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞)} : ℝ≥0∞) ≤
  HPow.hPow (β := ℝ) (eLpNorm μ[g | ℱ n] 1 μ) 1
Tactic: rw [ENNReal.toReal_one, ENNReal.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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 : ι
⊢ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑C : ℝ≥0∞) ≤ (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞)} : ℝ≥0∞) ≤
    HPow.hPow (β := ℝ) (eLpNorm μ[g | ℱ n] 1 μ) 1
have h₁ : ∀ (x : α), (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞) = ‖μ[g | ℱ n] x‖ₑ ^ ENNReal.toReal 1
Tactic: convert!
        mul_meas_ge_le_pow_eLpNorm μ one_ne_zero ENNReal.one_ne_top
          (stronglyMeasurable_condExp.mono (hℱ n)).aestronglyMeasurable C
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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 : ι
x : α
⊢ (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞) = ‖μ[g | ℱ n] x‖ₑ ^ ENNReal.toReal 1
have h₁ : (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞) = HPow.hPow (β := ℝ) ‖μ[g | ℱ n] x‖ₑ 1
Tactic: rw [ENNReal.toReal_one, ENNReal.rpow_one, enorm_eq_nnnorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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 : ι
x : α
h₁ : (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞) = HPow.hPow (β := ℝ) ‖μ[g | ℱ n] x‖ₑ 1
⊢ (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞) = ‖μ[g | ℱ n] x‖ₑ ^ ENNReal.toReal 1
have h₂ : (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞) = ‖μ[g | ℱ n] x‖ₑ
Tactic: rw [ENNReal.toReal_one, ENNReal.rpow_one, enorm_eq_nnnorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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 : ι
x : α
h₁ : (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞) = HPow.hPow (β := ℝ) ‖μ[g | ℱ n] x‖ₑ 1
h₂ : (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞) = ‖μ[g | ℱ n] x‖ₑ
⊢ (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞) = ‖μ[g | ℱ n] x‖ₑ ^ ENNReal.toReal 1
have h₃ : (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞) = (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞)
Tactic: rw [ENNReal.toReal_one, ENNReal.rpow_one, enorm_eq_nnnorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (hypothesis)
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 δ
have this : HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ ENNReal.toReal 1)
    ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑C : ℝ≥0∞) ≤ (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞)} : ℝ≥0∞) ≤
  eLpNorm μ[g | ℱ n] 1 μ ^ ENNReal.toReal 1
Tactic: 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (hypothesis)
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 :
  HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ ENNReal.toReal 1)
      ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑C : ℝ≥0∞) ≤ (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞)} : ℝ≥0∞) ≤
    eLpNorm μ[g | ℱ n] 1 μ ^ ENNReal.toReal 1
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ ENNReal.ofReal δ
have this₁ : (μ : (a : Set α) → ℝ≥0∞) {x : α | (↑C : ℝ≥0∞) ≤ (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞)} ≤
  HPow.hPow (β := ℝ) (eLpNorm μ[g | ℱ n] 1 μ) 1 / (↑C : ℝ≥0∞)
Tactic: 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (hypothesis)
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 : ℝ≥0∞) ≤ (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞)} ≤
    HPow.hPow (β := ℝ) (eLpNorm μ[g | ℱ n] 1 μ) 1 / (↑C : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ ENNReal.ofReal δ
have this₁ : (μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ HPow.hPow (β := ℝ) (eLpNorm μ[g | ℱ n] 1 μ) 1 / (↑C : ℝ≥0∞)
Tactic: simp_rw [ENNReal.coe_le_coe] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ ENNReal.ofReal δ
have refine : HPow.hPow (β := ℝ) (eLpNorm μ[g | ℱ n] 1 μ) 1 / (↑C : ℝ≥0∞) ≤ ENNReal.ofReal δ
Tactic: refine this.trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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∞)
⊢ HPow.hPow (β := ℝ) (eLpNorm μ[g | ℱ n] 1 μ) 1 / (↑C : ℝ≥0∞) ≤ ENNReal.ofReal δ
have rw : eLpNorm μ[g | ℱ n] 1 μ ≤ eLpNorm g 1 μ
Tactic: 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (hypothesis)
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
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ i] x‖₊} μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε
have this : ∀ (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 _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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 ε
have neg : ∀ (n : ι),
  eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} μ[g | ℱ n]) 1 μ ≤
    eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} g) 1 μ
Tactic: refine ⟨C, fun n => le_trans ?_ (h {x : α | C ≤ ‖(μ[g|ℱ n]) x‖₊} (hmeas n C) (this n))⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (hypothesis)
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 : ι
⊢ eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} μ[g | ℱ n]) 1 μ ≤
    eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} g) 1 μ
have hmeasℱ : 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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 μ
have neg : 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ℱ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (goal)
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
⊢ (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0
have 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
Tactic: obtain ⟨g, hg_sm, hfg⟩ := lpMeas.ae_fin_strongly_measurable' hm f hp_ne_zero hp_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (goal)
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
have refine : g =ᶠ[ae μ] 0
Tactic: refine hfg.trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (goal)
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
have refine_1 : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
Tactic: refine ae_eq_zero_of_forall_setIntegral_eq_of_finStronglyMeasurable_trim hm ?_ ?_ hg_sm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (goal)
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 μ
⊢ g =ᶠ[ae μ] 0
have 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
Tactic: refine ae_eq_zero_of_forall_setIntegral_eq_of_finStronglyMeasurable_trim hm ?_ ?_ hg_sm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (hypothesis)
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∞)
⊢ IntegrableOn g s μ
have hfg_restrict : (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae (μ.restrict s)] g
Tactic: have hfg_restrict : f =ᵐ[μ.restrict s] g := ae_restrict_of_ae hfg