awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
hX_int₂ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ -HPow.hPow (β := ℕ) (X ω) 2) μ
hX_int₁ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ (a + b) * X ω) μ
h0 : 0 ≤ -∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ + (a + b) * ∫ (x : Ω), X x ∂μ - a * b
_ : Var[X; μ] ≤ (a + b) * ∫ (x : Ω), X x ∂μ - a * b - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2
_₁ :
  (a + b) * ∫ (x : Ω), X x ∂μ - a * b - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2 =
    (b - ∫ (x : Ω), X x ∂μ) * (∫ (x : Ω), X x ∂μ - a)
⊢ Var[X; μ] ≤ (b - ∫ (x : Ω), X x ∂μ) * (∫ (x : Ω), X x ∂μ - a)

Tactic:
calc
    _ ≤ (a + b) * μ[X] - a * b - μ[X] ^ 2 := by
      rw [variance_eq_sub (memLp_of_bounded h hX.aestronglyMeasurable 2)]
      linarith
    _ = (b - μ[X]) * (μ[X] - a) := by ring

Premises used: HSub.hSub, HAdd.hAdd, MeasureTheory.integral
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
⊢ (b - ∫ (x : Ω), X x ∂μ) * (∫ (x : Ω), X x ∂μ - a) =
    HPow.hPow (β := ℕ) ((b - a) / 2) 2 - HPow.hPow (β := ℕ) (∫ (x : Ω), X x ∂μ - (b + a) / 2) 2

Tactic:
ring
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
X : Ω → ℝ
Y : Ω' → ℝ
hfμ : MemLp X 2 μ
hgν : MemLp Y 2 ν
⊢ Var[fun (p : Ω × Ω') ↦ X p.1 + Y p.2; μ.prod ν] = Var[X; μ] + Var[Y; ν]

Tactic:
(IndepFun.variance_fun_add (hfμ.comp_fst ν) (hgν.comp_snd μ) ?_).trans ?_

Premises used: MeasureTheory.MemLp.comp_snd, ProbabilityTheory.IndepFun.variance_fun_add, MeasureTheory.MemLp.comp_fst, Eq.trans
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
X : Ω → ℝ
Y : Ω' → ℝ
hfμ : MemLp X 2 μ
hgν : MemLp Y 2 ν
refine_1 : (fun (x : Ω × Ω') ↦ X x.1) ⟂ᵢ[μ.prod ν] fun (x : Ω × Ω') ↦ Y x.2
refine_2 : Var[fun (x : Ω × Ω') ↦ X x.1; μ.prod ν] + Var[fun (x : Ω × Ω') ↦ Y x.2; μ.prod ν] = Var[X; μ] + Var[Y; ν]
⊢ Var[fun (p : Ω × Ω') ↦ X p.1 + Y p.2; μ.prod ν] = Var[X; μ] + Var[Y; ν]

Tactic:
refine (IndepFun.variance_fun_add (hfμ.comp_fst ν) (hgν.comp_snd μ) ?_).trans ?_

Premises used: MeasureTheory.MemLp.comp_snd, ProbabilityTheory.IndepFun.variance_fun_add, MeasureTheory.MemLp.comp_fst, Eq.trans
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
X : Ω → ℝ
Y : Ω' → ℝ
hfμ : MemLp X 2 μ
hgν : MemLp Y 2 ν
⊢ (fun (x : Ω × Ω') ↦ X x.1) ⟂ᵢ[μ.prod ν] fun (x : Ω × Ω') ↦ Y x.2

Tactic:
indepFun_prod₀ hfμ.aemeasurable hgν.aemeasurable

Premises used: MeasureTheory.MemLp.aemeasurable, ProbabilityTheory.indepFun_prod₀
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
X : Ω → ℝ
Y : Ω' → ℝ
hfμ : MemLp X 2 μ
hgν : MemLp Y 2 ν
⊢ (fun (x : Ω × Ω') ↦ X x.1) ⟂ᵢ[μ.prod ν] fun (x : Ω × Ω') ↦ Y x.2

Tactic:
exact indepFun_prod₀ hfμ.aemeasurable hgν.aemeasurable

Premises used: MeasureTheory.MemLp.aemeasurable, ProbabilityTheory.indepFun_prod₀
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
X : Ω → ℝ
Y : Ω' → ℝ
hfμ : MemLp X 2 μ
hgν : MemLp Y 2 ν
refine_2 : Var[X; μ] + Var[fun (x : Ω × Ω') ↦ Y x.2; μ.prod ν] = Var[X; μ] + Var[Y; ν]
refine_2₁ refine_2₂ : Var[X; μ] + Var[Y; ν] = Var[X; μ] + Var[Y; ν]
⊢ Var[fun (x : Ω × Ω') ↦ X x.1; μ.prod ν] + Var[fun (x : Ω × Ω') ↦ Y x.2; μ.prod ν] = Var[X; μ] + Var[Y; ν]

Tactic:
rw [measurePreserving_fst.variance_fun_comp hfμ.aemeasurable,
      measurePreserving_snd.variance_fun_comp hgν.aemeasurable]

Premises used: MeasureTheory.MemLp.aemeasurable, MeasureTheory.measurePreserving_snd, MeasureTheory.MeasurePreserving.variance_fun_comp, MeasureTheory.measurePreserving_fst
-- Module: Mathlib.Probability.Moments.Variance
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
inst_4 : IsProbabilityMeasure μ
ν : Measure F
inst_5 : IsProbabilityMeasure ν
L : StrongDual ℝ (E × F)
hLμ : MemLp (ε := ℝ) (⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → ℝ) 2 μ
hLν : MemLp (ε := ℝ) (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → ℝ) 2 ν
h :
  ∀ (x : E × F),
    (L : (a : E × F) → ℝ) x =
      HAdd.hAdd (α := ℝ) (β := ℝ) ((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → ℝ) x.1 : ℝ)
        ((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → ℝ) x.2 : ℝ)
⊢ Eq (α := (a : E × F) → ℝ) (⇑L : (a : E × F) → ℝ) fun (x : E × F) ↦
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → ℝ) x.1 : ℝ)
      ((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → ℝ) x.2 : ℝ)

Tactic:
ext
-- Module: Mathlib.Probability.Moments.Variance
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
inst_4 : IsProbabilityMeasure μ
ν : Measure F
inst_5 : IsProbabilityMeasure ν
L : StrongDual ℝ (E × F)
hLμ : MemLp (ε := ℝ) (⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → ℝ) 2 μ
hLν : MemLp (ε := ℝ) (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → ℝ) 2 ν
x : E × F
h h₁ : Eq (α := ℝ) ((L : (a : E × F) → ℝ) x : ℝ) ((L : (a : E × F) → ℝ) x : ℝ)
⊢ (L : (a : E × F) → ℝ) x =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → ℝ) x.1 : ℝ)
      ((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → ℝ) x.2 : ℝ)

Tactic:
rw [L.comp_inl_add_comp_inr]

Premises used: ContinuousLinearMap.comp_inl_add_comp_inr
-- Module: Mathlib.Probability.Moments.Variance
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
inst_4 : IsProbabilityMeasure μ
ν : Measure F
inst_5 : IsProbabilityMeasure ν
L : StrongDual ℝ (E × F)
hLμ : MemLp (ε := ℝ) (⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → ℝ) 2 μ
hLν : MemLp (ε := ℝ) (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → ℝ) 2 ν
⊢ Eq (α := (a : E × F) → ℝ) (⇑L : (a : E × F) → ℝ) fun (x : E × F) ↦
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → ℝ) x.1 : ℝ)
      ((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → ℝ) x.2 : ℝ)

Tactic:
have : L = fun x : E × F ↦ L.comp (.inl ℝ E F) x.1 + L.comp (.inr ℝ E F) x.2 := by
    ext; rw [L.comp_inl_add_comp_inr]
-- Module: Mathlib.Probability.Moments.Variance
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
inst_4 : IsProbabilityMeasure μ
ν : Measure F
inst_5 : IsProbabilityMeasure ν
L : StrongDual ℝ (E × F)
hLμ : MemLp (ε := ℝ) (⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → ℝ) 2 μ
hLν : MemLp (ε := ℝ) (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → ℝ) 2 ν
this :
  Eq (α := (a : E × F) → ℝ) (⇑L : (a : E × F) → ℝ) fun (x : E × F) ↦
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → ℝ) x.1 : ℝ)
      ((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → ℝ) x.2 : ℝ)
rw :
  Var[fun (x : E × F) ↦
      HAdd.hAdd (α := ℝ) (β := ℝ) ((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → ℝ) x.1 : ℝ)
        ((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → ℝ) x.2 : ℝ);
      μ.prod ν] =
    Var[(⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → ℝ); μ] +
      Var[(⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → ℝ); ν]
rw₁ rw₂ :
  Var[(⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → ℝ); μ] +
      Var[(⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → ℝ); ν] =
    Var[(⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → ℝ); μ] +
      Var[(⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → ℝ); ν]
⊢ Var[(⇑L : (a : E × F) → ℝ); μ.prod ν] =
    Var[(⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → ℝ); μ] +
      Var[(⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → ℝ); ν]

Tactic:
rw [this, variance_add_prod hLμ hLν]

Premises used: ProbabilityTheory.variance_add_prod
-- Module: Mathlib.Probability.Moments.Variance
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
inst_4 : IsProbabilityMeasure μ
ν : Measure F
inst_5 : IsProbabilityMeasure ν
L : StrongDual ℝ (E × F)
hLμ : MemLp id 2 μ
hLν : MemLp id 2 ν
⊢ Var[(⇑L : (a : E × F) → ℝ); μ.prod ν] =
    Var[(⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → ℝ); μ] +
      Var[(⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → ℝ); ν]

Tactic:
variance_dual_prod' (ContinuousLinearMap.comp_memLp' _ hLμ)
    (ContinuousLinearMap.comp_memLp' _ hLν)

Premises used: ContinuousLinearMap.comp_memLp', ProbabilityTheory.variance_dual_prod'
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p q : PMF α
h : ∀ (x : α), Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) x : ℝ≥0∞) ((q : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
⊢ p = q

Tactic:
DFunLike.ext p q h

Premises used: DFunLike.ext
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
⊢ HasSum (α := ℝ≥0∞) (⇑p : (a : α) → ℝ≥0∞) 1

Tactic:
p.2

Premises used: Subtype.property
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
⊢ Eq (α := ℝ≥0∞) (∑' (a : α), (p : (a : α) → ℝ≥0∞) a) 1

Tactic:
p.hasSum_coe_one.tsum_eq

Premises used: HasSum.tsum_eq, PMF.hasSum_coe_one
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
⊢ Ne (α := ℝ≥0∞) (∑' (a : α), (p : (a : α) → ℝ≥0∞) a) ∞

Tactic:
p.tsum_coe.symm ▸ ENNReal.one_ne_top

Premises used: PMF.tsum_coe, Eq.rec, Eq.symm, ENNReal.one_ne_top
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
s : Set α
⊢ Ne (α := ℝ≥0∞) (∑' (a : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) a) ∞

Tactic:
ne_of_lt (lt_of_le_of_lt
    (ENNReal.tsum_le_tsum (fun _ => Set.indicator_apply_le fun _ => le_rfl))
    (lt_of_le_of_ne le_top p.tsum_coe_ne_top))

Premises used: lt_of_le_of_lt, ENNReal.tsum_le_tsum, le_rfl, PMF.tsum_coe_ne_top, le_top, Set.indicator_apply_le, ne_of_lt, lt_of_le_of_ne
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
⊢ Ne (α := (a : α) → ℝ≥0∞) (⇑p : (a : α) → ℝ≥0∞) 0

Tactic:
fun hp =>
  zero_ne_one ((tsum_zero.symm.trans (tsum_congr fun x => symm (congr_fun hp x))).trans p.tsum_coe)

Premises used: PMF.tsum_coe, tsum_congr, zero_ne_one, tsum_zero, symm, congr_fun, Eq.symm, Not, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
⊢ a ∈ p.support ↔ Ne (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, PMF.support, Function.support, Not
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
⊢ p.support.Nonempty

Tactic:
Function.support_nonempty_iff.2 p.coe_ne_zero

Premises used: Iff.mpr, PMF.support, PMF.coe_ne_zero, Function.support_nonempty_iff
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
⊢ p.support.Countable

Tactic:
Summable.countable_support_ennreal (tsum_coe_ne_top p)

Premises used: PMF.support, PMF.tsum_coe_ne_top, Summable.countable_support_ennreal
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
rw :
  Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ↔ ¬Ne (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ↔ Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ↔ a ∉ p.support

Tactic:
rw [mem_support_iff, Classical.not_not]

Premises used: Classical.not_not, PMF.mem_support_iff
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ↔ a ∈ p.support

Tactic:
pos_iff_ne_zero.trans (p.mem_support_iff a).symm

Premises used: PMF.mem_support_iff, Iff.trans, pos_iff_ne_zero, Iff.symm
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
⊢ Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞) ↔ p.support = {a}

Tactic:
⟨fun h => Set.Subset.antisymm (fun a' ha' => by_contra fun ha => ?_)
    fun a' ha' => ha'.symm ▸ (p.mem_support_iff a).2 fun ha => zero_ne_one <| ha.symm.trans h,
    fun h => _root_.trans (symm <| tsum_eq_single a
      fun a' ha' => (p.apply_eq_zero_iff a').2 (h.symm ▸ ha')) p.tsum_coe⟩

Premises used: PMF.tsum_coe, Set.Subset.antisymm, Iff.mpr, trans, Eq.rec, zero_ne_one, PMF.apply_eq_zero_iff, PMF.mem_support_iff, Iff.intro, tsum_eq_single, by_contra, symm, Eq.symm, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
refine :
  ∀ (h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)) (a' : α) (ha' : a' ∈ p.support) (ha : a' ∉ {a}),
    False
⊢ Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞) ↔ p.support = {a}

Tactic:
refine ⟨fun h => Set.Subset.antisymm (fun a' ha' => by_contra fun ha => ?_)
    fun a' ha' => ha'.symm ▸ (p.mem_support_iff a).2 fun ha => zero_ne_one <| ha.symm.trans h,
    fun h => _root_.trans (symm <| tsum_eq_single a
      fun a' ha' => (p.apply_eq_zero_iff a').2 (h.symm ▸ ha')) p.tsum_coe⟩
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
suffices : LT.lt (α := ℝ≥0∞) 1 (∑' (a : α), (p : (a : α) → ℝ≥0∞) a)
⊢ False

Tactic:
suffices 1 < ∑' a, p a from ne_of_lt this p.tsum_coe.symm
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
rw : ∃ (x : α), Ne (α := ℝ≥0∞) (if x = a then 0 else (p : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) 0 (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b)

Tactic:
rw [pos_iff_ne_zero, ENNReal.summable.tsum_ne_zero_iff]

Premises used: ENNReal.summable, Summable.tsum_ne_zero_iff, pos_iff_ne_zero
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
⊢ ∃ (x : α), Ne (α := ℝ≥0∞) (if x = a then 0 else (p : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
⟨a', ite_ne_left_iff.2 ⟨ha, Ne.symm <| (p.mem_support_iff a').2 ha'⟩⟩

Premises used: Iff.mpr, Ne.symm, ite_ne_left_iff, PMF.mem_support_iff, And.intro, Exists.intro
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
⊢ ∃ (x : α), Ne (α := ℝ≥0∞) (if x = a then 0 else (p : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact ⟨a', ite_ne_left_iff.2 ⟨ha, Ne.symm <| (p.mem_support_iff a').2 ha'⟩⟩
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
⊢ LT.lt (α := ℝ≥0∞) 0 (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b)

Tactic:
have : 0 < ∑' b, ite (b = a) 0 (p b) := by
    rw [pos_iff_ne_zero, ENNReal.summable.tsum_ne_zero_iff]
    exact ⟨a', ite_ne_left_iff.2 ⟨ha, Ne.symm <| (p.mem_support_iff a').2 ha'⟩⟩
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
this : LT.lt (α := ℝ≥0∞) 0 (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b)
⊢ 1 = HAdd.hAdd (α := ℝ≥0∞) 1 0

Tactic:
(add_zero 1).symm

Premises used: add_zero, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
this : LT.lt (α := ℝ≥0∞) 0 (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b)
⊢ HAdd.hAdd (α := ℝ≥0∞) 1 0 <
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b : ℝ≥0∞)

Tactic:
(ENNReal.add_lt_add_of_le_of_lt ENNReal.one_ne_top (le_of_eq h.symm) this)

Premises used: ENNReal.add_lt_add_of_le_of_lt, le_of_eq, Eq.symm, ENNReal.one_ne_top
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
this : LT.lt (α := ℝ≥0∞) 0 (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b)
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (if True then (p : (a : α) → ℝ≥0∞) a else 0 : ℝ≥0∞)
      (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
rw₁ rw₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (if a = a then (p : (a : α) → ℝ≥0∞) a else 0 : ℝ≥0∞)
      (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b : ℝ≥0∞)

Tactic:
rw [eq_self_iff_true, if_true]

Premises used: if_true, eq_self_iff_true
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
this : LT.lt (α := ℝ≥0∞) 0 (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b)
e_a :
  Eq (α := ℝ≥0∞) (if a = a then (p : (a : α) → ℝ≥0∞) a else 0 : ℝ≥0∞)
    (∑' (b : α), if b = a then (p : (a : α) → ℝ≥0∞) b else 0 : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (if a = a then (p : (a : α) → ℝ≥0∞) a else 0 : ℝ≥0∞)
      (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (∑' (b : α), if b = a then (p : (a : α) → ℝ≥0∞) b else 0)
      (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b)

Tactic:
congr
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
this : LT.lt (α := ℝ≥0∞) 0 (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b)
⊢ Eq (α := ℝ≥0∞) (if a = a then (p : (a : α) → ℝ≥0∞) a else 0 : ℝ≥0∞)
    (∑' (b : α), if b = a then (p : (a : α) → ℝ≥0∞) b else 0 : ℝ≥0∞)

Tactic:
symm (tsum_eq_single a fun b hb => if_neg hb)

Premises used: tsum_eq_single, symm, if_neg
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
this : LT.lt (α := ℝ≥0∞) 0 (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b)
⊢ Eq (α := ℝ≥0∞) (if a = a then (p : (a : α) → ℝ≥0∞) a else 0 : ℝ≥0∞)
    (∑' (b : α), if b = a then (p : (a : α) → ℝ≥0∞) b else 0 : ℝ≥0∞)

Tactic:
exact symm (tsum_eq_single a fun b hb => if_neg hb)

Premises used: tsum_eq_single, symm, if_neg
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
this : LT.lt (α := ℝ≥0∞) 0 (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b)
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑' (b : α), if b = a then (p : (a : α) → ℝ≥0∞) b else 0)
      (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b) =
    ∑' (b : α),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (if b = a then (p : (a : α) → ℝ≥0∞) b else 0 : ℝ≥0∞)
        (if b = a then 0 else (p : (a : α) → ℝ≥0∞) b : ℝ≥0∞)

Tactic:
ENNReal.tsum_add.symm

Premises used: ENNReal.tsum_add, Eq.symm
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
this : LT.lt (α := ℝ≥0∞) 0 (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b)
b : α
pos : b = a → HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞) = (p : (a : α) → ℝ≥0∞) b
neg : ¬b = a → HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) b : ℝ≥0∞) = (p : (a : α) → ℝ≥0∞) b
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (if b = a then (p : (a : α) → ℝ≥0∞) b else 0 : ℝ≥0∞)
      (if b = a then 0 else (p : (a : α) → ℝ≥0∞) b : ℝ≥0∞) =
    (p : (a : α) → ℝ≥0∞) b

Tactic:
split_ifs
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
this : LT.lt (α := ℝ≥0∞) 0 (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b)
b : α
h_1 : b = a
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞) = (p : (a : α) → ℝ≥0∞) b

Tactic:
simp only [zero_add, add_zero]

Premises used: zero_add, add_zero
-- Module: Mathlib.Probability.ProbabilityMassFunction.Basic
Goal:
α : Type u_1
p : PMF α
a : α
h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
this : LT.lt (α := ℝ≥0∞) 0 (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b)
b : α
h_1 : ¬b = a
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) b : ℝ≥0∞) = (p : (a : α) → ℝ≥0∞) b

Tactic:
simp only [zero_add, add_zero]

Premises used: zero_add, add_zero