awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.SubGaussian
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) μ
⊢ n < n + 1 + 1 - 1

Tactic:
lia
-- Module: Mathlib.Probability.Moments.SubGaussian
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) μ
succ : HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) (μ.trim ⋯)
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω + Y (n + 1) ω)
    (∑ i ∈ Finset.range (n + 1), cY i + cY (n + 1)) μ

Tactic:
refine HasSubgaussianMGF.add_of_hasCondSubgaussianMGF (ℱ.le n) ?_ (h_subG n (by lia))

Premises used: ProbabilityTheory.HasSubgaussianMGF.add_of_hasCondSubgaussianMGF, MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Moments.SubGaussian
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 ⋯)

Tactic:
HasSubgaussianMGF.trim (ℱ.le n) ?_ hn

Premises used: ProbabilityTheory.HasSubgaussianMGF.trim, MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Moments.SubGaussian
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) μ
succ : Measurable (β := ℝ) fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) (μ.trim ⋯)

Tactic:
refine HasSubgaussianMGF.trim (ℱ.le n) ?_ hn

Premises used: ProbabilityTheory.HasSubgaussianMGF.trim, MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Moments.SubGaussian
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 ω

Tactic:
Finset.measurable_fun_sum (Finset.range (n + 1)) fun m hm ↦
        ((h_adapted m).mono (ℱ.mono ?_)).measurable

Premises used: MeasureTheory.StronglyMeasurable.measurable, Finset.range, HAdd.hAdd, MeasureTheory.StronglyMeasurable.mono, Finset.measurable_fun_sum, MeasureTheory.Filtration.mono, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.SubGaussian
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) μ
succ : ∀ (m : ℕ) (hm : m ∈ Finset.range (n + 1)), m ≤ n
⊢ Measurable (β := ℝ) fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω

Tactic:
refine Finset.measurable_fun_sum (Finset.range (n + 1)) fun m hm ↦
        ((h_adapted m).mono (ℱ.mono ?_)).measurable

Premises used: MeasureTheory.StronglyMeasurable.measurable, Finset.range, HAdd.hAdd, MeasureTheory.StronglyMeasurable.mono, Finset.measurable_fun_sum, MeasureTheory.Filtration.mono, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.SubGaussian
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 + 1

Tactic:
simp only [Finset.mem_range] at hm

Premises used: Finset.mem_range
-- Module: Mathlib.Probability.Moments.SubGaussian
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 < n + 1
⊢ m ≤ n

Tactic:
lia
-- Module: Mathlib.Probability.Moments.SubGaussian
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) μ
succ :
  ∀ (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) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, 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

Premises used: MeasureTheory.StronglyMeasurable.measurable, Finset.mem_range, Finset.range, HAdd.hAdd, MeasureTheory.StronglyMeasurable.mono, ProbabilityTheory.HasSubgaussianMGF.add_of_hasCondSubgaussianMGF, Finset.measurable_fun_sum, MeasureTheory.Filtration.mono, MeasureTheory.Filtration.le, ProbabilityTheory.HasSubgaussianMGF.zero, OfNat.ofNat, Finset.sum_range_succ
-- Module: Mathlib.Probability.Moments.SubGaussian
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)) μ
ε : ℝ
hε : 0 ≤ ε
⊢ μ.real {ω : Ω | ε ≤ ∑ i ∈ Finset.range n, Y i ω} ≤
    rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑(∑ i ∈ Finset.range n, cY i) : ℝ)))

Tactic:
(HasSubgaussianMGF.sum_of_hasCondSubgaussianMGF h_adapted h0 n h_subG).measure_ge_le hε

Premises used: ProbabilityTheory.HasSubgaussianMGF.measure_ge_le, ProbabilityTheory.HasSubgaussianMGF.sum_of_hasCondSubgaussianMGF
-- Module: Mathlib.Probability.Moments.Tilted
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) ∂μ
rw₁ 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 ∂μ) ∂μ
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / mgf X μ t) ∂μ

Tactic:
rw [tilted_apply' _ _ hs, mgf]

Premises used: ProbabilityTheory.mgf, MeasureTheory.tilted_apply'
-- Module: Mathlib.Probability.Moments.Tilted
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) ∂μ
rw₁ 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 ∂μ) ∂μ
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / mgf X μ t) ∂μ

Tactic:
rw [tilted_apply, mgf]

Premises used: MeasureTheory.tilted_apply, ProbabilityTheory.mgf
-- Module: Mathlib.Probability.Moments.Tilted
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
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)) ∂μ
⊢ (μ.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μ

Premises used: eq_zero_or_neZero, rfl
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
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:
simp
-- Module: Mathlib.Probability.Moments.Tilted
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)) ∂μ
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)) ∂μ
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ∫⁻ (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]

Premises used: ProbabilityTheory.exp_cgf, ProbabilityTheory.tilted_mul_apply_mgf', Real.exp_sub
-- Module: Mathlib.Probability.Moments.Tilted
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
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)) ∂μ
⊢ (μ.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μ

Premises used: eq_zero_or_neZero, rfl
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
inst : 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:
simp
-- Module: Mathlib.Probability.Moments.Tilted
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)) ∂μ
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)) ∂μ
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ∫⁻ (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]

Premises used: ProbabilityTheory.exp_cgf, ProbabilityTheory.tilted_mul_apply_mgf, Real.exp_sub
-- Module: Mathlib.Probability.Moments.Tilted
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 ∂μ)
rw₁ 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 ∂μ ∂μ)
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ)

Tactic:
rw [tilted_apply_eq_ofReal_integral' _ hs, mgf]

Premises used: ProbabilityTheory.mgf, MeasureTheory.tilted_apply_eq_ofReal_integral'
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst : SFinite μ
s : Set Ω
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 ∂μ)
rw₁ 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 ∂μ ∂μ)
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ)

Tactic:
rw [tilted_apply_eq_ofReal_integral _ s, mgf]

Premises used: MeasureTheory.tilted_apply_eq_ofReal_integral, ProbabilityTheory.mgf
-- Module: Mathlib.Probability.Moments.Tilted
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 =
      ENNReal.ofReal (@integral _ _ _ _ mΩ (Measure.restrict 0 s) fun (a : Ω) ↦ rexp (t * X a - cgf (m := mΩ) X 0 t))
inr :
  ∀ (hμ : NeZero μ),
    (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
      ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a - cgf X μ t) ∂μ)
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a - cgf X μ t) ∂μ)

Tactic:
rcases eq_zero_or_neZero μ with rfl | hμ

Premises used: eq_zero_or_neZero, rfl
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
ht : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) 0
⊢ ((Measure.tilted 0 fun (x : Ω) ↦ t * X x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
    ENNReal.ofReal (@integral _ _ _ _ mΩ (Measure.restrict 0 s) fun (a : Ω) ↦ rexp (t * X a - cgf (m := mΩ) X 0 t))

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hμ : NeZero μ
inr :
  ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ) =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / rexp (cgf X μ t) ∂μ)
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a - cgf X μ t) ∂μ)

Tactic:
simp_rw [tilted_mul_apply_eq_ofReal_integral_mgf' hs, exp_sub]

Premises used: ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_mgf', Real.exp_sub
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hμ : NeZero μ
inr :
  ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ) =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ)
inr₁ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
inr₂ :
  ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ) =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ)
inr₃ inr₄ inr₅ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ) =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / rexp (cgf X μ t) ∂μ)

Tactic:
rwa [exp_cgf]

Premises used: ProbabilityTheory.exp_cgf
-- Module: Mathlib.Probability.Moments.Tilted
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 =
      ENNReal.ofReal (@integral _ _ _ _ mΩ (Measure.restrict 0 s) fun (a : Ω) ↦ rexp (t * X a - cgf (m := mΩ) X 0 t))
inr :
  ∀ (hμ : NeZero μ),
    (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
      ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a - cgf X μ t) ∂μ)
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a - cgf X μ t) ∂μ)

Tactic:
rcases eq_zero_or_neZero μ with rfl | hμ

Premises used: eq_zero_or_neZero, rfl
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
inst : 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 =
    ENNReal.ofReal (@integral _ _ _ _ mΩ (Measure.restrict 0 s) fun (a : Ω) ↦ rexp (t * X a - cgf (m := mΩ) X 0 t))

Tactic:
simp