awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : StandardBorelSpace Ω
Y : ℕ → Ω → ℝ
cY : ℕ → ℝ≥0
ℱ : Filtration ℕ mΩ
inst_1 : IsZeroOrProbabilityMeasure μ
h_adapted : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ Y
h0 : HasSubgaussianMGF (Y 0) (cY 0) μ
n : ℕ
h :
  ∀
    (hn :
      ∀ (h_subG : ∀ i < n - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
        HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ)
    (h_subG : ∀ i < n + 1 - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ
h_subG : ∀ i < n + 1 + 1 - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ
hn : HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1 + 1), Y i ω) (∑ i ∈ Finset.range (n + 1 + 1), cY i) μ
have succ : HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω + Y (n + 1) ω)
  (∑ i ∈ Finset.range (n + 1), cY i + cY (n + 1)) μ
Tactic: simp_rw [Finset.sum_range_succ _ (n + 1)]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : StandardBorelSpace Ω
Y : ℕ → Ω → ℝ
cY : ℕ → ℝ≥0
ℱ : Filtration ℕ mΩ
inst_1 : IsZeroOrProbabilityMeasure μ
h_adapted : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ Y
h0 : HasSubgaussianMGF (Y 0) (cY 0) μ
n : ℕ
h :
  ∀
    (hn :
      ∀ (h_subG : ∀ i < n - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
        HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ)
    (h_subG : ∀ i < n + 1 - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ
h_subG : ∀ i < n + 1 + 1 - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ
hn : HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω + Y (n + 1) ω)
    (∑ i ∈ Finset.range (n + 1), cY i + cY (n + 1)) μ
have succ : HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) (μ.trim sorry)
Tactic: refine HasSubgaussianMGF.add_of_hasCondSubgaussianMGF (ℱ.le n) ?_ (h_subG n (by lia))
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : StandardBorelSpace Ω
Y : ℕ → Ω → ℝ
cY : ℕ → ℝ≥0
ℱ : Filtration ℕ mΩ
inst_1 : IsZeroOrProbabilityMeasure μ
h_adapted : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ Y
h0 : HasSubgaussianMGF (Y 0) (cY 0) μ
n : ℕ
h :
  ∀
    (hn :
      ∀ (h_subG : ∀ i < n - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
        HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ)
    (h_subG : ∀ i < n + 1 - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ
h_subG : ∀ i < n + 1 + 1 - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ
hn : HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) (μ.trim ⋯)
have succ : Measurable (β := ℝ) fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω
Tactic: refine HasSubgaussianMGF.trim (ℱ.le n) ?_ hn
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : StandardBorelSpace Ω
Y : ℕ → Ω → ℝ
cY : ℕ → ℝ≥0
ℱ : Filtration ℕ mΩ
inst_1 : IsZeroOrProbabilityMeasure μ
h_adapted : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ Y
h0 : HasSubgaussianMGF (Y 0) (cY 0) μ
n : ℕ
h :
  ∀
    (hn :
      ∀ (h_subG : ∀ i < n - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
        HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ)
    (h_subG : ∀ i < n + 1 - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ
h_subG : ∀ i < n + 1 + 1 - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ
hn : HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ
⊢ Measurable (β := ℝ) fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω
have succ : ∀ (m : ℕ) (hm : m ∈ Finset.range (n + 1)), m ≤ n
Tactic: refine Finset.measurable_fun_sum (Finset.range (n + 1)) fun m hm ↦
        ((h_adapted m).mono (ℱ.mono ?_)).measurable
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : StandardBorelSpace Ω
Y : ℕ → Ω → ℝ
cY : ℕ → ℝ≥0
ℱ : Filtration ℕ mΩ
inst_1 : IsZeroOrProbabilityMeasure μ
h_adapted : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ Y
h0 : HasSubgaussianMGF (Y 0) (cY 0) μ
n : ℕ
h :
  ∀
    (hn :
      ∀ (h_subG : ∀ i < n - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
        HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ)
    (h_subG : ∀ i < n + 1 - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ
h_subG : ∀ i < n + 1 + 1 - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ
hn : HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ
m : ℕ
hm : m ∈ Finset.range (n + 1)
⊢ m ≤ n
have hm₁ : m < n + 1
Tactic: simp only [Finset.mem_range] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : StandardBorelSpace Ω
Y : ℕ → Ω → ℝ
cY : ℕ → ℝ≥0
ℱ : Filtration ℕ mΩ
inst_1 : IsZeroOrProbabilityMeasure μ
h_adapted : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ Y
h0 : HasSubgaussianMGF (Y 0) (cY 0) μ
n : ℕ
hn :
  ∀ (h_subG : ∀ i < n - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ
h_subG : ∀ i < n + 1 - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ
have succ : ∀
  (hn :
    ∀
      (h_subG :
        ∀ i < HSub.hSub (α := ℕ) 0 1,
          HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) sorry (Y (i + 1)) (cY (i + 1)) μ),
      HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range 0, Y i ω) (∑ i ∈ Finset.range 0, cY i) μ)
  (h_subG :
    ∀ i < HAdd.hAdd (α := ℕ) 0 1 - 1,
      HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) sorry (Y (i + 1)) (cY (i + 1)) μ),
  HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), Y i ω)
    (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), cY i) μ
Tactic: induction n with
    | zero => simp [h0]
    | succ n =>
      specialize hn fun i hi ↦ h_subG i (by lia)
      simp_rw [Finset.sum_range_succ _ (n + 1)]
      refine HasSubgaussianMGF.add_of_hasCondSubgaussianMGF (ℱ.le n) ?_ (h_subG n (by lia))
      refine HasSubgaussianMGF.trim (ℱ.le n) ?_ hn
      refine Finset.measurable_fun_sum (Finset.range (n + 1)) fun m hm ↦
        ((h_adapted m).mono (ℱ.mono ?_)).measurable
      simp only [Finset.mem_range] at hm
      lia
Cleared hypotheses: n, hn, h_subG
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : StandardBorelSpace Ω
Y : ℕ → Ω → ℝ
cY : ℕ → ℝ≥0
ℱ : Filtration ℕ mΩ
inst_1 : IsZeroOrProbabilityMeasure μ
h_adapted : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ Y
h0 : HasSubgaussianMGF (Y 0) (cY 0) μ
n : ℕ
hn :
  ∀ (h_subG : ∀ i < n - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ
h_subG : ∀ i < n + 1 - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ
succ :
  ∀
    (hn :
      ∀
        (h_subG :
          ∀ i < HSub.hSub (α := ℕ) 0 1,
            HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
        HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range 0, Y i ω) (∑ i ∈ Finset.range 0, cY i) μ)
    (h_subG :
      ∀ i < HAdd.hAdd (α := ℕ) 0 1 - 1,
        HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), Y i ω)
      (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), cY i) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ
have succ₁ : ∀ (n : ℕ),
  (∀
      (hn :
        ∀ (h_subG : ∀ i < n - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) sorry (Y (i + 1)) (cY (i + 1)) μ),
          HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ)
      (h_subG : ∀ i < n + 1 - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) sorry (Y (i + 1)) (cY (i + 1)) μ),
      HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ) →
    ∀
      (hn :
        ∀
          (h_subG :
            ∀ i < n + 1 - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) sorry (Y (i + 1)) (cY (i + 1)) μ),
          HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ)
      (h_subG :
        ∀ i < n + 1 + 1 - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) sorry (Y (i + 1)) (cY (i + 1)) μ),
      HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1 + 1), Y i ω) (∑ i ∈ Finset.range (n + 1 + 1), cY i) μ
Tactic: induction n with
    | zero => simp [h0]
    | succ n =>
      specialize hn fun i hi ↦ h_subG i (by lia)
      simp_rw [Finset.sum_range_succ _ (n + 1)]
      refine HasSubgaussianMGF.add_of_hasCondSubgaussianMGF (ℱ.le n) ?_ (h_subG n (by lia))
      refine HasSubgaussianMGF.trim (ℱ.le n) ?_ hn
      refine Finset.measurable_fun_sum (Finset.range (n + 1)) fun m hm ↦
        ((h_adapted m).mono (ℱ.mono ?_)).measurable
      simp only [Finset.mem_range] at hm
      lia
Cleared hypotheses: n, hn, h_subG
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : StandardBorelSpace Ω
Y : ℕ → Ω → ℝ
cY : ℕ → ℝ≥0
ℱ : Filtration ℕ mΩ
inst_1 : IsZeroOrProbabilityMeasure μ
h_adapted : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ Y
h0 : HasSubgaussianMGF (Y 0) (cY 0) μ
n : ℕ
h_subG : ∀ i < n - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ
have zero : ∀
  (h_subG :
    ∀ i < HSub.hSub (α := ℕ) 0 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) sorry (Y (i + 1)) (cY (i + 1)) μ),
  HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range 0, Y i ω) (∑ i ∈ Finset.range 0, cY i) μ
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    induction n with
    | zero => simp [h0]
    | succ n =>
      specialize hn fun i hi ↦ h_subG i (by lia)
      simp_rw [Finset.sum_range_succ _ (n + 1)]
      refine HasSubgaussianMGF.add_of_hasCondSubgaussianMGF (ℱ.le n) ?_ (h_subG n (by lia))
      refine HasSubgaussianMGF.trim (ℱ.le n) ?_ hn
      refine Finset.measurable_fun_sum (Finset.range (n + 1)) fun m hm ↦
        ((h_adapted m).mono (ℱ.mono ?_)).measurable
      simp only [Finset.mem_range] at hm
      lia
Cleared hypotheses: n, h_subG
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : StandardBorelSpace Ω
Y : ℕ → Ω → ℝ
cY : ℕ → ℝ≥0
ℱ : Filtration ℕ mΩ
inst_1 : IsZeroOrProbabilityMeasure μ
h_adapted : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ Y
h0 : HasSubgaussianMGF (Y 0) (cY 0) μ
n : ℕ
h_subG : ∀ i < n - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ
zero :
  ∀
    (h_subG :
      ∀ i < HSub.hSub (α := ℕ) 0 1,
        HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range 0, Y i ω) (∑ i ∈ Finset.range 0, cY i) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ
have succ : ∀ (n : ℕ)
  (hn :
    ∀ (h_subG : ∀ i < n - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) sorry (Y (i + 1)) (cY (i + 1)) μ),
      HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ)
  (h_subG : ∀ i < n + 1 - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) sorry (Y (i + 1)) (cY (i + 1)) μ),
  HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    induction n with
    | zero => simp [h0]
    | succ n =>
      specialize hn fun i hi ↦ h_subG i (by lia)
      simp_rw [Finset.sum_range_succ _ (n + 1)]
      refine HasSubgaussianMGF.add_of_hasCondSubgaussianMGF (ℱ.le n) ?_ (h_subG n (by lia))
      refine HasSubgaussianMGF.trim (ℱ.le n) ?_ hn
      refine Finset.measurable_fun_sum (Finset.range (n + 1)) fun m hm ↦
        ((h_adapted m).mono (ℱ.mono ?_)).measurable
      simp only [Finset.mem_range] at hm
      lia
Cleared hypotheses: n, h_subG
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / mgf X μ t) ∂μ
have rw : ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / ∫ (x : Ω), rexp (t * X x) ∂μ) ∂μ =
  ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / mgf X μ t) ∂μ
Tactic: rw [tilted_apply' _ _ hs, mgf]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
rw :
  ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / ∫ (x : Ω), rexp (t * X x) ∂μ) ∂μ =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / mgf X μ t) ∂μ
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / mgf X μ t) ∂μ
have rw₁ : ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / ∫ (x : Ω), rexp (t * X x) ∂μ) ∂μ =
  ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ) ∂μ
Tactic: rw [tilted_apply' _ _ hs, mgf]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst : SFinite μ
s : Set Ω
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / mgf X μ t) ∂μ
have rw : ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / ∫ (x : Ω), rexp (t * X x) ∂μ) ∂μ =
  ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / mgf X μ t) ∂μ
Tactic: rw [tilted_apply, mgf]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst : SFinite μ
s : Set Ω
rw :
  ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / ∫ (x : Ω), rexp (t * X x) ∂μ) ∂μ =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / mgf X μ t) ∂μ
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / mgf X μ t) ∂μ
have rw₁ : ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / ∫ (x : Ω), rexp (t * X x) ∂μ) ∂μ =
  ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ) ∂μ
Tactic: rw [tilted_apply, mgf]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a - cgf X μ t)) ∂μ
have inl : ∀ (ht : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) 0),
  ((Measure.tilted 0 fun (x : Ω) ↦ t * X x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a - cgf (m := mΩ) X 0 t)) ∂0
Tactic: rcases eq_zero_or_neZero μ with rfl | hμ
Cleared hypotheses: μ, ht
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
inl :
  ∀ (ht : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) 0),
    ((Measure.tilted 0 fun (x : Ω) ↦ t * X x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
      ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a - cgf (m := mΩ) X 0 t)) ∂0
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a - cgf X μ t)) ∂μ
have inr : ∀ (hμ : NeZero μ),
  (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a - cgf X μ t)) ∂μ
Tactic: rcases eq_zero_or_neZero μ with rfl | hμ
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a - cgf X μ t)) ∂μ
have inr : ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / mgf X μ t) ∂μ =
  ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a - cgf X μ t)) ∂μ
Tactic: simp_rw [tilted_mul_apply_mgf' hs, exp_sub, exp_cgf ht]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hμ : NeZero μ
inr :
  ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / mgf X μ t) ∂μ =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a - cgf X μ t)) ∂μ
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a - cgf X μ t)) ∂μ
have inr₁ : ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / mgf X μ t) ∂μ =
  ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / rexp (cgf X μ t)) ∂μ
Tactic: simp_rw [tilted_mul_apply_mgf' hs, exp_sub, exp_cgf ht]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst : SFinite μ
s : Set Ω
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a - cgf X μ t)) ∂μ
have inl : ∀ [SFinite.{u_1} (α := Ω) (m0 := mΩ) 0] (ht : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) 0),
  ((Measure.tilted 0 fun (x : Ω) ↦ t * X x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a - cgf (m := mΩ) X 0 t)) ∂0
Tactic: rcases eq_zero_or_neZero μ with rfl | hμ
Cleared hypotheses: μ, inst, ht
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst : SFinite μ
s : Set Ω
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
inl :
  ∀ [SFinite.{u_1} (α := Ω) (m0 := mΩ) 0] (ht : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) 0),
    ((Measure.tilted 0 fun (x : Ω) ↦ t * X x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
      ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a - cgf (m := mΩ) X 0 t)) ∂0
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a - cgf X μ t)) ∂μ
have inr : ∀ (hμ : NeZero μ),
  (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a - cgf X μ t)) ∂μ
Tactic: rcases eq_zero_or_neZero μ with rfl | hμ
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst : SFinite μ
s : Set Ω
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a - cgf X μ t)) ∂μ
have inr : ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / mgf X μ t) ∂μ =
  ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a - cgf X μ t)) ∂μ
Tactic: simp_rw [tilted_mul_apply_mgf s, exp_sub, exp_cgf ht]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst : SFinite μ
s : Set Ω
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hμ : NeZero μ
inr :
  ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / mgf X μ t) ∂μ =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a - cgf X μ t)) ∂μ
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a - cgf X μ t)) ∂μ
have inr₁ : ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / mgf X μ t) ∂μ =
  ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / rexp (cgf X μ t)) ∂μ
Tactic: simp_rw [tilted_mul_apply_mgf s, exp_sub, exp_cgf ht]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ)
have rw : ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / ∫ (x : Ω), rexp (t * X x) ∂μ ∂μ) =
  ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ)
Tactic: rw [tilted_apply_eq_ofReal_integral' _ hs, mgf]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
rw :
  ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / ∫ (x : Ω), rexp (t * X x) ∂μ ∂μ) =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ)
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ)
have rw₁ : ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / ∫ (x : Ω), rexp (t * X x) ∂μ ∂μ) =
  ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ ∂μ)
Tactic: rw [tilted_apply_eq_ofReal_integral' _ hs, mgf]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst : SFinite μ
s : Set Ω
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ)
have rw : ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / ∫ (x : Ω), rexp (t * X x) ∂μ ∂μ) =
  ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ)
Tactic: rw [tilted_apply_eq_ofReal_integral _ s, mgf]