awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : (↑unitInterval : Type)
h : p ≠ 0
⊢ IsProbabilityMeasure (α := ℕ) (m0 := Nat.instMeasurableSpace)
    (Measure.sum fun (n : ℕ) ↦
      HSMul.hSMul (β := Measure ℕ) (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))) (Measure.dirac n))

Tactic:
exact (hasSum_one_geometricMeasure h).isProbabilityMeasure_sum_dirac
      (geometricMeasure_nonneg p)

Premises used: ProbabilityTheory.geometricMeasure_nonneg, HasSum.isProbabilityMeasure_sum_dirac, ProbabilityTheory.hasSum_one_geometricMeasure
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : (↑unitInterval : Type)
h : ¬p ≠ 0
⊢ IsProbabilityMeasure (α := ℕ) (m0 := Nat.instMeasurableSpace) (Measure.dirac 0)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : (↑unitInterval : Type)
E : Type u_1
inst : NormedAddCommGroup E
f : ℕ → E
hp : p ≠ 0
⊢ ∀ (i : ℕ), ENNReal.ofReal ((1 - (↑p : ℝ)) ^ i * (↑p : ℝ)) ≠ ∞

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : (↑unitInterval : Type)
E : Type u_1
inst : NormedAddCommGroup E
f : ℕ → E
hp : p ≠ 0
rw :
  (Summable (α := ℝ) fun (i : ℕ) ↦ (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ i * (↑p : ℝ))).toReal * ‖f i‖) ↔
    Summable (α := ℝ) fun (n : ℕ) ↦ (1 - (↑p : ℝ)) ^ n * (↑p : ℝ) * ‖f n‖
⊢ Integrable f (geometricMeasure p) ↔ Summable (α := ℝ) fun (n : ℕ) ↦ (1 - (↑p : ℝ)) ^ n * (↑p : ℝ) * ‖f n‖

Tactic:
rw [geometricMeasure_eq hp, integrable_sum_dirac_iff (by simp)]

Premises used: ProbabilityTheory.geometricMeasure_eq, MeasureTheory.integrable_sum_dirac_iff
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : (↑unitInterval : Type)
E : Type u_1
inst : NormedAddCommGroup E
f : ℕ → E
hp : p ≠ 0
a : ∀ (n : ℕ), (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal = (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)
⊢ (Summable (α := ℝ) fun (i : ℕ) ↦ (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ i * (↑p : ℝ))).toReal * ‖f i‖) ↔
    Summable (α := ℝ) fun (n : ℕ) ↦ (1 - (↑p : ℝ)) ^ n * (↑p : ℝ) * ‖f n‖

Tactic:
congrm Summable (fun n ↦ ?_ * _)

Premises used: HMul.hMul, Summable, SummationFilter.unconditional
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : (↑unitInterval : Type)
E : Type u_1
inst : NormedAddCommGroup E
f : ℕ → E
hp : p ≠ 0
n : ℕ
a a₁ : (1 - (↑p : ℝ)) ^ n * (↑p : ℝ) = (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)
⊢ (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal = (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)

Tactic:
rw [ENNReal.toReal_ofReal (geometricMeasure_nonneg p n)]

Premises used: ProbabilityTheory.geometricMeasure_nonneg, ENNReal.toReal_ofReal
-- Module: Mathlib.Probability.Distributions.Geometric
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)
h : ∀ (n : ℕ), ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n = (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal • f n
⊢ 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:
ext n
-- Module: Mathlib.Probability.Distributions.Geometric
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 : ℕ
h h₁ : ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n = ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n
⊢ ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n = (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal • f n

Tactic:
rw [ENNReal.toReal_ofReal (geometricMeasure_nonneg p n)]

Premises used: ProbabilityTheory.geometricMeasure_nonneg, ENNReal.toReal_ofReal
-- Module: Mathlib.Probability.Distributions.Geometric
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

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)]
-- Module: Mathlib.Probability.Distributions.Geometric
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
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)
⊢ HasSum.{u_1, 0} (α := E) (fun (n : ℕ) ↦ ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n) (∫ (n : ℕ), f n ∂geometricMeasure p)

Tactic:
rw [this, geometricMeasure_eq hp]

Premises used: ProbabilityTheory.geometricMeasure_eq
-- Module: Mathlib.Probability.Distributions.Geometric
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
⊢ ∀ (i : ℕ), ENNReal.ofReal ((1 - (↑p : ℝ)) ^ i * (↑p : ℝ)) ≠ ∞

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Geometric
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
apply : Summable (α := ℝ) fun (i : ℕ) ↦ (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ i * (↑p : ℝ))).toReal * ‖f i‖
⊢ 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:
apply hasSum_integral_sum_dirac (by simp)

Premises used: MeasureTheory.hasSum_integral_sum_dirac
-- Module: Mathlib.Probability.Distributions.Geometric
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 (n : ℕ) ↦ (1 - (↑p : ℝ)) ^ n * (↑p : ℝ) * ‖f n‖

Tactic:
(integrable_geometricMeasure_iff hp).1 hf

Premises used: ProbabilityTheory.integrable_geometricMeasure_iff, Iff.mp
-- Module: Mathlib.Probability.Distributions.Geometric
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
h : ∀ (n : ℕ), (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal = (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ i * (↑p : ℝ))).toReal * ‖f i‖

Tactic:
convert! (integrable_geometricMeasure_iff hp).1 hf with n

Premises used: ProbabilityTheory.integrable_geometricMeasure_iff, Iff.mp
-- Module: Mathlib.Probability.Distributions.Geometric
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 : ℕ
h h₁ : (1 - (↑p : ℝ)) ^ n * (↑p : ℝ) = (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)
⊢ (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal = (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)

Tactic:
rw [ENNReal.toReal_ofReal (geometricMeasure_nonneg p n)]

Premises used: ProbabilityTheory.geometricMeasure_nonneg, ENNReal.toReal_ofReal
-- Module: Mathlib.Probability.Distributions.Geometric
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} (α := E) (∫ (n : ℕ), f n ∂geometricMeasure p) (∑' (n : ℕ), ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n)

Tactic:
(hasSum_integral_geometricMeasure hp hf).tsum_eq.symm

Premises used: HasSum.tsum_eq, ProbabilityTheory.hasSum_integral_geometricMeasure, Eq.symm
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : (↑unitInterval : Type)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
hp : p ≠ 0
f : ℕ → E
⊢ ∀ (i : ℕ), ENNReal.ofReal ((1 - (↑p : ℝ)) ^ i * (↑p : ℝ)) ≠ ∞

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : (↑unitInterval : Type)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
hp : p ≠ 0
f : ℕ → E
e_f : ∀ (n : ℕ), (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal • f n = ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n
⊢ Eq.{u_1 + 1} (α := E) (∑' (i : ℕ), (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ i * (↑p : ℝ))).toReal • f i)
    (∑' (n : ℕ), ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n)

Tactic:
congr with n
-- Module: Mathlib.Probability.Distributions.Geometric
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 : ℕ
e_f e_f₁ : ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n = ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n
⊢ (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal • f n = ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) • f n

Tactic:
rw [ENNReal.toReal_ofReal (geometricMeasure_nonneg p n)]

Premises used: ProbabilityTheory.geometricMeasure_nonneg, ENNReal.toReal_ofReal
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
⊢ 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)
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
this : HasSum (fun (n : ℕ) ↦ (1 - p) ^ n) (1 - (1 - p))⁻¹
⊢ HasSum (fun (i : ℕ) ↦ (1 - p) ^ i * p) ((1 - (1 - p))⁻¹ * p)

Tactic:
apply (hasSum_mul_right_iff (hp_pos.ne')).mpr at this

Premises used: Iff.mpr, hasSum_mul_right_iff, LT.lt.ne'
-- Module: Mathlib.Probability.Distributions.Geometric
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 (i : ℕ) ↦ (1 - p) ^ i * p) (p⁻¹ * p)

Tactic:
simp only [sub_sub_cancel] at this

Premises used: sub_sub_cancel
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
this : HasSum (fun (i : ℕ) ↦ (1 - p) ^ i * p) (p⁻¹ * p)
⊢ HasSum (α := ℝ) (fun (i : ℕ) ↦ (1 - p) ^ i * p) 1

Tactic:
rw [inv_mul_eq_div, div_self hp_pos.ne'] at this

Premises used: inv_mul_eq_div, LT.lt.ne', div_self
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
this : HasSum (α := ℝ) (fun (i : ℕ) ↦ (1 - p) ^ i * p) 1
⊢ HasSum (α := ℝ) (fun (n : ℕ) ↦ (1 - p) ^ n * p) 1

Tactic:
this
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
this : HasSum (α := ℝ) (fun (i : ℕ) ↦ (1 - p) ^ i * p) 1
⊢ HasSum (α := ℝ) (fun (n : ℕ) ↦ (1 - p) ^ n * p) 1

Tactic:
exact this
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : ℝ
n : ℕ
hp_pos : 0 < p
hp_lt_one : p < 1
positivity positivity₁ positivity₂ positivity₃ : 0 < 1 - p → 0 < (1 - p) ^ n * p
⊢ 0 < (1 - p) ^ n * p

Tactic:
positivity [sub_pos.mpr hp_lt_one]

Premises used: Iff.mpr, sub_pos
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : ℝ
n : ℕ
hp_pos : 0 < p
hp_le_one : p ≤ 1
positivity positivity₁ positivity₂ positivity₃ : 0 ≤ 1 - p → 0 ≤ (1 - p) ^ n * p
⊢ 0 ≤ (1 - p) ^ n * p

Tactic:
positivity [sub_nonneg.mpr hp_le_one]

Premises used: Iff.mpr, sub_nonneg
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p_1 : (↑unitInterval : Type)
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
apply : HasSum (α := ℝ≥0) (fun (a : ℕ) ↦ (geometricPMFReal p a).toNNReal) 1
⊢ HasSum (α := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal (geometricPMFReal p n)) 1

Tactic:
apply ENNReal.hasSum_coe.mpr

Premises used: Iff.mpr, ENNReal.hasSum_coe
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p_1 : (↑unitInterval : Type)
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
rw : HasSum (fun (a : ℕ) ↦ (geometricPMFReal p a).toNNReal) (toNNReal 1)
⊢ HasSum (α := ℝ≥0) (fun (a : ℕ) ↦ (geometricPMFReal p a).toNNReal) 1

Tactic:
rw [← toNNReal_one]

Premises used: Real.toNNReal_one
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p_1 : (↑unitInterval : Type)
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
⊢ HasSum (fun (a : ℕ) ↦ (geometricPMFReal p a).toNNReal) (toNNReal 1)

Tactic:
(geometricPMFRealSum hp_pos hp_le_one).toNNReal
      (fun n ↦ geometricPMFReal_nonneg hp_pos hp_le_one)

Premises used: HasSum.toNNReal, ProbabilityTheory.geometricPMFReal_nonneg, ProbabilityTheory.geometricPMFRealSum
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p_1 : (↑unitInterval : Type)
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
⊢ HasSum (fun (a : ℕ) ↦ (geometricPMFReal p a).toNNReal) (toNNReal 1)

Tactic:
exact (geometricPMFRealSum hp_pos hp_le_one).toNNReal
      (fun n ↦ geometricPMFReal_nonneg hp_pos hp_le_one)

Premises used: HasSum.toNNReal, ProbabilityTheory.geometricPMFReal_nonneg, ProbabilityTheory.geometricPMFRealSum
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : ℝ
funProp : Nat.instMeasurableSpace ≤ Nat.instMeasurableSpace
⊢ Measurable (geometricPMFReal p)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : ℝ
⊢ StronglyMeasurable (geometricPMFReal p)

Tactic:
stronglyMeasurable_iff_measurable.mpr measurable_geometricPMFReal

Premises used: Iff.mpr, ProbabilityTheory.measurable_geometricPMFReal, stronglyMeasurable_iff_measurable
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r x : ℝ
⊢ paretoPDF t r x = ENNReal.ofReal (if t ≤ x then r * t ^ r * x ^ (-(r + 1)) else 0)

Tactic:
rfl

Premises used: ProbabilityTheory.paretoPDFReal, ProbabilityTheory.paretoPDF, rfl
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r x : ℝ
hx : x < t
⊢ paretoPDF t r x = 0

Tactic:
simp only [paretoPDF_eq, if_neg (not_le.mpr hx), ENNReal.ofReal_zero]

Premises used: not_le, Iff.mpr, ProbabilityTheory.paretoPDF_eq, ENNReal.ofReal_zero, if_neg
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r x : ℝ
hx : t ≤ x
⊢ paretoPDF t r x = ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))

Tactic:
simp only [paretoPDF_eq, if_pos hx]

Premises used: if_pos, ProbabilityTheory.paretoPDF_eq
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r x : ℝ
hx : x ≤ t
rw : ∫⁻ (x : ℝ) in Iio x, 0 = 0
rw₁ : EqOn (paretoPDF t r) (fun (x : ℝ) ↦ 0) (Iio x)
⊢ ∫⁻ (y : ℝ) in Iio x, paretoPDF t r y = 0

Tactic:
rw [setLIntegral_congr_fun (g := fun _ ↦ 0) measurableSet_Iio]

Premises used: measurableSet_Iio, MeasureTheory.setLIntegral_congr_fun
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r x : ℝ
hx : x ≤ t
rw : Eq (α := ℝ≥0∞) 0 0
rw₁ rw₂ : ENNReal.ofReal 0 = ENNReal.ofReal 0
⊢ ∫⁻ (x : ℝ) in Iio x, 0 = 0

Tactic:
rw [lintegral_zero, ← ENNReal.ofReal_zero]

Premises used: MeasureTheory.lintegral_zero, ENNReal.ofReal_zero
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r x : ℝ
hx : x ≤ t
a : ℝ
a₁ : a < x → paretoPDF t r a = (fun (x : ℝ) ↦ (0 : ℝ≥0∞)) a
⊢ a ∈ Iio x → paretoPDF t r a = (fun (x : ℝ) ↦ (0 : ℝ≥0∞)) a

Tactic:
(_ : a < _)
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r x : ℝ
hx : x ≤ t
a : ℝ
h : a < x
simp : (if t ≤ a then r * t ^ r * a ^ (-(r + 1)) else 0) ≤ 0
⊢ paretoPDF t r a = (fun (x : ℝ) ↦ (0 : ℝ≥0∞)) a

Tactic:
simp only [paretoPDF_eq, ENNReal.ofReal_eq_zero]

Premises used: ENNReal.ofReal_eq_zero, ProbabilityTheory.paretoPDF_eq
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r x : ℝ
hx : x ≤ t
a : ℝ
h : a < x
linarith : t ≤ a → x - t + (a - x) + (t - a) = 0
⊢ ¬t ≤ a

Tactic:
linarith
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r x : ℝ
hx : x ≤ t
a : ℝ
h : a < x
rw rw₁ : LE.le (α := ℝ) 0 0
⊢ (if t ≤ a then r * t ^ r * a ^ (-(r + 1)) else 0) ≤ 0

Tactic:
rw [if_neg (by linarith)]

Premises used: if_neg
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
⊢ Measurable (paretoPDFReal t r)

Tactic:
Measurable.ite measurableSet_Ici ((measurable_id.pow_const _).const_mul _) measurable_const

Premises used: measurable_id, ProbabilityTheory.paretoPDFReal, Measurable.ite, measurable_const, Measurable.const_mul, Measurable.pow_const, measurableSet_Ici
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
⊢ StronglyMeasurable (paretoPDFReal t r)

Tactic:
(measurable_paretoPDFReal t r).stronglyMeasurable

Premises used: Measurable.stronglyMeasurable, ProbabilityTheory.measurable_paretoPDFReal
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r x : ℝ
ht : 0 < t
hr : 0 < r
hx : t ≤ x
rw : 0 < r * t ^ r * x ^ (-(r + 1))
⊢ 0 < paretoPDFReal t r x

Tactic:
rw [paretoPDFReal, if_pos hx]

Premises used: ProbabilityTheory.paretoPDFReal, if_pos
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r x : ℝ
ht : 0 < t
hr : 0 < r
hx : t ≤ x
linarith : x ≤ 0 → 0 - t + (t - x) + (x - 0) = 0
⊢ 0 < x

Tactic:
linarith
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r x : ℝ
ht : 0 < t
hr : 0 < r
hx : t ≤ x
⊢ 0 < x

Tactic:
have _ : 0 < x := by linarith
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r x : ℝ
ht : 0 < t
hr : 0 < r
hx : t ≤ x
h : 0 < x
⊢ 0 < r * t ^ r * x ^ (-(r + 1))

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
pos : ∀ (h : t ≤ x), 0 ≤ r * t ^ r * x ^ (-(r + 1))
neg : ∀ (h : ¬t ≤ x), LE.le (α := ℝ) 0 0
⊢ 0 ≤ if t ≤ x then r * t ^ r * x ^ (-(r + 1)) else 0

Tactic:
split_ifs with h
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : t ≤ x
ht0 : 0 = t
⊢ 0 ≤ x

Tactic:
rw [← ht0] at h
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : t ≤ x
ht0 : 0 = t
h₁ : 0 ≤ x
⊢ 0 = t

Tactic:
rw [← ht0] at h
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : 0 ≤ x
ht0 : 0 = t
⊢ 0 ≤ r * t ^ r * x ^ (-(r + 1))

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : t ≤ x
htp : 0 < t
pos pos₁ pos₂ pos₃ : 0 < x → 0 ≤ r * t ^ r * x ^ (-(r + 1))
⊢ 0 ≤ r * t ^ r * x ^ (-(r + 1))

Tactic:
positivity [lt_of_lt_of_le htp h]

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : t ≤ 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]

Premises used: le_iff_eq_or_lt, Iff.mp
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : ¬t ≤ x
⊢ LE.le (α := ℝ) 0 0

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
⊢ ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0

Tactic:
have leftSide : ∫⁻ x in Iio t, paretoPDF t r x = 0 := lintegral_paretoPDF_of_le (le_refl t)
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
⊢ ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))

Tactic:
have rightSide : ∫⁻ x in Ici t, paretoPDF t r x =
      ∫⁻ x in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1))) :=
    setLIntegral_congr_fun measurableSet_Ici (fun _ ↦ paretoPDF_of_le)
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici t)) fun (a : ℝ) ↦
      r * t ^ r * a ^ (-(r + 1)))
    1
hf :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ici t))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
    r * t ^ r * x ^ (-(r + 1))
hfm :
  AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ r * t ^ r * x ^ (-(r + 1)))
    (Measure.restrict volume (Ici t))
⊢ ∫⁻ (x : ℝ), paretoPDF t r x = 1

Tactic:
rw [← ENNReal.toReal_eq_one_iff, ← lintegral_add_compl _ measurableSet_Ici, compl_Ici,
    leftSide, rightSide, add_zero, ← integral_eq_lintegral_of_nonneg_ae]

Premises used: MeasureTheory.lintegral_add_compl, MeasureTheory.integral_eq_lintegral_of_nonneg_ae, Set.compl_Ici, add_zero, measurableSet_Ici, ENNReal.toReal_eq_one_iff
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
rw : r * t ^ r * (-t ^ (-(r + 1) + 1) / (-(r + 1) + 1)) = 1
rw₁ : -(r + 1) < -1
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici t)) fun (a : ℝ) ↦
      r * t ^ r * a ^ (-(r + 1)))
    1

Tactic:
rw [integral_Ici_eq_integral_Ioi, integral_const_mul, integral_Ioi_rpow_of_lt _ ht]

Premises used: MeasureTheory.integral_Ici_eq_integral_Ioi, MeasureTheory.integral_const_mul, integral_Ioi_rpow_of_lt
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
⊢ r * t ^ r * (-t ^ (-(r + 1) + 1) / (-(r + 1) + 1)) = 1

Tactic:
simp [field, ← rpow_add ht]

Premises used: Real.rpow_add
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
linarith : -1 ≤ -(r + 1) → 0 - r + (-1 - -(r + 1)) = 0
⊢ -(r + 1) < -1

Tactic:
linarith
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
hf : ∀ᵐ (x : ℝ), x ∈ Ici t → 0 x ≤ r * t ^ r * x ^ (-(r + 1))
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ici t))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
    r * t ^ r * x ^ (-(r + 1))

Tactic:
rw [EventuallyLE, ae_restrict_iff' measurableSet_Ici]

Premises used: MeasureTheory.ae_restrict_iff', Filter.EventuallyLE, measurableSet_Ici
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
x : ℝ
hx : x ∈ Ici t
positivity positivity₁ positivity₂ positivity₃ : 0 < x → 0 x ≤ r * t ^ r * x ^ (-(r + 1))
⊢ 0 x ≤ r * t ^ r * x ^ (-(r + 1))

Tactic:
positivity [lt_of_lt_of_le ht hx]

Premises used: lt_of_lt_of_le