awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
t : ℝ
⊢ charFun (gaussianReal m₁ v₁ ∗ gaussianReal m₂ v₂) t = charFun (gaussianReal (m₁ + m₂) (v₁ + v₂)) t
have h : cexp ((↑t : ℂ) * (↑m₁ : ℂ) * Complex.I - (↑(↑v₁ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2) *
    cexp ((↑t : ℂ) * (↑m₂ : ℂ) * Complex.I - (↑(↑v₂ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2) =
  cexp ((↑t : ℂ) * (↑(m₁ + m₂) : ℂ) * Complex.I - (↑(↑(v₁ + v₂) : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)
Tactic: simp_rw [charFun_conv, charFun_gaussianReal]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
t : ℝ
⊢ cexp ((↑t : ℂ) * (↑m₁ : ℂ) * Complex.I - (↑(↑v₁ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2) *
      cexp ((↑t : ℂ) * (↑m₂ : ℂ) * Complex.I - (↑(↑v₂ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2) =
    cexp ((↑t : ℂ) * (↑(m₁ + m₂) : ℂ) * Complex.I - (↑(↑(v₁ + v₂) : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)
have h : cexp
    ((↑t : ℂ) * (↑m₁ : ℂ) * Complex.I - (↑(↑v₁ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 +
      ((↑t : ℂ) * (↑m₂ : ℂ) * Complex.I - (↑(↑v₂ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)) =
  cexp ((↑t : ℂ) * (↑(m₁ + m₂) : ℂ) * Complex.I - (↑(↑(v₁ + v₂) : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)
Tactic: rw [← Complex.exp_add]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
t : ℝ
⊢ cexp
      ((↑t : ℂ) * (↑m₁ : ℂ) * Complex.I - (↑(↑v₁ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 +
        ((↑t : ℂ) * (↑m₂ : ℂ) * Complex.I - (↑(↑v₂ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)) =
    cexp ((↑t : ℂ) * (↑(m₁ + m₂) : ℂ) * Complex.I - (↑(↑(v₁ + v₂) : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)
have h : cexp
    ((↑t : ℂ) * (↑m₁ : ℂ) * Complex.I - (↑(↑v₁ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 +
      ((↑t : ℂ) * (↑m₂ : ℂ) * Complex.I - (↑(↑v₂ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)) =
  cexp
    ((↑t : ℂ) * ((↑m₁ : ℂ) + (↑m₂ : ℂ)) * Complex.I -
      ((↑(↑v₁ : ℝ) : ℂ) + (↑(↑v₂ : ℝ) : ℂ)) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)
Tactic: simp only [Complex.ofReal_add, NNReal.coe_add]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ Measure.map (X + Y) P = gaussianReal (m₁ + m₂) (v₁ + v₂)
have hf : AEMeasurable X P
Tactic: rw [hXY.map_add_eq_map_conv_map₀', hX, hY, gaussianReal_conv_gaussianReal]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
hf : AEMeasurable X P
⊢ Measure.map (X + Y) P = gaussianReal (m₁ + m₂) (v₁ + v₂)
have hg : AEMeasurable Y P
Tactic: rw [hXY.map_add_eq_map_conv_map₀', hX, hY, gaussianReal_conv_gaussianReal]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
hf : AEMeasurable X P
hg : AEMeasurable Y P
⊢ Measure.map (X + Y) P = gaussianReal (m₁ + m₂) (v₁ + v₂)
have σf : SigmaFinite (m0 := Real.measurableSpace) (Measure.map X P)
Tactic: rw [hXY.map_add_eq_map_conv_map₀', hX, hY, gaussianReal_conv_gaussianReal]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
hf : AEMeasurable X P
hg : AEMeasurable Y P
σf : SigmaFinite (m0 := Real.measurableSpace) (Measure.map X P)
⊢ Measure.map (X + Y) P = gaussianReal (m₁ + m₂) (v₁ + v₂)
have σg : SigmaFinite (m0 := Real.measurableSpace) (Measure.map Y P)
Tactic: rw [hXY.map_add_eq_map_conv_map₀', hX, hY, gaussianReal_conv_gaussianReal]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ AEMeasurable X P
have hf : Ne (α := Measure ℝ) (Measure.map X P) 0
Tactic: apply AEMeasurable.of_map_ne_zero
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ AEMeasurable Y P
have hg : Ne (α := Measure ℝ) (Measure.map Y P) 0
Tactic: apply AEMeasurable.of_map_ne_zero
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ SigmaFinite (m0 := Real.measurableSpace) (Measure.map X P)
have σf : SigmaFinite (gaussianReal m₁ v₁)
Tactic: rw [hX]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ SigmaFinite (m0 := Real.measurableSpace) (Measure.map Y P)
have σg : SigmaFinite (gaussianReal m₂ v₂)
Tactic: rw [hY]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (goal)
Goal:
p : (↑unitInterval : Type)
hp : p ≠ 0
n : ℕ
⊢ (geometricMeasure p : (a : Set ℕ) → ℝ≥0∞) {n} = ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))
have rw : (Measure.sum fun (n : ℕ) ↦
        HSMul.hSMul (β := Measure ℕ) (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))) (Measure.dirac n) :
      (a : Set ℕ) → ℝ≥0∞)
    {n} =
  ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))
Tactic: rw [geometricMeasure_eq hp, Measure.sum_smul_dirac_singleton]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (goal)
Goal:
p : (↑unitInterval : Type)
hp : p ≠ 0
n : ℕ
rw :
  (Measure.sum fun (n : ℕ) ↦
          HSMul.hSMul (β := Measure ℕ) (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))) (Measure.dirac n) :
        (a : Set ℕ) → ℝ≥0∞)
      {n} =
    ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))
⊢ (geometricMeasure p : (a : Set ℕ) → ℝ≥0∞) {n} = ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))
have rw₁ : ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) = ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))
Tactic: rw [geometricMeasure_eq hp, Measure.sum_smul_dirac_singleton]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (goal)
Goal:
p : (↑unitInterval : Type)
hp : p ≠ 0
n : ℕ
⊢ (geometricMeasure p).real {n} = (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)
have rw : ENNReal.toReal ((geometricMeasure p : (a : Set ℕ) → ℝ≥0∞) {n}) = (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)
Tactic: rw [measureReal_def, geometricMeasure_singleton hp,
    ENNReal.toReal_ofReal (geometricMeasure_nonneg p n)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (goal)
Goal:
p : (↑unitInterval : Type)
hp : p ≠ 0
n : ℕ
rw : ENNReal.toReal ((geometricMeasure p : (a : Set ℕ) → ℝ≥0∞) {n}) = (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)
⊢ (geometricMeasure p).real {n} = (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)
have rw₁ : (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal = (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)
Tactic: rw [measureReal_def, geometricMeasure_singleton hp,
    ENNReal.toReal_ofReal (geometricMeasure_nonneg p n)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (goal)
Goal:
p : (↑unitInterval : Type)
hp : p ≠ 0
n : ℕ
rw : ENNReal.toReal ((geometricMeasure p : (a : Set ℕ) → ℝ≥0∞) {n}) = (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)
rw₁ : (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal = (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)
⊢ (geometricMeasure p).real {n} = (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)
have rw₂ : (1 - (↑p : ℝ)) ^ n * (↑p : ℝ) = (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)
Tactic: rw [measureReal_def, geometricMeasure_singleton hp,
    ENNReal.toReal_ofReal (geometricMeasure_nonneg p n)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (goal)
Goal:
p : (↑unitInterval : Type)
h1 : p ≠ 0
h2 : p ≠ 1
n : ℕ
⊢ 0 < (geometricMeasure p).real {n}
have rw : 0 < (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)
Tactic: rw [geometricMeasure_real_singleton h1]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (goal)
Goal:
p : (↑unitInterval : Type)
hp : p ≠ 0
⊢ HasSum (α := ℝ) (fun (n : ℕ) ↦ (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) 1
have h : 1 = (1 - (1 - (↑p : ℝ)))⁻¹ * (↑p : ℝ)
Tactic: convert! (hasSum_geometric_of_lt_one (r := 1 - p) (by grind) (by grind)).mul_right (p : ℝ)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (goal)
Goal:
p : (↑unitInterval : Type)
⊢ IsProbabilityMeasure (α := ℕ) (m0 := Nat.instMeasurableSpace)
    (if p ≠ 0 then
      Measure.sum fun (n : ℕ) ↦
        HSMul.hSMul (β := Measure ℕ) (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))) (Measure.dirac n)
    else Measure.dirac 0)
have pos : ∀ (h : p ≠ 0),
  IsProbabilityMeasure (α := ℕ) (m0 := Nat.instMeasurableSpace)
    (Measure.sum fun (n : ℕ) ↦
      HSMul.hSMul (β := Measure ℕ) (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))) (Measure.dirac n))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (goal)
Goal:
p : (↑unitInterval : Type)
pos :
  ∀ (h : p ≠ 0),
    IsProbabilityMeasure (α := ℕ) (m0 := Nat.instMeasurableSpace)
      (Measure.sum fun (n : ℕ) ↦
        HSMul.hSMul (β := Measure ℕ) (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))) (Measure.dirac n))
⊢ IsProbabilityMeasure (α := ℕ) (m0 := Nat.instMeasurableSpace)
    (if p ≠ 0 then
      Measure.sum fun (n : ℕ) ↦
        HSMul.hSMul (β := Measure ℕ) (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))) (Measure.dirac n)
    else Measure.dirac 0)
have neg : ∀ (h : ¬p ≠ 0), IsProbabilityMeasure (α := ℕ) (m0 := Nat.instMeasurableSpace) (Measure.dirac 0)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (goal)
Goal:
p : (↑unitInterval : Type)
E : Type u_1
inst : NormedAddCommGroup E
f : ℕ → E
hp : p ≠ 0
⊢ Integrable f (geometricMeasure p) ↔ Summable (α := ℝ) fun (n : ℕ) ↦ (1 - (↑p : ℝ)) ^ n * (↑p : ℝ) * ‖f n‖
have rw : (Summable (α := ℝ) fun (i : ℕ) ↦ (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ i * (↑p : ℝ))).toReal * ‖f i‖) ↔
  Summable (α := ℝ) fun (n : ℕ) ↦ (1 - (↑p : ℝ)) ^ n * (↑p : ℝ) * ‖f n‖
Tactic: rw [geometricMeasure_eq hp, integrable_sum_dirac_iff (by simp)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (goal)
Goal:
p : (↑unitInterval : Type)
E : Type u_1
inst : NormedAddCommGroup E
f : ℕ → E
hp : p ≠ 0
⊢ (Summable (α := ℝ) fun (i : ℕ) ↦ (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ i * (↑p : ℝ))).toReal * ‖f i‖) ↔
    Summable (α := ℝ) fun (n : ℕ) ↦ (1 - (↑p : ℝ)) ^ n * (↑p : ℝ) * ‖f n‖
have a : ∀ (n : ℕ), (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal = (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)
Tactic: congrm Summable (fun n ↦ ?_ * _)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (goal)
Goal:
p : (↑unitInterval : Type)
E : Type u_1
inst : NormedAddCommGroup E
f : ℕ → E
hp : p ≠ 0
n : ℕ
⊢ (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal = (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)
have a : (1 - (↑p : ℝ)) ^ n * (↑p : ℝ) = (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)
Tactic: rw [ENNReal.toReal_ofReal (geometricMeasure_nonneg p n)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (goal)
Goal:
p : (↑unitInterval : Type)
E : Type u_1
inst : NormedAddCommGroup E
f : ℕ → E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hp : p ≠ 0
hf : Integrable f (geometricMeasure p)
⊢ Eq.{u_1 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n) fun (n : ℕ) ↦
    (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal • f n
have h : ∀ (n : ℕ), ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n = (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal • f n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (goal)
Goal:
p : (↑unitInterval : Type)
E : Type u_1
inst : NormedAddCommGroup E
f : ℕ → E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hp : p ≠ 0
hf : Integrable f (geometricMeasure p)
n : ℕ
⊢ ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n = (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal • f n
have h : ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n = ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n
Tactic: rw [ENNReal.toReal_ofReal (geometricMeasure_nonneg p n)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (hypothesis)
Goal:
p : (↑unitInterval : Type)
E : Type u_1
inst : NormedAddCommGroup E
f : ℕ → E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hp : p ≠ 0
hf : Integrable f (geometricMeasure p)
⊢ HasSum.{u_1, 0} (α := E) (fun (n : ℕ) ↦ ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n) (∫ (n : ℕ), f n ∂geometricMeasure p)
have this : Eq.{u_1 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n) fun (n : ℕ) ↦
  (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal • f n
Tactic: have : (fun n ↦ ((1 - p : ℝ) ^ n * p) • f n) =
      fun n ↦ (ENNReal.ofReal ((1 - p) ^ n * p)).toReal • f n := by
    ext n; rw [ENNReal.toReal_ofReal (geometricMeasure_nonneg p n)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (goal)
Goal:
p : (↑unitInterval : Type)
E : Type u_1
inst : NormedAddCommGroup E
f : ℕ → E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hp : p ≠ 0
hf : Integrable f (geometricMeasure p)
this :
  Eq.{u_1 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n) fun (n : ℕ) ↦
    (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal • f n
⊢ HasSum.{u_1, 0} (α := E) (fun (n : ℕ) ↦ ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n) (∫ (n : ℕ), f n ∂geometricMeasure p)
have rw : HasSum.{u_1, 0} (α := E) (fun (n : ℕ) ↦ (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal • f n)
  (@integral _ _ _ _ Nat.instMeasurableSpace
    (Measure.sum fun (n : ℕ) ↦
      HSMul.hSMul (β := Measure ℕ) (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))) (Measure.dirac n))
    fun (n : ℕ) ↦ f n)
Tactic: rw [this, geometricMeasure_eq hp]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (goal)
Goal:
p : (↑unitInterval : Type)
E : Type u_1
inst : NormedAddCommGroup E
f : ℕ → E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hp : p ≠ 0
hf : Integrable f (geometricMeasure p)
this :
  Eq.{u_1 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n) fun (n : ℕ) ↦
    (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal • f n
⊢ HasSum.{u_1, 0} (α := E) (fun (n : ℕ) ↦ (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal • f n)
    (@integral _ _ _ _ Nat.instMeasurableSpace
      (Measure.sum fun (n : ℕ) ↦
        HSMul.hSMul (β := Measure ℕ) (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))) (Measure.dirac n))
      fun (n : ℕ) ↦ f n)
have apply : Summable (α := ℝ) fun (i : ℕ) ↦ (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ i * (↑p : ℝ))).toReal * ‖f i‖
Tactic: apply hasSum_integral_sum_dirac (by simp)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (goal)
Goal:
p : (↑unitInterval : Type)
E : Type u_1
inst : NormedAddCommGroup E
f : ℕ → E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hp : p ≠ 0
hf : Integrable f (geometricMeasure p)
this :
  Eq.{u_1 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n) fun (n : ℕ) ↦
    (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal • f n
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ i * (↑p : ℝ))).toReal * ‖f i‖
have h : ∀ (n : ℕ), (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal = (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)
Tactic: convert! (integrable_geometricMeasure_iff hp).1 hf with n
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (goal)
Goal:
p : (↑unitInterval : Type)
E : Type u_1
inst : NormedAddCommGroup E
f : ℕ → E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hp : p ≠ 0
hf : Integrable f (geometricMeasure p)
this :
  Eq.{u_1 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n) fun (n : ℕ) ↦
    (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal • f n
n : ℕ
⊢ (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal = (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)
have h : (1 - (↑p : ℝ)) ^ n * (↑p : ℝ) = (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)
Tactic: rw [ENNReal.toReal_ofReal (geometricMeasure_nonneg p n)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (goal)
Goal:
p : (↑unitInterval : Type)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
hp : p ≠ 0
f : ℕ → E
⊢ Eq.{u_1 + 1} (α := E) (∑' (i : ℕ), (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ i * (↑p : ℝ))).toReal • f i)
    (∑' (n : ℕ), ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n)
have e_f : ∀ (n : ℕ), (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal • f n = ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n
Tactic: congr with n
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (goal)
Goal:
p : (↑unitInterval : Type)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
hp : p ≠ 0
f : ℕ → E
n : ℕ
⊢ (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal • f n = ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n
have e_f : ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n = ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n
Tactic: rw [ENNReal.toReal_ofReal (geometricMeasure_nonneg p n)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (hypothesis)
Goal:
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
⊢ HasSum (α := ℝ) (fun (n : ℕ) ↦ (1 - p) ^ n * p) 1
have this : HasSum (fun (n : ℕ) ↦ (1 - p) ^ n) (1 - (1 - p))⁻¹
Tactic: have := hasSum_geometric_of_lt_one (sub_nonneg.mpr hp_le_one) (sub_lt_self 1 hp_pos)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (hypothesis)
Goal:
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
this : HasSum (fun (n : ℕ) ↦ (1 - p) ^ n) (1 - (1 - p))⁻¹
⊢ HasSum (α := ℝ) (fun (n : ℕ) ↦ (1 - p) ^ n * p) 1
have this₁ : HasSum (fun (i : ℕ) ↦ (1 - p) ^ i * p) ((1 - (1 - p))⁻¹ * p)
Tactic: apply (hasSum_mul_right_iff (hp_pos.ne')).mpr at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (hypothesis)
Goal:
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
this : HasSum (fun (i : ℕ) ↦ (1 - p) ^ i * p) ((1 - (1 - p))⁻¹ * p)
⊢ HasSum (α := ℝ) (fun (n : ℕ) ↦ (1 - p) ^ n * p) 1
have this₁ : HasSum (fun (i : ℕ) ↦ (1 - p) ^ i * p) (p⁻¹ * p)
Tactic: simp only [sub_sub_cancel] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (goal)
Goal:
p : ℝ
n : ℕ
hp_pos : 0 < p
hp_lt_one : p < 1
⊢ 0 < (1 - p) ^ n * p
have positivity : 0 < 1 - p → 0 < (1 - p) ^ n * p
Tactic: positivity [sub_pos.mpr hp_lt_one]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (goal)
Goal:
p : ℝ
n : ℕ
hp_pos : 0 < p
hp_le_one : p ≤ 1
⊢ 0 ≤ (1 - p) ^ n * p
have positivity : 0 ≤ 1 - p → 0 ≤ (1 - p) ^ n * p
Tactic: positivity [sub_nonneg.mpr hp_le_one]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (goal)
Goal:
p_1 : (↑unitInterval : Type)
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
⊢ HasSum (α := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal (geometricPMFReal p n)) 1
have apply : HasSum (α := ℝ≥0) (fun (a : ℕ) ↦ (geometricPMFReal p a).toNNReal) 1
Tactic: apply ENNReal.hasSum_coe.mpr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (goal)
Goal:
p_1 : (↑unitInterval : Type)
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
⊢ HasSum (α := ℝ≥0) (fun (a : ℕ) ↦ (geometricPMFReal p a).toNNReal) 1
have rw : HasSum (fun (a : ℕ) ↦ (geometricPMFReal p a).toNNReal) (toNNReal 1)
Tactic: rw [← toNNReal_one]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Geometric (goal)
Goal:
p : ℝ
⊢ Measurable (geometricPMFReal p)
have funProp : Nat.instMeasurableSpace ≤ Nat.instMeasurableSpace
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
Goal:
t r x : ℝ
hx : x ≤ t
⊢ ∫⁻ (y : ℝ) in Iio x, paretoPDF t r y = 0
have rw : ∫⁻ (x : ℝ) in Iio x, 0 = 0
Tactic: rw [setLIntegral_congr_fun (g := fun _ ↦ 0) measurableSet_Iio]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
Goal:
t r x : ℝ
hx : x ≤ t
rw : ∫⁻ (x : ℝ) in Iio x, 0 = 0
⊢ ∫⁻ (y : ℝ) in Iio x, paretoPDF t r y = 0
have rw₁ : EqOn (paretoPDF t r) (fun (x : ℝ) ↦ 0) (Iio x)
Tactic: rw [setLIntegral_congr_fun (g := fun _ ↦ 0) measurableSet_Iio]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
Goal:
t r x : ℝ
hx : x ≤ t
⊢ ∫⁻ (x : ℝ) in Iio x, 0 = 0
have rw : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [lintegral_zero, ← ENNReal.ofReal_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
Goal:
t r x : ℝ
hx : x ≤ t
rw : Eq (α := ℝ≥0∞) 0 0
⊢ ∫⁻ (x : ℝ) in Iio x, 0 = 0
have rw₁ : ENNReal.ofReal 0 = ENNReal.ofReal 0
Tactic: rw [lintegral_zero, ← ENNReal.ofReal_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
Goal:
t r x : ℝ
hx : x ≤ t
a : ℝ
⊢ a ∈ Iio x → paretoPDF t r a = (fun (x : ℝ) ↦ (0 : ℝ≥0∞)) a
have a₁ : a < x → paretoPDF t r a = (fun (x : ℝ) ↦ (0 : ℝ≥0∞)) a
Tactic: (_ : a < _)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
Goal:
t r x : ℝ
hx : x ≤ t
a : ℝ
h : a < x
⊢ paretoPDF t r a = (fun (x : ℝ) ↦ (0 : ℝ≥0∞)) a
have simp : (if t ≤ a then r * t ^ r * a ^ (-(r + 1)) else 0) ≤ 0
Tactic: simp only [paretoPDF_eq, ENNReal.ofReal_eq_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
Goal:
t r x : ℝ
hx : x ≤ t
a : ℝ
h : a < x
⊢ ¬t ≤ a
have linarith : t ≤ a → x - t + (a - x) + (t - a) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
Goal:
t r x : ℝ
hx : x ≤ t
a : ℝ
h : a < x
⊢ (if t ≤ a then r * t ^ r * a ^ (-(r + 1)) else 0) ≤ 0
have rw : LE.le (α := ℝ) 0 0
Tactic: rw [if_neg (by linarith)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
Goal:
t r x : ℝ
ht : 0 < t
hr : 0 < r
hx : t ≤ x
⊢ 0 < paretoPDFReal t r x
have rw : 0 < r * t ^ r * x ^ (-(r + 1))
Tactic: rw [paretoPDFReal, if_pos hx]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
Goal:
t r x : ℝ
ht : 0 < t
hr : 0 < r
hx : t ≤ x
⊢ 0 < x
have linarith : x ≤ 0 → 0 - t + (t - x) + (x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (hypothesis)
Goal:
t r x : ℝ
ht : 0 < t
hr : 0 < r
hx : t ≤ x
⊢ 0 < r * t ^ r * x ^ (-(r + 1))
have x₁ : 0 < x
Tactic: have _ : 0 < x := by linarith
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
Goal:
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
⊢ 0 ≤ if t ≤ x then r * t ^ r * x ^ (-(r + 1)) else 0
have pos : ∀ (h : t ≤ x), 0 ≤ r * t ^ r * x ^ (-(r + 1))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
Goal:
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
pos : ∀ (h : t ≤ x), 0 ≤ r * t ^ r * x ^ (-(r + 1))
⊢ 0 ≤ if t ≤ x then r * t ^ r * x ^ (-(r + 1)) else 0
have neg : ∀ (h : ¬t ≤ x), LE.le (α := ℝ) 0 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (hypothesis)
Goal:
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : t ≤ x
ht0 : 0 = t
⊢ 0 ≤ r * t ^ r * x ^ (-(r + 1))
have h₁ : 0 ≤ x
Tactic: rw [← ht0] at h
Cleared hypotheses: h, ht0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
Goal:
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : t ≤ x
htp : 0 < t
⊢ 0 ≤ r * t ^ r * x ^ (-(r + 1))
have pos : 0 < x → 0 ≤ r * t ^ r * x ^ (-(r + 1))
Tactic: positivity [lt_of_lt_of_le htp h]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (hypothesis)
Goal:
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : t ≤ x
⊢ 0 ≤ r * t ^ r * x ^ (-(r + 1))
have x₁ : 0 = t ∨ 0 < t
Tactic: cases le_iff_eq_or_lt.1 ht with
    | inl ht0 =>
      rw [← ht0] at h
      positivity
    | inr htp =>
      positivity [lt_of_lt_of_le htp h]