awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
N : ℕ
⊢ ENNReal.ofReal ((b - a) * ∫ (a_1 : Ω), (↑(upcrossingsBefore a b f N a_1) : ℝ) ∂μ) ≤
    ⨆ (N : ℕ), ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)

Tactic:
exact (ENNReal.ofReal_le_ofReal
          (hf.mul_integral_upcrossingsBefore_le_integral_pos_part a b N)).trans
            (le_iSup (α := ℝ≥0∞) _ N)

Premises used: MeasureTheory.Submartingale.mul_integral_upcrossingsBefore_le_integral_pos_part, ENNReal.ofReal_le_ofReal, LE.le.trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
N : ℕ
⊢ Integrable (ε := ℝ) (fun (x : Ω) ↦ (↑(↑(upcrossingsBefore a b f N x) : ℝ≥0) : ℝ)) μ

Tactic:
simp only [NNReal.coe_natCast, hf.stronglyAdapted.integrable_upcrossingsBefore hab]

Premises used: NNReal.coe_natCast, MeasureTheory.Submartingale.stronglyAdapted, MeasureTheory.StronglyAdapted.integrable_upcrossingsBefore
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
⊢ ∀ (n : ℕ), AEMeasurable (β := ℝ≥0∞) (fun (ω : Ω) ↦ (↑(upcrossingsBefore a b f n ω) : ℝ≥0∞)) μ

Tactic:
fun n => measurable_from_top.comp_aemeasurable
        (hf.stronglyAdapted.measurable_upcrossingsBefore hab).aemeasurable

Premises used: measurable_from_top, Measurable.aemeasurable, MeasureTheory.Submartingale.stronglyAdapted, MeasureTheory.StronglyAdapted.measurable_upcrossingsBefore, Measurable.comp_aemeasurable
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
⊢ ∀ (n : ℕ), AEMeasurable (β := ℝ≥0∞) (fun (ω : Ω) ↦ (↑(upcrossingsBefore a b f n ω) : ℝ≥0∞)) μ

Tactic:
exact fun n => measurable_from_top.comp_aemeasurable
        (hf.stronglyAdapted.measurable_upcrossingsBefore hab).aemeasurable

Premises used: measurable_from_top, Measurable.aemeasurable, MeasureTheory.Submartingale.stronglyAdapted, MeasureTheory.StronglyAdapted.measurable_upcrossingsBefore, Measurable.comp_aemeasurable
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
pos :
  ∀ (ω : Ω) ⦃N M : ℕ⦄ (hNM : N ≤ M),
    LE.le (α := ℝ≥0∞) ((fun (n : ℕ) ↦ ((↑(upcrossingsBefore a b f n ω) : ℝ≥0∞) : ℝ≥0∞)) N)
      ((fun (n : ℕ) ↦ ((↑(upcrossingsBefore a b f n ω) : ℝ≥0∞) : ℝ≥0∞)) M)
⊢ ∀ᵐ (x : Ω) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ (↑(upcrossingsBefore a b f n x) : ℝ≥0∞)

Tactic:
filter_upwards with ω N M hNM
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
ω : Ω
N M : ℕ
hNM : N ≤ M
pos : upcrossingsBefore a b f N ω ≤ upcrossingsBefore a b f M ω
⊢ LE.le (α := ℝ≥0∞) ((fun (n : ℕ) ↦ ((↑(upcrossingsBefore a b f n ω) : ℝ≥0∞) : ℝ≥0∞)) N)
    ((fun (n : ℕ) ↦ ((↑(upcrossingsBefore a b f n ω) : ℝ≥0∞) : ℝ≥0∞)) M)

Tactic:
rw [Nat.cast_le]

Premises used: Nat.cast_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
ω : Ω
N M : ℕ
hNM : N ≤ M
⊢ upcrossingsBefore a b f N ω ≤ upcrossingsBefore a b f M ω

Tactic:
upcrossingsBefore_mono hab hNM ω

Premises used: MeasureTheory.upcrossingsBefore_mono
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
ω : Ω
N M : ℕ
hNM : N ≤ M
⊢ upcrossingsBefore a b f N ω ≤ upcrossingsBefore a b f M ω

Tactic:
exact upcrossingsBefore_mono hab hNM ω

Premises used: MeasureTheory.upcrossingsBefore_mono
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : b ≤ a
⊢ b - a ≤ 0

Tactic:
rw [← sub_nonpos] at hab

Premises used: sub_nonpos
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : b - a ≤ 0
neg : LE.le (α := ℝ≥0∞) 0 (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ)
⊢ ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ

Tactic:
rw [ENNReal.ofReal_of_nonpos hab, zero_mul]

Premises used: MulZeroClass.zero_mul, ENNReal.ofReal_of_nonpos
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : b - a ≤ 0
⊢ LE.le (α := ℝ≥0∞) 0 (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ)

Tactic:
zero_le

Premises used: zero_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : b - a ≤ 0
⊢ LE.le (α := ℝ≥0∞) 0 (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ)

Tactic:
exact zero_le

Premises used: zero_le
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
p : ℕ
μ : Measure Ω
⊢ moment X p μ = ∫ (x : Ω), (X ^ p) x ∂μ

Tactic:
rfl

Premises used: ProbabilityTheory.moment, rfl
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
p : ℕ
μ : Measure Ω
hp : p ≠ 0
⊢ moment 0 p μ = 0

Tactic:
simp only [moment, hp, zero_pow, Ne, not_false_iff, Pi.zero_apply, integral_const,
    smul_eq_mul, mul_zero]

Premises used: Pi.zero_apply, Ne, ProbabilityTheory.moment, MulZeroClass.mul_zero, MeasureTheory.integral_const, smul_eq_mul, not_false_iff, zero_pow
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
p : ℕ
⊢ moment (m := m) X p 0 = 0

Tactic:
simp [moment]

Premises used: ProbabilityTheory.moment
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
p : ℕ
μ : Measure Ω
hp : p ≠ 0
⊢ centralMoment 0 p μ = 0

Tactic:
simp only [centralMoment, hp, Pi.zero_apply, integral_const, smul_eq_mul,
    mul_zero, zero_sub, Pi.pow_apply, Pi.neg_apply, neg_zero, zero_pow, Ne, not_false_iff]

Premises used: ProbabilityTheory.centralMoment, Pi.zero_apply, Ne, MulZeroClass.mul_zero, Pi.pow_apply, MeasureTheory.integral_const, smul_eq_mul, not_false_iff, neg_zero, Pi.neg_apply, zero_pow, zero_sub
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ moment X 1 μ = ∫ (x : Ω), X x ∂μ

Tactic:
simp [moment]

Premises used: ProbabilityTheory.moment
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
p : ℕ
⊢ centralMoment (m := m) X p 0 = 0

Tactic:
simp [centralMoment]

Premises used: ProbabilityTheory.centralMoment
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
h_int : Integrable X μ
simp : ∫ (x : Ω), X x - ∫ (x : Ω), X x ∂μ ∂μ = (1 - μ.real Set.univ) * ∫ (x : Ω), X x ∂μ
⊢ centralMoment X 1 μ = (1 - μ.real Set.univ) * ∫ (x : Ω), X x ∂μ

Tactic:
simp only [centralMoment, Pi.sub_apply, pow_one]

Premises used: ProbabilityTheory.centralMoment, pow_one, Pi.sub_apply
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
h_int : Integrable X μ
rw :
  HSub.hSub (α := ℝ) (∫ (a : Ω), X a ∂μ) (∫ (a : Ω), ∫ (x : Ω), X x ∂μ ∂μ) = (1 - μ.real Set.univ) * ∫ (x : Ω), X x ∂μ
⊢ ∫ (x : Ω), X x - ∫ (x : Ω), X x ∂μ ∂μ = (1 - μ.real Set.univ) * ∫ (x : Ω), X x ∂μ

Tactic:
rw [integral_sub h_int (integrable_const _)]

Premises used: MeasureTheory.integral_sub, MeasureTheory.integrable_const
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
h_int : Integrable X μ
⊢ HSub.hSub (α := ℝ) (∫ (a : Ω), X a ∂μ) (∫ (a : Ω), ∫ (x : Ω), X x ∂μ ∂μ) = (1 - μ.real Set.univ) * ∫ (x : Ω), X x ∂μ

Tactic:
simp only [sub_mul, integral_const, smul_eq_mul, one_mul]

Premises used: sub_mul, MeasureTheory.integral_const, smul_eq_mul, one_mul
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
inl : ∀ [IsZeroOrProbabilityMeasure.{u_1} (α := Ω) (m0 := m) 0], centralMoment (m := m) X 1 0 = 0
inr : ∀ (h : IsProbabilityMeasure μ), centralMoment X 1 μ = 0
⊢ centralMoment X 1 μ = 0

Tactic:
rcases eq_zero_or_isProbabilityMeasure μ with rfl | h

Premises used: MeasureTheory.eq_zero_or_isProbabilityMeasure, rfl
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
inst : IsZeroOrProbabilityMeasure.{u_1} (α := Ω) (m0 := m) 0
⊢ centralMoment (m := m) X 1 0 = 0

Tactic:
simp [centralMoment]

Premises used: ProbabilityTheory.centralMoment
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
pos : ∀ (h_int : Integrable X μ), centralMoment X 1 μ = 0
neg : ∀ (h_int : ¬Integrable X μ), centralMoment X 1 μ = 0
⊢ centralMoment X 1 μ = 0

Tactic:
by_cases h_int : Integrable X μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : Integrable X μ
pos : (1 - μ.real Set.univ) * ∫ (x : Ω), X x ∂μ = 0
⊢ centralMoment X 1 μ = 0

Tactic:
rw [centralMoment_one' h_int]

Premises used: ProbabilityTheory.centralMoment_one'
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : Integrable X μ
⊢ (1 - μ.real Set.univ) * ∫ (x : Ω), X x ∂μ = 0

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
neg : Eq (α := ℝ) (∫ (x : Ω), X x - ∫ (x : Ω), X x ∂μ ∂μ) 0
⊢ centralMoment X 1 μ = 0

Tactic:
simp only [centralMoment, Pi.sub_apply, pow_one]

Premises used: ProbabilityTheory.centralMoment, pow_one, Pi.sub_apply
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
⊢ ¬Integrable (ε := ℝ) (fun (x : Ω) ↦ X x - integral μ X) μ

Tactic:
fun h_sub => h_int ?_

Premises used: Not
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
refine : ∀ (h_sub : Integrable (ε := ℝ) (fun (x : Ω) ↦ X x - integral μ X) μ), Integrable X μ
⊢ ¬Integrable (ε := ℝ) (fun (x : Ω) ↦ X x - integral μ X) μ

Tactic:
refine fun h_sub => h_int ?_
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
h_sub : Integrable (ε := ℝ) (fun (x : Ω) ↦ X x - integral μ X) μ
h₁ :
  ∀ (x : Ω),
    X x = HAdd.hAdd (α := (x : Ω) → ℝ) (β := Ω → ℝ) (fun (x : Ω) ↦ X x - integral μ X) (fun (x : Ω) ↦ integral μ X) x
⊢ X = HAdd.hAdd (α := (x : Ω) → ℝ) (fun (x : Ω) ↦ X x - integral μ X) fun (x : Ω) ↦ integral μ X

Tactic:
ext1 x
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
h_sub : Integrable (ε := ℝ) (fun (x : Ω) ↦ X x - integral μ X) μ
x : Ω
⊢ X x = HAdd.hAdd (α := (x : Ω) → ℝ) (β := Ω → ℝ) (fun (x : Ω) ↦ X x - integral μ X) (fun (x : Ω) ↦ integral μ X) x

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
h_sub : Integrable (ε := ℝ) (fun (x : Ω) ↦ X x - integral μ X) μ
⊢ X = HAdd.hAdd (α := (x : Ω) → ℝ) (fun (x : Ω) ↦ X x - integral μ X) fun (x : Ω) ↦ integral μ X

Tactic:
have h_add : X = (fun x => X x - integral μ X) + fun _ => integral μ X := by ext1 x; simp
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
h_sub : Integrable (ε := ℝ) (fun (x : Ω) ↦ X x - integral μ X) μ
h_add : X = HAdd.hAdd (α := (x : Ω) → ℝ) (fun (x : Ω) ↦ X x - integral μ X) fun (x : Ω) ↦ integral μ X
rw : Integrable (HAdd.hAdd (α := (x : Ω) → ℝ) (fun (x : Ω) ↦ X x - integral μ X) fun (x : Ω) ↦ integral μ X) μ
⊢ Integrable X μ

Tactic:
rw [h_add]
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
h_sub : Integrable (ε := ℝ) (fun (x : Ω) ↦ X x - integral μ X) μ
h_add : X = HAdd.hAdd (α := (x : Ω) → ℝ) (fun (x : Ω) ↦ X x - integral μ X) fun (x : Ω) ↦ integral μ X
funProp : ‖integral μ X‖ₑ ≠ ∞
⊢ Integrable (HAdd.hAdd (α := (x : Ω) → ℝ) (fun (x : Ω) ↦ X x - integral μ X) fun (x : Ω) ↦ integral μ X) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
⊢ ¬Integrable (ε := ℝ) (fun (x : Ω) ↦ X x - integral μ X) μ

Tactic:
have : ¬Integrable (fun x => X x - integral μ X) μ := by
      refine fun h_sub => h_int ?_
      have h_add : X = (fun x => X x - integral μ X) + fun _ => integral μ X := by ext1 x; simp
      rw [h_add]
      fun_prop
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
this : ¬Integrable (ε := ℝ) (fun (x : Ω) ↦ X x - integral μ X) μ
neg neg₁ : Eq (α := ℝ) 0 0
⊢ Eq (α := ℝ) (∫ (x : Ω), X x - ∫ (x : Ω), X x ∂μ ∂μ) 0

Tactic:
rw [integral_undef this]

Premises used: MeasureTheory.integral_undef
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
⊢ centralMoment X 2 μ = Var[X; μ]

Tactic:
(variance_eq_integral hX).symm

Premises used: ProbabilityTheory.variance_eq_integral, ProbabilityTheory.centralMoment, Eq.symm
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
p : ℕ
μ : Measure Ω
X Y : Ω → ℝ
hXY : X =ᶠ[ae μ] Y
simp :
  Eq (α := ℝ) (∫ (x : Ω), ((X - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p) x ∂μ)
    (∫ (x : Ω), ((Y - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p) x ∂μ)
⊢ centralMoment X p μ = centralMoment Y p μ

Tactic:
simp only [centralMoment, integral_congr_ae hXY]

Premises used: MeasureTheory.integral_congr_ae, ProbabilityTheory.centralMoment
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
p : ℕ
μ : Measure Ω
X Y : Ω → ℝ
hXY : X =ᶠ[ae μ] Y
⊢ Eq (α := ℝ) (∫ (x : Ω), ((X - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p) x ∂μ)
    (∫ (x : Ω), ((Y - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p) x ∂μ)

Tactic:
integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
p : ℕ
μ : Measure Ω
X Y : Ω → ℝ
hXY : X =ᶠ[ae μ] Y
refine : (X - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p =ᶠ[ae μ] (Y - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p
⊢ Eq (α := ℝ) (∫ (x : Ω), ((X - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p) x ∂μ)
    (∫ (x : Ω), ((Y - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p) x ∂μ)

Tactic:
refine integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
p : ℕ
μ : Measure Ω
X Y : Ω → ℝ
hXY : X =ᶠ[ae μ] Y
x : Ω
hx : X x = Y x
⊢ ((X - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p) x = ((Y - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p) x

Tactic:
simp [hx]
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
p : ℕ
μ : Measure Ω
X Y : Ω → ℝ
hXY : X =ᶠ[ae μ] Y
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X x = Y x) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (x : Ω) ↦
                  ((X - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p) x = ((Y - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p) x)
                x}
            x}
      a
h₁ h₂ :
  ∀ (x : Ω) (hx : X x = Y x),
    ((X - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p) x = ((Y - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p) x
⊢ (X - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p =ᶠ[ae μ] (Y - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p

Tactic:
filter_upwards [hXY] with x hx using by simp [hx]
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
⊢ mgf 0 μ t = μ.real Set.univ

Tactic:
simp only [mgf, Pi.zero_apply, mul_zero, exp_zero, integral_const, smul_eq_mul, mul_one]

Premises used: Pi.zero_apply, MulZeroClass.mul_zero, MeasureTheory.integral_const, Real.exp_zero, smul_eq_mul, ProbabilityTheory.mgf, mul_one
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
⊢ cgf 0 μ t = log (μ.real Set.univ)

Tactic:
simp only [cgf, mgf_zero_fun]

Premises used: ProbabilityTheory.mgf_zero_fun, ProbabilityTheory.cgf
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
h : ∀ (x : ℝ), mgf (m := m) X 0 x = 0 x
⊢ mgf (m := m) X 0 = 0

Tactic:
ext
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
x : ℝ
⊢ mgf (m := m) X 0 x = 0 x

Tactic:
simp [mgf]

Premises used: ProbabilityTheory.mgf
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
h : ∀ (x : ℝ), cgf (m := m) X 0 x = 0 x
⊢ cgf (m := m) X 0 = 0

Tactic:
ext
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
x : ℝ
⊢ cgf (m := m) X 0 x = 0 x

Tactic:
simp [cgf]

Premises used: ProbabilityTheory.cgf
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t c : ℝ
⊢ mgf (fun (x : Ω) ↦ c) μ t = μ.real Set.univ * rexp (t * c)

Tactic:
simp only [mgf, integral_const, smul_eq_mul]

Premises used: MeasureTheory.integral_const, smul_eq_mul, ProbabilityTheory.mgf
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t c : ℝ
inst : IsProbabilityMeasure μ
⊢ mgf (fun (x : Ω) ↦ c) μ t = rexp (t * c)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
simp : log (μ.real Set.univ * rexp (t * c)) = log (μ.real Set.univ) + t * c
⊢ cgf (fun (x : Ω) ↦ c) μ t = log (μ.real Set.univ) + t * c

Tactic:
simp only [cgf, mgf_const']

Premises used: ProbabilityTheory.cgf, ProbabilityTheory.mgf_const'
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
rw : log (μ.real Set.univ) + log (rexp (t * c)) = log (μ.real Set.univ) + t * c
rw₁ : μ.real Set.univ ≠ 0
⊢ log (μ.real Set.univ * rexp (t * c)) = log (μ.real Set.univ) + t * c

Tactic:
rw [log_mul _ (exp_pos _).ne']

Premises used: LT.lt.ne', Real.log_mul, Real.exp_pos
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
rw rw₁ : log (μ.real Set.univ) + t * c = log (μ.real Set.univ) + t * c
⊢ log (μ.real Set.univ) + log (rexp (t * c)) = log (μ.real Set.univ) + t * c

Tactic:
rw [log_exp _]

Premises used: Real.log_exp
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
rw : ¬μ = 0
⊢ μ.real Set.univ ≠ 0

Tactic:
rw [Ne, measureReal_eq_zero_iff, Measure.measure_univ_eq_zero]

Premises used: Ne, MeasureTheory.Measure.measure_univ_eq_zero, MeasureTheory.measureReal_eq_zero_iff
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ ¬μ = 0

Tactic:
simp only [hμ, not_false_iff]

Premises used: not_false_iff
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst : IsProbabilityMeasure μ
c : ℝ
⊢ cgf (fun (x : Ω) ↦ c) μ t = t * c

Tactic:
simp only [cgf, mgf_const, log_exp]

Premises used: Real.log_exp, ProbabilityTheory.cgf, ProbabilityTheory.mgf_const
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ mgf X μ 0 = μ.real Set.univ

Tactic:
simp only [mgf, zero_mul, exp_zero, integral_const, smul_eq_mul, mul_one]

Premises used: MulZeroClass.zero_mul, MeasureTheory.integral_const, Real.exp_zero, smul_eq_mul, ProbabilityTheory.mgf, mul_one
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
⊢ mgf X μ 0 = 1

Tactic:
simp [mgf_zero']

Premises used: ProbabilityTheory.mgf_zero'
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ cgf X μ 0 = log (μ.real Set.univ)

Tactic:
simp only [cgf, mgf_zero']

Premises used: ProbabilityTheory.cgf, ProbabilityTheory.mgf_zero'
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
inl : ∀ [IsZeroOrProbabilityMeasure.{u_1} (α := Ω) (m0 := m) 0], cgf (m := m) X 0 0 = 0
inr : ∀ (h : IsProbabilityMeasure μ), cgf X μ 0 = 0
⊢ cgf X μ 0 = 0

Tactic:
rcases eq_zero_or_isProbabilityMeasure μ with rfl | h

Premises used: MeasureTheory.eq_zero_or_isProbabilityMeasure, rfl
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
inst : IsZeroOrProbabilityMeasure.{u_1} (α := Ω) (m0 := m) 0
⊢ cgf (m := m) X 0 0 = 0

Tactic:
simp [cgf_zero']

Premises used: ProbabilityTheory.cgf_zero'
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
⊢ cgf X μ 0 = 0

Tactic:
simp [cgf_zero']

Premises used: ProbabilityTheory.cgf_zero'