awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
B : ℝ
hB : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1)))) B
⊢ False
have h : ∀ (n : ℕ), ¬(↑B.toNNReal : ℝ≥0∞) < ∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
Tactic: refine not_eventually.2 (Frequently.of_forall fun n => ?_) (htends B.toNNReal)
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
B : ℝ
hB : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1)))) B
n : ℕ
⊢ ¬(↑B.toNNReal : ℝ≥0∞) < ∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
have h : ∀
  (hB :
    ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) x → x ≤ B)
  (n : ℕ), ¬(↑B.toNNReal : ℝ≥0∞) < ∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
Tactic: rw [mem_upperBounds] at hB
Cleared hypotheses: hB, n
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
B : ℝ
hB : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) x → x ≤ B
n : ℕ
⊢ ¬(↑B.toNNReal : ℝ≥0∞) < ∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
have h : Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1)))
  (ENNReal.toReal (∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))))
Tactic: specialize hB (∑ k ∈ Finset.range n, μ (s (k + 1))).toReal _
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
B : ℝ
hB : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) x → x ≤ B
n : ℕ
h :
  Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1)))
    (ENNReal.toReal (∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))))
⊢ ¬(↑B.toNNReal : ℝ≥0∞) < ∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
have h₁ : ∀ (hB : ENNReal.toReal (∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))) ≤ B),
  ¬(↑B.toNNReal : ℝ≥0∞) < ∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
Tactic: specialize hB (∑ k ∈ Finset.range n, μ (s (k + 1))).toReal _
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
B : ℝ
hB : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) x → x ≤ B
n : ℕ
⊢ Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1)))
    (ENNReal.toReal (∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))))
have h : (fun (n : ℕ) ↦ (∑ x ∈ Finset.range n, μ.real (s (x + 1)) : ℝ)) n =
  ENNReal.toReal (∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1)))
Tactic: refine ⟨n, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
B : ℝ
hB : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) x → x ≤ B
n : ℕ
⊢ (fun (n : ℕ) ↦ (∑ x ∈ Finset.range n, μ.real (s (x + 1)) : ℝ)) n =
    ENNReal.toReal (∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1)))
have h : Eq (α := ℝ) ((fun (n : ℕ) ↦ (∑ x ∈ Finset.range n, μ.real (s (x + 1)) : ℝ)) n)
  (∑ a ∈ Finset.range n, ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) (s (a + 1))))
Tactic: rw [ENNReal.toReal_sum (by finiteness)]
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
B : ℝ
n : ℕ
hB : ENNReal.toReal (∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))) ≤ B
⊢ ¬(↑B.toNNReal : ℝ≥0∞) < ∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
have h : Ne (α := ℝ≥0∞) (∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))) ∞
Tactic: rwa [not_lt, ENNReal.ofNNReal_toNNReal, ENNReal.le_ofReal_iff_toReal_le]
-- Lean 4 proof step from Mathlib.Probability.BorelCantelli (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0∞) (s n)) ∞
this_1 : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (n : ℕ),
      Eq (α := ℝ) (μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω)
        ((fun (x : Ω) ↦ μ.real (s (n + 1))) ω)
ω : Ω
hω :
  ∀ (n : ℕ),
    μ[(s (n + 1)).indicator 1 | (↑(filtrationOfSet (s := s) hsm) : ℕ → MeasurableSpace Ω) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, (↑x : ℝ≥0∞) < ∑ k ∈ Finset.range a, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
B : ℝ
n : ℕ
hB : ENNReal.toReal (∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))) ≤ B
h : Ne (α := ℝ≥0∞) (∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))) ∞
⊢ ¬(↑B.toNNReal : ℝ≥0∞) < ∑ k ∈ Finset.range n, (μ : (a : Set Ω) → ℝ≥0∞) (s (k + 1))
have h₁ : 0 ≤ B
Tactic: rwa [not_lt, ENNReal.ofNNReal_toNNReal, ENNReal.le_ofReal_iff_toReal_le]
-- Lean 4 proof step from Mathlib.Probability.CDF (hypothesis)
Goal:
μ : Measure ℝ
inst : IsProbabilityMeasure μ
x : ℝ
⊢ ENNReal.ofReal ((↑(cdf μ) : ℝ → ℝ) x) = (μ : (a : Set ℝ) → ENNReal) (Iic x)
have h : ∫⁻ (a : Unit),
    ENNReal.ofReal
      ((↑(condCDF (mα := PUnit.instMeasurableSpace) (Measure.prod (dirac ()) μ) a) : ℝ → ℝ)
        x) ∂fst (Measure.prod (dirac ()) μ) =
  (Measure.prod (dirac ()) μ : (a : Set (Unit × ℝ)) → ENNReal) (SProd.sprod (α := Set Unit) univ (Iic x))
Tactic: have h := lintegral_condCDF ((dirac Unit.unit).prod μ) x
-- Lean 4 proof step from Mathlib.Probability.CDF (goal)
Goal:
μ : Measure ℝ
inst : IsProbabilityMeasure μ
x : ℝ
⊢ (↑(cdf μ) : ℝ → ℝ) x = μ.real (Iic x)
have rw : (↑(cdf μ) : ℝ → ℝ) x = ENNReal.toReal ((μ : (a : Set ℝ) → ENNReal) (Iic x))
Tactic: rw [measureReal_def, ← ofReal_cdf μ x, ENNReal.toReal_ofReal (cdf_nonneg μ x)]
-- Lean 4 proof step from Mathlib.Probability.CDF (goal)
Goal:
μ : Measure ℝ
inst : IsProbabilityMeasure μ
x : ℝ
rw : (↑(cdf μ) : ℝ → ℝ) x = ENNReal.toReal ((μ : (a : Set ℝ) → ENNReal) (Iic x))
⊢ (↑(cdf μ) : ℝ → ℝ) x = μ.real (Iic x)
have rw₁ : (↑(cdf μ) : ℝ → ℝ) x = (ENNReal.ofReal ((↑(cdf μ) : ℝ → ℝ) x)).toReal
Tactic: rw [measureReal_def, ← ofReal_cdf μ x, ENNReal.toReal_ofReal (cdf_nonneg μ x)]
-- Lean 4 proof step from Mathlib.Probability.CDF (goal)
Goal:
μ : Measure ℝ
inst : IsProbabilityMeasure μ
x : ℝ
rw : (↑(cdf μ) : ℝ → ℝ) x = ENNReal.toReal ((μ : (a : Set ℝ) → ENNReal) (Iic x))
rw₁ : (↑(cdf μ) : ℝ → ℝ) x = (ENNReal.ofReal ((↑(cdf μ) : ℝ → ℝ) x)).toReal
⊢ (↑(cdf μ) : ℝ → ℝ) x = μ.real (Iic x)
have rw₂ : (↑(cdf μ) : ℝ → ℝ) x = (↑(cdf μ) : ℝ → ℝ) x
Tactic: rw [measureReal_def, ← ofReal_cdf μ x, ENNReal.toReal_ofReal (cdf_nonneg μ x)]
-- Lean 4 proof step from Mathlib.Probability.CDF (goal)
Goal:
μ : Measure ℝ
⊢ IsProbabilityMeasure (m0 := Real.measurableSpace) (cdf μ).measure
have measure_univ : Eq (α := ENNReal) (((cdf μ).measure : (a : Set ℝ) → ENNReal) univ : ENNReal) (1 : ENNReal)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.CDF (goal)
Goal:
μ : Measure ℝ
inst : IsProbabilityMeasure μ
⊢ (cdf μ).measure = μ
have refine : ∀ (a : ℝ),
  Eq (α := ENNReal) (((cdf μ).measure : (a : Set ℝ) → ENNReal) (Iic a) : ENNReal)
    ((μ : (a : Set ℝ) → ENNReal) (Iic a) : ENNReal)
Tactic: refine ext_of_Iic (cdf μ).measure μ (fun a ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.CDF (goal)
Goal:
μ : Measure ℝ
inst : IsProbabilityMeasure μ
a : ℝ
⊢ Eq (α := ENNReal) (((cdf μ).measure : (a : Set ℝ) → ENNReal) (Iic a) : ENNReal)
    ((μ : (a : Set ℝ) → ENNReal) (Iic a) : ENNReal)
have rw : ENNReal.ofReal ((↑(cdf μ) : ℝ → ℝ) a - 0) = (μ : (a : Set ℝ) → ENNReal) (Iic a)
Tactic: rw [StieltjesFunction.measure_Iic _ (tendsto_cdf_atBot μ), sub_zero, ofReal_cdf]
-- Lean 4 proof step from Mathlib.Probability.CDF (goal)
Goal:
μ : Measure ℝ
inst : IsProbabilityMeasure μ
a : ℝ
rw : ENNReal.ofReal ((↑(cdf μ) : ℝ → ℝ) a - 0) = (μ : (a : Set ℝ) → ENNReal) (Iic a)
⊢ Eq (α := ENNReal) (((cdf μ).measure : (a : Set ℝ) → ENNReal) (Iic a) : ENNReal)
    ((μ : (a : Set ℝ) → ENNReal) (Iic a) : ENNReal)
have rw₁ : ENNReal.ofReal ((↑(cdf μ) : ℝ → ℝ) a) = (μ : (a : Set ℝ) → ENNReal) (Iic a)
Tactic: rw [StieltjesFunction.measure_Iic _ (tendsto_cdf_atBot μ), sub_zero, ofReal_cdf]
-- Lean 4 proof step from Mathlib.Probability.CDF (goal)
Goal:
μ : Measure ℝ
inst : IsProbabilityMeasure μ
a : ℝ
rw : ENNReal.ofReal ((↑(cdf μ) : ℝ → ℝ) a - 0) = (μ : (a : Set ℝ) → ENNReal) (Iic a)
rw₁ : ENNReal.ofReal ((↑(cdf μ) : ℝ → ℝ) a) = (μ : (a : Set ℝ) → ENNReal) (Iic a)
⊢ Eq (α := ENNReal) (((cdf μ).measure : (a : Set ℝ) → ENNReal) (Iic a) : ENNReal)
    ((μ : (a : Set ℝ) → ENNReal) (Iic a) : ENNReal)
have rw₂ : Eq (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Iic a) : ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Iic a) : ENNReal)
Tactic: rw [StieltjesFunction.measure_Iic _ (tendsto_cdf_atBot μ), sub_zero, ofReal_cdf]
-- Lean 4 proof step from Mathlib.Probability.CDF (goal)
Goal:
f : StieltjesFunction ℝ
hf0 : Tendsto (↑f : ℝ → ℝ) atBot (𝓝 0)
hf1 : Tendsto (↑f : ℝ → ℝ) atTop (𝓝 1)
⊢ cdf f.measure = f
have refine : Eq (α := Measure ℝ) (cdf f.measure).measure f.measure
Tactic: refine (cdf f.measure).eq_of_measure_of_tendsto_atBot f ?_ (tendsto_cdf_atBot _) hf0
-- Lean 4 proof step from Mathlib.Probability.CDF (goal)
Goal:
f : StieltjesFunction ℝ
hf0 : Tendsto (↑f : ℝ → ℝ) atBot (𝓝 0)
hf1 : Tendsto (↑f : ℝ → ℝ) atTop (𝓝 1)
⊢ Eq (α := ENNReal) ((f.measure : (a : Set ℝ) → ENNReal) univ : ENNReal) (1 : ENNReal)
have rw : ENNReal.ofReal (HSub.hSub (α := ℝ) 1 0) = 1
Tactic: rw [f.measure_univ hf0 hf1, sub_zero, ENNReal.ofReal_one]
-- Lean 4 proof step from Mathlib.Probability.CDF (goal)
Goal:
f : StieltjesFunction ℝ
hf0 : Tendsto (↑f : ℝ → ℝ) atBot (𝓝 0)
hf1 : Tendsto (↑f : ℝ → ℝ) atTop (𝓝 1)
rw : ENNReal.ofReal (HSub.hSub (α := ℝ) 1 0) = 1
⊢ Eq (α := ENNReal) ((f.measure : (a : Set ℝ) → ENNReal) univ : ENNReal) (1 : ENNReal)
have rw₁ : ENNReal.ofReal 1 = 1
Tactic: rw [f.measure_univ hf0 hf1, sub_zero, ENNReal.ofReal_one]
-- Lean 4 proof step from Mathlib.Probability.CDF (goal)
Goal:
f : StieltjesFunction ℝ
hf0 : Tendsto (↑f : ℝ → ℝ) atBot (𝓝 0)
hf1 : Tendsto (↑f : ℝ → ℝ) atTop (𝓝 1)
rw : ENNReal.ofReal (HSub.hSub (α := ℝ) 1 0) = 1
rw₁ : ENNReal.ofReal 1 = 1
⊢ Eq (α := ENNReal) ((f.measure : (a : Set ℝ) → ENNReal) univ : ENNReal) (1 : ENNReal)
have rw₂ : Eq (α := ENNReal) 1 1
Tactic: rw [f.measure_univ hf0 hf1, sub_zero, ENNReal.ofReal_one]
-- Lean 4 proof step from Mathlib.Probability.CDF (hypothesis)
Goal:
f : StieltjesFunction ℝ
hf0 : Tendsto (↑f : ℝ → ℝ) atBot (𝓝 0)
hf1 : Tendsto (↑f : ℝ → ℝ) atTop (𝓝 1)
⊢ Eq (α := Measure ℝ) (cdf f.measure).measure f.measure
have h_prob : IsProbabilityMeasure (m0 := Real.measurableSpace) f.measure
Tactic: have h_prob : IsProbabilityMeasure f.measure :=
    ⟨by rw [f.measure_univ hf0 hf1, sub_zero, ENNReal.ofReal_one]⟩
-- Lean 4 proof step from Mathlib.Probability.CDF (hypothesis)
Goal:
μ : Measure (↑I : Type)
inst : IsProbabilityMeasure μ
x : (↑I : Type)
⊢ (↑(cdf (Measure.map (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) μ)) : ℝ → ℝ) (↑x : ℝ) = μ.real (Icc 0 x)
have this : IsProbabilityMeasure (m0 := Real.measurableSpace) (Measure.map (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) μ)
Tactic: haveI : IsProbabilityMeasure (μ.map Subtype.val) := isProbabilityMeasure_map (by fun_prop)
-- Lean 4 proof step from Mathlib.Probability.CDF (goal)
Goal:
μ : Measure (↑I : Type)
inst : IsProbabilityMeasure μ
x : (↑I : Type)
this : IsProbabilityMeasure (m0 := Real.measurableSpace) (Measure.map (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) μ)
⊢ (↑(cdf (Measure.map (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) μ)) : ℝ → ℝ) (↑x : ℝ) = μ.real (Icc 0 x)
have rw : Measure.real (m := Real.measurableSpace) (Measure.map (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) μ) (Iic (↑x : ℝ)) =
  μ.real (Icc 0 x)
Tactic: rw [ProbabilityTheory.cdf_eq_real,
    map_measureReal_apply measurable_subtype_coe measurableSet_Iic, subtype_Iic_eq_Icc]
-- Lean 4 proof step from Mathlib.Probability.CDF (goal)
Goal:
μ : Measure (↑I : Type)
inst : IsProbabilityMeasure μ
x : (↑I : Type)
this : IsProbabilityMeasure (m0 := Real.measurableSpace) (Measure.map (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) μ)
rw :
  Measure.real (m := Real.measurableSpace) (Measure.map (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) μ) (Iic (↑x : ℝ)) =
    μ.real (Icc 0 x)
⊢ (↑(cdf (Measure.map (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) μ)) : ℝ → ℝ) (↑x : ℝ) = μ.real (Icc 0 x)
have rw₁ : μ.real (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I) ⁻¹' Iic (↑x : ℝ)) = μ.real (Icc 0 x)
Tactic: rw [ProbabilityTheory.cdf_eq_real,
    map_measureReal_apply measurable_subtype_coe measurableSet_Iic, subtype_Iic_eq_Icc]
-- Lean 4 proof step from Mathlib.Probability.CDF (goal)
Goal:
μ : Measure (↑I : Type)
inst : IsProbabilityMeasure μ
x : (↑I : Type)
this : IsProbabilityMeasure (m0 := Real.measurableSpace) (Measure.map (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) μ)
rw :
  Measure.real (m := Real.measurableSpace) (Measure.map (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) μ) (Iic (↑x : ℝ)) =
    μ.real (Icc 0 x)
rw₁ : μ.real (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I) ⁻¹' Iic (↑x : ℝ)) = μ.real (Icc 0 x)
⊢ (↑(cdf (Measure.map (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) μ)) : ℝ → ℝ) (↑x : ℝ) = μ.real (Icc 0 x)
have rw₂ : μ.real (Icc 0 x) = μ.real (Icc 0 x)
Tactic: rw [ProbabilityTheory.cdf_eq_real,
    map_measureReal_apply measurable_subtype_coe measurableSet_Iic, subtype_Iic_eq_Icc]
-- Lean 4 proof step from Mathlib.Probability.CDF (goal)
Goal:
μ ν : Measure ℝ
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
h : cdf μ = cdf ν
⊢ μ = ν
have rw : (cdf μ).measure = ν
Tactic: rw [← measure_cdf μ, ← measure_cdf ν, h]
-- Lean 4 proof step from Mathlib.Probability.CDF (goal)
Goal:
μ ν : Measure ℝ
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
h : cdf μ = cdf ν
rw : (cdf μ).measure = ν
⊢ μ = ν
have rw₁ : Eq (α := Measure ℝ) (cdf μ).measure (cdf ν).measure
Tactic: rw [← measure_cdf μ, ← measure_cdf ν, h]
-- Lean 4 proof step from Mathlib.Probability.CDF (goal)
Goal:
μ ν : Measure ℝ
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
h : cdf μ = cdf ν
rw : (cdf μ).measure = ν
rw₁ : Eq (α := Measure ℝ) (cdf μ).measure (cdf ν).measure
⊢ μ = ν
have rw₂ : Eq (α := Measure ℝ) (cdf ν).measure (cdf ν).measure
Tactic: rw [← measure_cdf μ, ← measure_cdf ν, h]
-- Lean 4 proof step from Mathlib.Probability.CDF (goal)
Goal:
μ ν : Measure ℝ
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
h : μ = ν
⊢ cdf μ = cdf ν
have rw : cdf ν = cdf ν
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : ℕ → Ω → ℝ
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
n : ℕ
t : ℝ
⊢ charFun (mE := Real.measurableSpace) (Measure.map (fun (ω : Ω) ↦ (√(↑n : ℝ))⁻¹ * ∑ k ∈ Finset.range n, X k ω) P) t =
    charFun (mE := Real.measurableSpace) (Measure.map (X 0) P) ((√(↑n : ℝ))⁻¹ * t) ^ n
have mX : ∀ (n : ℕ), AEMeasurable (X n) P
Tactic: have mX n := (hident n).aemeasurable_fst
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : ℕ → Ω → ℝ
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
n : ℕ
t : ℝ
mX : ∀ (n : ℕ), AEMeasurable (X n) P
⊢ charFun (mE := Real.measurableSpace) (Measure.map (fun (ω : Ω) ↦ (√(↑n : ℝ))⁻¹ * ∑ k ∈ Finset.range n, X k ω) P) t =
    charFun (mE := Real.measurableSpace) (Measure.map (X 0) P) ((√(↑n : ℝ))⁻¹ * t) ^ n
have rw : (∏ i ∈ Finset.range n, charFun (mE := Real.measurableSpace) (Measure.map (X i) P)) ((√(↑n : ℝ))⁻¹ * t) =
  charFun (mE := Real.measurableSpace) (Measure.map (X 0) P) ((√(↑n : ℝ))⁻¹ * t) ^ n
Tactic: rw [charFun_map_mul_comp, (hindep.restrict _).charFun_map_fun_finsetSum_eq_prod (fun _ _ ↦ mX _)]
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : ℕ → Ω → ℝ
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
n : ℕ
t : ℝ
mX : ∀ (n : ℕ), AEMeasurable (X n) P
rw :
  (∏ i ∈ Finset.range n, charFun (mE := Real.measurableSpace) (Measure.map (X i) P)) ((√(↑n : ℝ))⁻¹ * t) =
    charFun (mE := Real.measurableSpace) (Measure.map (X 0) P) ((√(↑n : ℝ))⁻¹ * t) ^ n
⊢ charFun (mE := Real.measurableSpace) (Measure.map (fun (ω : Ω) ↦ (√(↑n : ℝ))⁻¹ * ∑ k ∈ Finset.range n, X k ω) P) t =
    charFun (mE := Real.measurableSpace) (Measure.map (X 0) P) ((√(↑n : ℝ))⁻¹ * t) ^ n
have hf : AEMeasurable (β := ℝ) (fun (ω : Ω) ↦ ∑ k ∈ Finset.range n, X k ω) P
Tactic: rw [charFun_map_mul_comp, (hindep.restrict _).charFun_map_fun_finsetSum_eq_prod (fun _ _ ↦ mX _)]
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : Eq (α := ℝ) (∫ (x : Ω), X x ∂P) 0
h1 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) 1
t : ℝ
⊢ Tendsto (fun (n : ℕ) ↦ charFun (mE := Real.measurableSpace) (Measure.map X P) ((√(↑n : ℝ))⁻¹ * t) ^ n) atTop
    (𝓝 (cexp (-HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)))
have hf : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) atTop
  (fun (n : ℕ) ↦
    charFun (mE := Real.measurableSpace) (Measure.map X P) ((√(↑n : ℝ))⁻¹ * t) -
      (1 + -HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 / (↑n : ℂ)))
  fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)
Tactic: apply tendsto_pow_exp_of_isLittleO_sub_add_div
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : Eq (α := ℝ) (∫ (x : Ω), X x ∂P) 0
h1 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) 1
t : ℝ
this :
  Asymptotics.IsLittleO (E := ℂ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      charFun (mE := Real.measurableSpace) (Measure.map X P) ((√(↑n : ℝ))⁻¹ * t) -
        (1 + -(HPow.hPow (β := ℕ) ((↑(√(↑n : ℝ))⁻¹ : ℂ) * (↑t : ℂ)) 2 / 2)))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) ((√(↑n : ℝ))⁻¹ * t) 2
⊢ Asymptotics.IsLittleO (E := ℂ) (F := ℂ) atTop
    (fun (n : ℕ) ↦
      charFun (mE := Real.measurableSpace) (Measure.map X P) ((√(↑n : ℝ))⁻¹ * t) -
        (1 + -HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 / (↑n : ℂ)))
    fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)
have aux : Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ ‖HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)‖) fun (n : ℕ) ↦ ‖HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)‖
Tactic: have aux : (fun (n : ℕ) ↦ ‖(1 / n : ℂ)‖) = fun (n : ℕ) ↦ ‖(1 / n : ℝ)‖ := by simp