awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 : ℕ
pos :
  ENNReal.ofReal ((b - a) * ∫ (a_1 : Ω), (↑(↑(upcrossingsBefore a b f N a_1) : ℝ≥0) : ℝ) ∂μ) ≤
    ⨆ (N : ℕ), ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
⊢ ENNReal.ofReal (b - a) * ∫⁻ (a_1 : Ω), (↑(upcrossingsBefore a b f N a_1) : ℝ≥0∞) ∂μ ≤
    ⨆ (N : ℕ), ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
have pos₁ : Integrable (ε := ℝ) (fun (x : Ω) ↦ (↑(↑(upcrossingsBefore a b f N x) : ℝ≥0) : ℝ)) μ
Tactic: rw [(by simp :
          ∫⁻ ω, upcrossingsBefore a b f N ω ∂μ = ∫⁻ ω, ↑(upcrossingsBefore a b f N ω : ℝ≥0) ∂μ),
        lintegral_coe_eq_integral, ← ENNReal.ofReal_mul (sub_pos.2 hab).le]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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)⁺ ∂μ)
⊢ ∀ᵐ (x : Ω) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ (↑(upcrossingsBefore a b f n x) : ℝ≥0∞)
have 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)
Tactic: filter_upwards with ω N M hNM
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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
⊢ LE.le (α := ℝ≥0∞) ((fun (n : ℕ) ↦ ((↑(upcrossingsBefore a b f n ω) : ℝ≥0∞) : ℝ≥0∞)) N)
    ((fun (n : ℕ) ↦ ((↑(upcrossingsBefore a b f n ω) : ℝ≥0∞) : ℝ≥0∞)) M)
have pos : upcrossingsBefore a b f N ω ≤ upcrossingsBefore a b f M ω
Tactic: rw [Nat.cast_le]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : b ≤ a
⊢ ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
have hab₁ : b - a ≤ 0
Tactic: rw [← sub_nonpos] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : b - a ≤ 0
⊢ ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
have neg : LE.le (α := ℝ≥0∞) 0 (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ)
Tactic: rw [ENNReal.ofReal_of_nonpos hab, zero_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
h_int : Integrable X μ
⊢ centralMoment X 1 μ = (1 - μ.real Set.univ) * ∫ (x : Ω), X x ∂μ
have simp : ∫ (x : Ω), X x - ∫ (x : Ω), X x ∂μ ∂μ = (1 - μ.real Set.univ) * ∫ (x : Ω), X x ∂μ
Tactic: simp only [centralMoment, Pi.sub_apply, pow_one]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
h_int : Integrable X μ
⊢ ∫ (x : Ω), X x - ∫ (x : Ω), X x ∂μ ∂μ = (1 - μ.real Set.univ) * ∫ (x : Ω), X x ∂μ
have rw : HSub.hSub (α := ℝ) (∫ (a : Ω), X a ∂μ) (∫ (a : Ω), ∫ (x : Ω), X x ∂μ ∂μ) = (1 - μ.real Set.univ) * ∫ (x : Ω), X x ∂μ
Tactic: rw [integral_sub h_int (integrable_const _)]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
⊢ centralMoment X 1 μ = 0
have inl : ∀ [IsZeroOrProbabilityMeasure.{u_1} (α := Ω) (m0 := m) 0], centralMoment (m := m) X 1 0 = 0
Tactic: rcases eq_zero_or_isProbabilityMeasure μ with rfl | h
Cleared hypotheses: μ, inst
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
inl : ∀ [IsZeroOrProbabilityMeasure.{u_1} (α := Ω) (m0 := m) 0], centralMoment (m := m) X 1 0 = 0
⊢ centralMoment X 1 μ = 0
have inr : ∀ (h : IsProbabilityMeasure μ), centralMoment X 1 μ = 0
Tactic: rcases eq_zero_or_isProbabilityMeasure μ with rfl | h
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
⊢ centralMoment X 1 μ = 0
have pos : ∀ (h_int : Integrable X μ), centralMoment X 1 μ = 0
Tactic: by_cases h_int : Integrable X μ
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
pos : ∀ (h_int : Integrable X μ), centralMoment X 1 μ = 0
⊢ centralMoment X 1 μ = 0
have neg : ∀ (h_int : ¬Integrable X μ), centralMoment X 1 μ = 0
Tactic: by_cases h_int : Integrable X μ
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : Integrable X μ
⊢ centralMoment X 1 μ = 0
have pos : (1 - μ.real Set.univ) * ∫ (x : Ω), X x ∂μ = 0
Tactic: rw [centralMoment_one' h_int]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
⊢ centralMoment X 1 μ = 0
have neg : Eq (α := ℝ) (∫ (x : Ω), X x - ∫ (x : Ω), X x ∂μ ∂μ) 0
Tactic: simp only [centralMoment, Pi.sub_apply, pow_one]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
⊢ ¬Integrable (ε := ℝ) (fun (x : Ω) ↦ X x - integral μ X) μ
have refine : ∀ (h_sub : Integrable (ε := ℝ) (fun (x : Ω) ↦ X x - integral μ X) μ), Integrable X μ
Tactic: refine fun h_sub => h_int ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
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
have h₁ : ∀ (x : Ω),
  X x = HAdd.hAdd (α := (x : Ω) → ℝ) (β := Ω → ℝ) (fun (x : Ω) ↦ X x - integral μ X) (fun (x : Ω) ↦ integral μ X) x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (hypothesis)
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) μ
⊢ Integrable X μ
have h_add : 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
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
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
⊢ Integrable X μ
have rw : Integrable (HAdd.hAdd (α := (x : Ω) → ℝ) (fun (x : Ω) ↦ X x - integral μ X) fun (x : Ω) ↦ integral μ X) μ
Tactic: rw [h_add]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
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
⊢ Integrable (HAdd.hAdd (α := (x : Ω) → ℝ) (fun (x : Ω) ↦ X x - integral μ X) fun (x : Ω) ↦ integral μ X) μ
have funProp : ‖integral μ X‖ₑ ≠ ∞
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
⊢ Eq (α := ℝ) (∫ (x : Ω), X x - ∫ (x : Ω), X x ∂μ ∂μ) 0
have this : ¬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
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
this : ¬Integrable (ε := ℝ) (fun (x : Ω) ↦ X x - integral μ X) μ
⊢ Eq (α := ℝ) (∫ (x : Ω), X x - ∫ (x : Ω), X x ∂μ ∂μ) 0
have neg : Eq (α := ℝ) 0 0
Tactic: rw [integral_undef this]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
p : ℕ
μ : Measure Ω
X Y : Ω → ℝ
hXY : X =ᶠ[ae μ] Y
⊢ centralMoment X p μ = centralMoment Y p μ
have simp : Eq (α := ℝ) (∫ (x : Ω), ((X - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p) x ∂μ)
  (∫ (x : Ω), ((Y - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p) x ∂μ)
Tactic: simp only [centralMoment, integral_congr_ae hXY]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
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 ∂μ)
have refine : (X - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p =ᶠ[ae μ] (Y - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p
Tactic: refine integral_congr_ae ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
p : ℕ
μ : Measure Ω
X Y : Ω → ℝ
hXY : X =ᶠ[ae μ] Y
⊢ (X - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p =ᶠ[ae μ] (Y - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p
have 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
Tactic: filter_upwards [hXY] with x hx using by simp [hx]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
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
⊢ (X - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p =ᶠ[ae μ] (Y - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p
have h₁ : ∀ (a : Ω), X a = Y a → ((X - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p) a = ((Y - fun (x : Ω) ↦ ∫ (a : Ω), Y a ∂μ) ^ p) a
Tactic: filter_upwards [hXY] with x hx using by simp [hx]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
⊢ mgf (m := m) X 0 = 0
have h : ∀ (x : ℝ), mgf (m := m) X 0 x = 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
⊢ cgf (m := m) X 0 = 0
have h : ∀ (x : ℝ), cgf (m := m) X 0 x = 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ cgf (fun (x : Ω) ↦ c) μ t = log (μ.real Set.univ) + t * c
have simp : log (μ.real Set.univ * rexp (t * c)) = log (μ.real Set.univ) + t * c
Tactic: simp only [cgf, mgf_const']
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ log (μ.real Set.univ * rexp (t * c)) = log (μ.real Set.univ) + t * c
have rw : log (μ.real Set.univ) + log (rexp (t * c)) = log (μ.real Set.univ) + t * c
Tactic: rw [log_mul _ (exp_pos _).ne']
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
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
⊢ log (μ.real Set.univ * rexp (t * c)) = log (μ.real Set.univ) + t * c
have rw₁ : μ.real Set.univ ≠ 0
Tactic: rw [log_mul _ (exp_pos _).ne']
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ log (μ.real Set.univ) + log (rexp (t * c)) = log (μ.real Set.univ) + t * c
have rw : log (μ.real Set.univ) + t * c = log (μ.real Set.univ) + t * c
Tactic: rw [log_exp _]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ μ.real Set.univ ≠ 0
have rw : ¬μ = 0
Tactic: rw [Ne, measureReal_eq_zero_iff, Measure.measure_univ_eq_zero]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
⊢ cgf X μ 0 = 0
have inl : ∀ [IsZeroOrProbabilityMeasure.{u_1} (α := Ω) (m0 := m) 0], cgf (m := m) X 0 0 = 0
Tactic: rcases eq_zero_or_isProbabilityMeasure μ with rfl | h
Cleared hypotheses: μ, inst
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
inl : ∀ [IsZeroOrProbabilityMeasure.{u_1} (α := Ω) (m0 := m) 0], cgf (m := m) X 0 0 = 0
⊢ cgf X μ 0 = 0
have inr : ∀ (h : IsProbabilityMeasure μ), cgf X μ 0 = 0
Tactic: rcases eq_zero_or_isProbabilityMeasure μ with rfl | h
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ LT.lt (α := ℝ) 0 (∫ (x : Ω), rexp (t * X x) ∂μ)
have this : Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)
Tactic: have : ∫ x : Ω, exp (t * X x) ∂μ = ∫ x : Ω in Set.univ, exp (t * X x) ∂μ := by
    simp only [Measure.restrict_univ]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
this : Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)
⊢ LT.lt (α := ℝ) 0 (∫ (x : Ω), rexp (t * X x) ∂μ)
have rw : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
  ((μ : (a : Set Ω) → ℝ≥0∞) ((Function.support (M := ℝ) fun (x : Ω) ↦ rexp (t * X x)) ∩ Set.univ) : ℝ≥0∞)
Tactic: rw [this, setIntegral_pos_iff_support_of_nonneg_ae _ _]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
this : Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)
rw :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) ((Function.support (M := ℝ) fun (x : Ω) ↦ rexp (t * X x)) ∩ Set.univ) : ℝ≥0∞)
⊢ LT.lt (α := ℝ) 0 (∫ (x : Ω), rexp (t * X x) ∂μ)
have rw₁ : (ae (μ.restrict Set.univ)).EventuallyLE (β := ℝ) 0 fun (x : Ω) ↦ rexp (t * X x)
Tactic: rw [this, setIntegral_pos_iff_support_of_nonneg_ae _ _]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
this : Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)
rw :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) ((Function.support (M := ℝ) fun (x : Ω) ↦ rexp (t * X x)) ∩ Set.univ) : ℝ≥0∞)
rw₁ : (ae (μ.restrict Set.univ)).EventuallyLE (β := ℝ) 0 fun (x : Ω) ↦ rexp (t * X x)
⊢ LT.lt (α := ℝ) 0 (∫ (x : Ω), rexp (t * X x) ∂μ)
have rw₂ : IntegrableOn (ε := ℝ) (fun (x : Ω) ↦ rexp (t * X x)) Set.univ μ
Tactic: rw [this, setIntegral_pos_iff_support_of_nonneg_ae _ _]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
this : Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)
⊢ Eq.{u_1 + 1} (α := Set Ω) (Function.support (M := ℝ) fun (x : Ω) ↦ rexp (t * X x)) Set.univ
have h : ∀ (x : Ω),
  Membership.mem (γ := Set Ω) (Function.support (M := ℝ) fun (x : Ω) ↦ rexp (t * X x)) x ↔
    Membership.mem (γ := Set Ω) Set.univ x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
this : Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)
x : Ω
⊢ Membership.mem (γ := Set Ω) (Function.support (M := ℝ) fun (x : Ω) ↦ rexp (t * X x)) x ↔
    Membership.mem (γ := Set Ω) Set.univ x
have h : rexp (t * X x) ≠ 0
Tactic: simp only [Function.mem_support, Set.mem_univ, iff_true]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
this : Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) ((Function.support (M := ℝ) fun (x : Ω) ↦ rexp (t * X x)) ∩ Set.univ) : ℝ≥0∞)
have h_eq_univ : Eq.{u_1 + 1} (α := Set Ω) (Function.support (M := ℝ) fun (x : Ω) ↦ rexp (t * X x)) Set.univ
Tactic: have h_eq_univ : (Function.support fun x : Ω => exp (t * X x)) = Set.univ := by
      ext1 x
      simp only [Function.mem_support, Set.mem_univ, iff_true]
      exact (exp_pos _).ne'
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
this : Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)
h_eq_univ : Eq.{u_1 + 1} (α := Set Ω) (Function.support (M := ℝ) fun (x : Ω) ↦ rexp (t * X x)) Set.univ
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) ((Function.support (M := ℝ) fun (x : Ω) ↦ rexp (t * X x)) ∩ Set.univ) : ℝ≥0∞)
have rw : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
Tactic: rw [h_eq_univ, Set.inter_univ _]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
this : Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)
h_eq_univ : Eq.{u_1 + 1} (α := Set Ω) (Function.support (M := ℝ) fun (x : Ω) ↦ rexp (t * X x)) Set.univ
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
have refine : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (⊥ : ℝ≥0∞)
Tactic: refine Ne.bot_lt ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
this : Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)
⊢ (ae (μ.restrict Set.univ)).EventuallyLE (β := ℝ) 0 fun (x : Ω) ↦ rexp (t * X x)
have h : ∀ (x : Ω), 0 x ≤ rexp (t * X x)
Tactic: filter_upwards with x
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : NeZero μ
⊢ 0 < mgf X μ t ↔ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
have refine : ∀ (h : 0 < mgf X μ t), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ mgf_pos' hμ.out h⟩
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : NeZero μ
h : 0 < mgf X μ t
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
have contrapose! : ∀ (h : ¬Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ), mgf X μ t ≤ 0
Tactic: contrapose! h with h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : NeZero μ
hX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ rexp (cgf X μ t) = mgf X μ t
have rw : rexp (log (mgf X μ t)) = mgf X μ t
Tactic: rw [cgf, exp_log (mgf_pos' hμ.out hX)]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : NeZero μ
hX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
rw : rexp (log (mgf X μ t)) = mgf X μ t
⊢ rexp (cgf X μ t) = mgf X μ t
have rw₁ : mgf X μ t = mgf X μ t
Tactic: rw [cgf, exp_log (mgf_pos' hμ.out hX)]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
X : Ω → ℝ
hY : AEMeasurable Y μ
t : ℝ
hX : AEStronglyMeasurable (β := ℝ) (m₀ := m) (fun (ω : Ω) ↦ rexp (t * X ω)) (Measure.map Y μ)
⊢ mgf (m := m) X (Measure.map Y μ) t = mgf (X ∘ Y) μ t
have simp_rw : Eq (α := ℝ) (@integral _ _ _ _ m (Measure.map Y μ) fun (x : Ω) ↦ rexp (t * X x)) (∫ (x : Ω'), rexp (t * (X ∘ Y) x) ∂μ)
Tactic: simp_rw [mgf, integral_map hY hX, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
X : Ω → ℝ
hY : AEMeasurable Y μ
t : ℝ
hX : AEStronglyMeasurable (β := ℝ) (m₀ := m) (fun (ω : Ω) ↦ rexp (t * X ω)) (Measure.map Y μ)
simp_rw :
  Eq (α := ℝ) (@integral _ _ _ _ m (Measure.map Y μ) fun (x : Ω) ↦ rexp (t * X x)) (∫ (x : Ω'), rexp (t * (X ∘ Y) x) ∂μ)
⊢ mgf (m := m) X (Measure.map Y μ) t = mgf (X ∘ Y) μ t
have simp_rw₁ : Eq (α := ℝ) (∫ (x : Ω'), rexp (t * X (Y x)) ∂μ) (∫ (x : Ω'), rexp (t * (X ∘ Y) x) ∂μ)
Tactic: simp_rw [mgf, integral_map hY hX, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
⊢ mgf (m := measurableSpace) id (Measure.map X μ) = mgf X μ
have h : ∀ (t : ℝ), mgf (m := measurableSpace) id (Measure.map X μ) t = mgf X μ t
Tactic: ext t
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℝ
⊢ mgf (m := measurableSpace) id (Measure.map X μ) t = mgf X μ t
have h : AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (ω : ℝ) ↦ rexp (t * id ω)) (Measure.map X μ)
Tactic: rw [mgf_map hX, Function.id_comp]