awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : Integrable f μ
h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑R : ℝ) < |μ[f | m] x|} : ℝ≥0∞)
x : α
hx : Membership.mem (γ := Set α) {x : α | (↑R : ℝ) < |μ[f | m] x|} x
⊢ NNReal.mk (↑R : ℝ) ⋯ ≤ ‖μ[f | m] x‖₊

Tactic:
Subtype.mk_le_mk.2 (le_of_lt hx)

Premises used: Iff.mpr, le_of_lt, Subtype.mk_le_mk
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : Integrable f μ
h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑R : ℝ) < |μ[f | m] x|} : ℝ≥0∞)
x : α
hx : Membership.mem (γ := Set α) {x : α | (↑R : ℝ) < |μ[f | m] x|} x
⊢ NNReal.mk (↑R : ℝ) ⋯ ≤ ‖μ[f | m] x‖₊

Tactic:
exact Subtype.mk_le_mk.2 (le_of_lt hx)

Premises used: Iff.mpr, le_of_lt, Subtype.mk_le_mk
-- 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
⊢ ∀ (n : ι) (C : ℝ≥0), MeasurableSet.{u_1} (α := α) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊}

Tactic:
have hmeas : ∀ n, ∀ C, MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} := fun n C =>
    measurableSet_le measurable_const (stronglyMeasurable_condExp.mono (hℱ n)).measurable.nnnorm
-- 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‖₊}
⊢ MemLp g 1 μ

Tactic:
have hg : MemLp g 1 μ := memLp_one_iff_integrable.2 hint
-- 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 μ
⊢ UniformIntegrable (β := ℝ) (fun (i : ι) ↦ μ[g | ℱ i]) 1 μ

Tactic:
uniformIntegrable_of le_rfl ENNReal.one_ne_top
    (fun n => (stronglyMeasurable_condExp.mono (hℱ n)).aestronglyMeasurable) fun ε hε => ?_

Premises used: le_rfl, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.uniformIntegrable_of, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.StronglyMeasurable.mono, ENNReal.one_ne_top
-- 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 μ
refine :
  ∀ (ε : ℝ) (hε : 0 < ε),
    ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ i] x‖₊} μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε
⊢ UniformIntegrable (β := ℝ) (fun (i : ι) ↦ μ[g | ℱ i]) 1 μ

Tactic:
refine uniformIntegrable_of le_rfl ENNReal.one_ne_top
    (fun n => (stronglyMeasurable_condExp.mono (hℱ n)).aestronglyMeasurable) fun ε hε => ?_

Premises used: le_rfl, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.uniformIntegrable_of, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.StronglyMeasurable.mono, ENNReal.one_ne_top
-- 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 < ε
pos :
  ∀ (hne : eLpNorm g 1 μ = 0),
    ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ i] x‖₊} μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε
neg :
  ∀ (hne : ¬eLpNorm g 1 μ = 0),
    ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ i] x‖₊} μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ i] x‖₊} μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε

Tactic:
by_cases hne : eLpNorm g 1 μ = 0

Premises used: OfNat.ofNat, MeasureTheory.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
⊢ g =ᶠ[ae μ] 0

Tactic:
rw [eLpNorm_eq_zero_iff hg.1 one_ne_zero] at hne

Premises used: MeasureTheory.eLpNorm_eq_zero_iff, And.left, one_ne_zero
-- 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 : g =ᶠ[ae μ] 0
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ i] x‖₊} μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε

Tactic:
⟨0, fun n => (le_of_eq <|
      (eLpNorm_eq_zero_iff ((stronglyMeasurable_condExp.mono (hℱ n)).aestronglyMeasurable.indicator
        (hmeas n 0)) one_ne_zero).2 ?_).trans zero_le⟩

Premises used: Iff.mpr, zero_le, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.eLpNorm_eq_zero_iff, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.StronglyMeasurable.mono, MeasureTheory.AEStronglyMeasurable.indicator, Exists.intro, LE.le.trans, le_of_eq, one_ne_zero, OfNat.ofNat
-- 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 : g =ᶠ[ae μ] 0
pos : ∀ (n : ι), Set.indicator {x : α | 0 ≤ ‖μ[g | ℱ n] x‖₊} μ[g | ℱ n] =ᶠ[ae μ] 0
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ i] x‖₊} μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨0, fun n => (le_of_eq <|
      (eLpNorm_eq_zero_iff ((stronglyMeasurable_condExp.mono (hℱ n)).aestronglyMeasurable.indicator
        (hmeas n 0)) one_ne_zero).2 ?_).trans zero_le⟩
-- 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 : g =ᶠ[ae μ] 0
n : ι
h : ∀ (x : α) (hx : μ[g | ℱ n] x = μ[0 | ℱ n] x), Set.indicator {x : α | 0 ≤ ‖μ[g | ℱ n] x‖₊} μ[g | ℱ n] x = 0 x
⊢ Set.indicator {x : α | 0 ≤ ‖μ[g | ℱ n] x‖₊} μ[g | ℱ n] =ᶠ[ae μ] 0

Tactic:
filter_upwards [condExp_congr_ae (m := ℱ n) hne] with x hx

Premises used: MeasureTheory.condExp_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 : g =ᶠ[ae μ] 0
n : ι
x : α
hx : μ[g | ℱ n] x = μ[0 | ℱ n] x
⊢ Set.indicator {x : α | 0 ≤ ‖μ[g | ℱ n] x‖₊} μ[g | ℱ n] x = 0 x

Tactic:
simp only [zero_le', Set.setOf_true, Set.indicator_univ, Pi.zero_apply, hx, condExp_zero]

Premises used: MeasureTheory.condExp_zero, Pi.zero_apply, Set.indicator_univ, zero_le', Set.setOf_true
-- 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 ε
⊢ let C := (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal;
  C = (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal

Tactic:
set C : ℝ≥0 := (.mk δ hδ.le)⁻¹ * (eLpNorm g 1 μ).toNNReal with hC

Premises used: ENNReal.toNNReal, OfNat.ofNat, MeasureTheory.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
⊢ 0 < C

Tactic:
have hCpos : 0 < C := mul_pos (inv_pos.2 hδ) (ENNReal.toNNReal_pos hne hg.eLpNorm_lt_top.ne)
-- 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 : ι
rw :
  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑C : ℝ≥0∞) ≤ (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞)} : ℝ≥0∞) ≤
    HPow.hPow (β := ℝ) (eLpNorm μ[g | ℱ n] 1 μ) 1
⊢ 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:
rw [ENNReal.toReal_one, ENNReal.rpow_one]

Premises used: ENNReal.toReal_one, ENNReal.rpow_one
-- 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 : ι
⊢ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑C : ℝ≥0∞) ≤ ‖μ[g | ℱ n] x‖ₑ ^ ENNReal.toReal 1} : ℝ≥0∞) ≤
    eLpNorm μ[g | ℱ n] 1 μ ^ ENNReal.toReal 1

Tactic:
mul_meas_ge_le_pow_eLpNorm μ one_ne_zero ENNReal.one_ne_top
          (stronglyMeasurable_condExp.mono (hℱ n)).aestronglyMeasurable C

Premises used: ENNReal.ofNNReal, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.StronglyMeasurable.mono, one_ne_zero, MeasureTheory.mul_meas_ge_le_pow_eLpNorm, ENNReal.one_ne_top
-- 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 : ι
h₁ : ∀ (x : α), (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞) = ‖μ[g | ℱ n] x‖ₑ ^ ENNReal.toReal 1
⊢ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑C : ℝ≥0∞) ≤ (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞)} : ℝ≥0∞) ≤
    HPow.hPow (β := ℝ) (eLpNorm μ[g | ℱ n] 1 μ) 1

Tactic:
convert!
        mul_meas_ge_le_pow_eLpNorm μ one_ne_zero ENNReal.one_ne_top
          (stronglyMeasurable_condExp.mono (hℱ n)).aestronglyMeasurable C

Premises used: ENNReal.ofNNReal, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.StronglyMeasurable.mono, one_ne_zero, MeasureTheory.mul_meas_ge_le_pow_eLpNorm, ENNReal.one_ne_top
-- 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 : ι
x : α
h₁ : (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞) = HPow.hPow (β := ℝ) ‖μ[g | ℱ n] x‖ₑ 1
h₂ : (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞) = ‖μ[g | ℱ n] x‖ₑ
h₃ h₄ : (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞) = (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞)
⊢ (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞) = ‖μ[g | ℱ n] x‖ₑ ^ ENNReal.toReal 1

Tactic:
rw [ENNReal.toReal_one, ENNReal.rpow_one, enorm_eq_nnnorm]

Premises used: ENNReal.toReal_one, ENNReal.rpow_one, enorm_eq_nnnorm
-- 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 : ι
⊢ 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]
-- 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 :
  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 : ℝ≥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

Premises used: Iff.mpr, ENNReal.toReal_one, ENNReal.rpow_one, ENNReal.le_div_iff_mul_le, ENNReal.coe_ne_zero, LT.lt.ne', mul_comm, Or.inl, ENNReal.coe_lt_top, LT.lt.ne
-- 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 : ℝ≥0∞) ≤ (↑‖μ[g | ℱ n] x‖₊ : ℝ≥0∞)} ≤
    HPow.hPow (β := ℝ) (eLpNorm μ[g | ℱ n] 1 μ) 1 / (↑C : ℝ≥0∞)
⊢ (μ : (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

Premises used: ENNReal.coe_le_coe
-- 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∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ ENNReal.ofReal δ

Tactic:
this.trans ?_

Premises used: LE.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
n : ι
this :
  (μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ HPow.hPow (β := ℝ) (eLpNorm μ[g | ℱ n] 1 μ) 1 / (↑C : ℝ≥0∞)
refine : HPow.hPow (β := ℝ) (eLpNorm μ[g | ℱ n] 1 μ) 1 / (↑C : ℝ≥0∞) ≤ ENNReal.ofReal δ
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ ENNReal.ofReal δ

Tactic:
refine this.trans ?_

Premises used: LE.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
n : ι
this :
  (μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ HPow.hPow (β := ℝ) (eLpNorm μ[g | ℱ n] 1 μ) 1 / (↑C : ℝ≥0∞)
rw : eLpNorm μ[g | ℱ n] 1 μ ≤ eLpNorm g 1 μ
⊢ HPow.hPow (β := ℝ) (eLpNorm μ[g | ℱ n] 1 μ) 1 / (↑C : ℝ≥0∞) ≤ ENNReal.ofReal δ

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]

Premises used: ENNReal.coe_toNNReal, Iff.mpr, mul_inv_cancel₀, ENNReal.ofReal_mul, mul_assoc, ENNReal.rpow_one, ENNReal.div_le_iff_le_mul, LT.lt.le, ENNReal.ofReal_one, ENNReal.coe_ne_zero, LT.lt.ne', ENNReal.coe_mul, ENNReal.ofReal_eq_coe_nnreal, MeasureTheory.MemLp.eLpNorm_lt_top, Or.inl, one_mul, NNReal.inv_mk, ENNReal.coe_lt_top, LT.lt.ne
-- 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:
eLpNorm_one_condExp_le_eLpNorm _

Premises used: MeasureTheory.eLpNorm_one_condExp_le_eLpNorm