awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
h'' : ¬∀ i ∈ s, X i =ᶠ[ae μ] 0
j : ι
hj1 : j ∈ s
hj2 : ¬X j =ᶠ[ae μ] 0
h' : s.Nontrivial
k : ι
hk1 : k ∈ s
hk2 : k ≠ j
this : IsProbabilityMeasure μ
neg : ∀ (i : ι) (hi : i ∈ s), ∑ j ∈ s, cov[X i, X j; μ] = Var[X i; μ]
⊢ Eq (α := ℝ) (∑ i ∈ s, ∑ j ∈ s, cov[X i, X j; μ]) (∑ i ∈ s, Var[X i; μ])

Tactic:
refine Finset.sum_congr rfl (fun i hi ↦ ?_)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
h'' : ¬∀ i ∈ s, X i =ᶠ[ae μ] 0
j : ι
hj1 : j ∈ s
hj2 : ¬X j =ᶠ[ae μ] 0
h' : s.Nontrivial
k : ι
hk1 : k ∈ s
hk2 : k ≠ j
this : IsProbabilityMeasure μ
i : ι
hi : i ∈ s
neg : ∑ j ∈ s, cov[X i, X j; μ] = cov[X i, X i; μ]
⊢ ∑ j ∈ s, cov[X i, X j; μ] = Var[X i; μ]

Tactic:
rw [← covariance_self (hs i hi).aemeasurable]

Premises used: MeasureTheory.MemLp.aemeasurable, ProbabilityTheory.covariance_self
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
h'' : ¬∀ i ∈ s, X i =ᶠ[ae μ] 0
j : ι
hj1 : j ∈ s
hj2 : ¬X j =ᶠ[ae μ] 0
h' : s.Nontrivial
k : ι
hk1 : k ∈ s
hk2 : k ≠ j
this : IsProbabilityMeasure μ
i : ι
hi : i ∈ s
⊢ ∑ j ∈ s, cov[X i, X j; μ] = cov[X i, X i; μ]

Tactic:
Finset.sum_eq_single_of_mem i hi fun j hj1 hj2 ↦ ?_

Premises used: Finset.sum_eq_single_of_mem
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
h'' : ¬∀ i ∈ s, X i =ᶠ[ae μ] 0
j : ι
hj1 : j ∈ s
hj2 : ¬X j =ᶠ[ae μ] 0
h' : s.Nontrivial
k : ι
hk1 : k ∈ s
hk2 : k ≠ j
this : IsProbabilityMeasure μ
i : ι
hi : i ∈ s
neg : ∀ (j : ι) (hj1 : j ∈ s) (hj2 : j ≠ i), cov[X i, X j; μ] = 0
⊢ ∑ j ∈ s, cov[X i, X j; μ] = cov[X i, X i; μ]

Tactic:
refine Finset.sum_eq_single_of_mem i hi fun j hj1 hj2 ↦ ?_

Premises used: Finset.sum_eq_single_of_mem
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
h'' : ¬∀ i ∈ s, X i =ᶠ[ae μ] 0
j_1 : ι
hj1_1 : j_1 ∈ s
hj2_1 : ¬X j_1 =ᶠ[ae μ] 0
h' : s.Nontrivial
k : ι
hk1 : k ∈ s
hk2 : k ≠ j_1
this : IsProbabilityMeasure μ
i : ι
hi : i ∈ s
j : ι
hj1 : j ∈ s
hj2 : j ≠ i
⊢ cov[X i, X j; μ] = 0

Tactic:
(h hi hj1 hj2.symm).covariance_eq_zero (hs i hi) (hs j hj1)

Premises used: Ne.symm, ProbabilityTheory.IndepFun.covariance_eq_zero
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
h'' : ¬∀ i ∈ s, X i =ᶠ[ae μ] 0
j_1 : ι
hj1_1 : j_1 ∈ s
hj2_1 : ¬X j_1 =ᶠ[ae μ] 0
h' : s.Nontrivial
k : ι
hk1 : k ∈ s
hk2 : k ≠ j_1
this : IsProbabilityMeasure μ
i : ι
hi : i ∈ s
j : ι
hj1 : j ∈ s
hj2 : j ≠ i
⊢ cov[X i, X j; μ] = 0

Tactic:
exact (h hi hj1 hj2.symm).covariance_eq_zero (hs i hi) (hs j hj1)

Premises used: Ne.symm, ProbabilityTheory.IndepFun.covariance_eq_zero
-- Module: Mathlib.Probability.Moments.Variance
Goal:
ι : Type u_2
inst : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
rw : Eq (α := ℝ) (∑ i : ι, Var[fun (ω : (i : ι) → Ω i) ↦ X i (ω i); Measure.pi (α := Ω) μ]) (∑ i : ι, Var[X i; μ i])
hs :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) univ i →
      MemLp (ε := ℝ) (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) 2 (Measure.pi (α := Ω) μ)
h₁ :
  (↑univ : Set ι).Pairwise fun (i j : ι) ↦
    (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) ⟂ᵢ[Measure.pi (α := Ω) μ] fun (ω : (i : ι) → Ω i) ↦ X j (ω j)
⊢ Var[∑ i : ι, fun (ω : (i : ι) → Ω i) ↦ X i (ω i); Measure.pi (α := Ω) μ] = ∑ i : ι, Var[X i; μ i]

Tactic:
rw [IndepFun.variance_sum]

Premises used: ProbabilityTheory.IndepFun.variance_sum
-- Module: Mathlib.Probability.Moments.Variance
Goal:
ι : Type u_2
inst : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
e_f : ∀ (i : ι), Var[fun (ω : (i : ι) → Ω i) ↦ X i (ω i); Measure.pi (α := Ω) μ] = Var[X i; μ i]
⊢ Eq (α := ℝ) (∑ i : ι, Var[fun (ω : (i : ι) → Ω i) ↦ X i (ω i); Measure.pi (α := Ω) μ]) (∑ i : ι, Var[X i; μ i])

Tactic:
congr with i
-- Module: Mathlib.Probability.Moments.Variance
Goal:
ι : Type u_2
inst : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
i : ι
e_f : Var[X i ∘ fun (ω : (i : ι) → Ω i) ↦ ω i; Measure.pi (α := Ω) μ] = Var[X i; μ i]
⊢ Var[fun (ω : (i : ι) → Ω i) ↦ X i (ω i); Measure.pi (α := Ω) μ] = Var[X i; μ i]

Tactic:
change Var[(X i) ∘ (fun ω ↦ ω i); Measure.pi μ] = _

Premises used: MeasureTheory.Measure.pi
-- Module: Mathlib.Probability.Moments.Variance
Goal:
ι : Type u_2
inst : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
i : ι
e_f : AEMeasurable (_m := mΩ i) (X i) (Measure.map (fun (ω : (i : ι) → Ω i) ↦ ω i) (Measure.pi (α := Ω) μ))
e_f₁ : AEMeasurable (β := Ω i) (fun (ω : (i : ι) → Ω i) ↦ ω i) (Measure.pi (α := Ω) μ)
⊢ Var[X i ∘ fun (ω : (i : ι) → Ω i) ↦ ω i; Measure.pi (α := Ω) μ] = Var[X i; μ i]

Tactic:
rw [← variance_map, (measurePreserving_eval _ i).map_eq]

Premises used: MeasureTheory.measurePreserving_eval, MeasureTheory.MeasurePreserving.map_eq, ProbabilityTheory.variance_map
-- Module: Mathlib.Probability.Moments.Variance
Goal:
ι : Type u_2
inst : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
i : ι
e_f : AEMeasurable (X i) (μ i)
⊢ AEMeasurable (_m := mΩ i) (X i) (Measure.map (fun (ω : (i : ι) → Ω i) ↦ ω i) (Measure.pi (α := Ω) μ))

Tactic:
rw [(measurePreserving_eval _ i).map_eq]

Premises used: MeasureTheory.measurePreserving_eval, MeasureTheory.MeasurePreserving.map_eq
-- Module: Mathlib.Probability.Moments.Variance
Goal:
ι : Type u_2
inst : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
i : ι
⊢ AEMeasurable (X i) (μ i)

Tactic:
(h i).aestronglyMeasurable.aemeasurable

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, MeasureTheory.MemLp.aestronglyMeasurable
-- Module: Mathlib.Probability.Moments.Variance
Goal:
ι : Type u_2
inst : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
i : ι
⊢ AEMeasurable (X i) (μ i)

Tactic:
exact (h i).aestronglyMeasurable.aemeasurable

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, MeasureTheory.MemLp.aestronglyMeasurable
-- Module: Mathlib.Probability.Moments.Variance
Goal:
ι : Type u_2
inst : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
i : ι
⊢ Measurable (β := Ω i) fun (ω : (i : ι) → Ω i) ↦ ω i

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.Variance
Goal:
ι : Type u_2
inst : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
i : ι
⊢ AEMeasurable (β := Ω i) (fun (ω : (i : ι) → Ω i) ↦ ω i) (Measure.pi (α := Ω) μ)

Tactic:
exact Measurable.aemeasurable (by fun_prop)

Premises used: Measurable.aemeasurable
-- Module: Mathlib.Probability.Moments.Variance
Goal:
ι : Type u_2
inst : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
⊢ ∀ (i : ι),
    Membership.mem (γ := Finset ι) univ i →
      MemLp (ε := ℝ) (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) 2 (Measure.pi (α := Ω) μ)

Tactic:
fun i _ ↦ (h i).comp_measurePreserving (measurePreserving_eval _ i)

Premises used: MeasureTheory.measurePreserving_eval, MeasureTheory.MemLp.comp_measurePreserving
-- Module: Mathlib.Probability.Moments.Variance
Goal:
ι : Type u_2
inst : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
⊢ ∀ (i : ι),
    Membership.mem (γ := Finset ι) univ i →
      MemLp (ε := ℝ) (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) 2 (Measure.pi (α := Ω) μ)

Tactic:
exact fun i _ ↦ (h i).comp_measurePreserving (measurePreserving_eval _ i)

Premises used: MeasureTheory.measurePreserving_eval, MeasureTheory.MemLp.comp_measurePreserving
-- Module: Mathlib.Probability.Moments.Variance
Goal:
ι : Type u_2
inst : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
⊢ (↑univ : Set ι).Pairwise fun (i j : ι) ↦
    (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) ⟂ᵢ[Measure.pi (α := Ω) μ] fun (ω : (i : ι) → Ω i) ↦ X j (ω j)

Tactic:
fun i _ j _ hij ↦
      (iIndepFun_pi fun i ↦ (h i).aestronglyMeasurable.aemeasurable).indepFun hij

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, ProbabilityTheory.iIndepFun_pi, Set.Pairwise, ProbabilityTheory.iIndepFun.indepFun, MeasureTheory.MemLp.aestronglyMeasurable
-- Module: Mathlib.Probability.Moments.Variance
Goal:
ι : Type u_2
inst : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
⊢ (↑univ : Set ι).Pairwise fun (i j : ι) ↦
    (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) ⟂ᵢ[Measure.pi (α := Ω) μ] fun (ω : (i : ι) → Ω i) ↦ X j (ω j)

Tactic:
exact fun i _ j _ hij ↦
      (iIndepFun_pi fun i ↦ (h i).aestronglyMeasurable.aemeasurable).indepFun hij

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, ProbabilityTheory.iIndepFun_pi, ProbabilityTheory.iIndepFun.indepFun, MeasureTheory.MemLp.aestronglyMeasurable
-- 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 μ
⊢ ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω

Tactic:
have ha : ∀ᵐ ω ∂μ, a ≤ X ω := h.mono fun ω h => h.1
-- 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 ω
⊢ ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b

Tactic:
have hb : ∀ᵐ ω ∂μ, X ω ≤ b := h.mono fun ω h => h.2
-- 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
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ -HPow.hPow (β := ℕ) (X ω) 2) μ

Tactic:
have hX_int₂ : Integrable (fun ω ↦ -X ω ^ 2) μ :=
    (memLp_of_bounded h hX.aestronglyMeasurable 2).integrable_sq.neg
-- 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) μ
ω : Ω
⊢ a ≤ X ω → X ω ≤ b → ‖X ω‖ ≤ max |a| |b|

Tactic:
abs_le_max_abs_abs

Premises used: abs_le_max_abs_abs
-- 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) μ
h₁ :
  ∀ (a_1 : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (ω : Ω) ↦ a ≤ X ω) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              Membership.mem (γ := Set Ω) {x : Ω | (fun (ω : Ω) ↦ X ω ≤ b) x} x →
                Membership.mem (γ := Set Ω) {x : Ω | (fun (a_4 : Ω) ↦ ‖X a_4‖ ≤ max |a| |b|) x} x}
            x}
      a_1
h₂ h₃ : ∀ (ω : Ω), a ≤ X ω → X ω ≤ b → ‖X ω‖ ≤ max |a| |b|
⊢ ∀ᵐ (a_1 : Ω) ∂μ, ‖X a_1‖ ≤ max |a| |b|

Tactic:
filter_upwards [ha, hb] with ω using abs_le_max_abs_abs

Premises used: abs_le_max_abs_abs
-- 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) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ (a + b) * X ω) μ

Tactic:
have hX_int₁ : Integrable (fun ω ↦ (a + b) * X ω) μ :=
    ((integrable_const (max |a| |b|)).mono' hX.aestronglyMeasurable
      (by filter_upwards [ha, hb] with ω using abs_le_max_abs_abs)).const_mul (a + b)
-- 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 ω) μ
hf : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : Ω) ↦ (b - X x) * (X x - a)
⊢ LE.le (α := ℝ) 0 (∫ (ω : Ω), (b - X ω) * (X ω - a) ∂μ)

Tactic:
apply integral_nonneg_of_ae

Premises used: MeasureTheory.integral_nonneg_of_ae
-- 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 ω) μ
h₁ : ∀ (ω : Ω) (ha' : a ≤ X ω) (hb' : X ω ≤ b), 0 ω ≤ (b - X ω) * (X ω - a)
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : Ω) ↦ (b - X x) * (X x - a)

Tactic:
filter_upwards [ha, hb] with ω ha' hb'
-- 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 ω) μ
ω : Ω
ha' : a ≤ X ω
hb' : X ω ≤ b
linarith : b - X ω < 0 → X ω - b + (b - X ω - 0) = 0
⊢ 0 ≤ b - X ω

Tactic:
linarith
-- 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 ω) μ
ω : Ω
ha' : a ≤ X ω
hb' : X ω ≤ b
linarith : X ω - a < 0 → a - X ω + (X ω - a - 0) = 0
⊢ 0 ≤ X ω - a

Tactic:
linarith
-- 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 ω) μ
ω : Ω
ha' : a ≤ X ω
hb' : X ω ≤ b
⊢ 0 ω ≤ (b - X ω) * (X ω - a)

Tactic:
exact mul_nonneg (by linarith : 0 ≤ b - X ω) (by linarith : 0 ≤ X ω - a)

Premises used: mul_nonneg
-- 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 ω) μ
ω : Ω
⊢ Eq (α := ℝ) ((fun (ω : Ω) ↦ (b - X ω) * (X ω - a)) ω)
    ((fun (ω : Ω) ↦ -HPow.hPow (β := ℕ) (X ω) 2 + (a + b) * X ω - a * b) ω)

Tactic:
ring
-- 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 ω) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ -HPow.hPow (β := ℕ) (X ω) 2 + (a + b) * X ω) μ

Tactic:
fun_prop
-- 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 ω) μ
⊢ HSub.hSub (α := ℝ) (∫ (ω : Ω), -HPow.hPow (β := ℕ) (X ω) 2 + (a + b) * X ω ∂μ) (∫ (x : Ω), a * b ∂μ) =
    ∫ (ω : Ω), -HPow.hPow (β := ℕ) (X ω) 2 + (a + b) * X ω ∂μ - a * b

Tactic:
simp
-- 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 ω) μ
⊢ ∫ (ω : Ω), -HPow.hPow (β := ℕ) (X ω) 2 + (a + b) * X ω ∂μ - a * b =
    -∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ + (a + b) * ∫ (x : Ω), X x ∂μ - a * b

Tactic:
simp [← integral_neg, ← integral_const_mul, integral_add hX_int₂ hX_int₁]

Premises used: MeasureTheory.integral_const_mul, MeasureTheory.integral_neg, MeasureTheory.integral_add
-- 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 ω) μ
⊢ 0 ≤ -∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ + (a + b) * ∫ (x : Ω), X x ∂μ - a * b

Tactic:
have h0 : 0 ≤ -μ[X ^ 2] + (a + b) * μ[X] - a * b :=
    calc
      _ ≤ ∫ ω, (b - X ω) * (X ω - a) ∂μ := by
        apply integral_nonneg_of_ae
        filter_upwards [ha, hb] with ω ha' hb'
        exact mul_nonneg (by linarith : 0 ≤ b - X ω) (by linarith : 0 ≤ X ω - a)
      _ = ∫ ω, -X ω ^ 2 + (a + b) * X ω - a * b ∂μ :=
        integral_congr_ae <| ae_of_all μ fun ω ↦ by ring
      _ = ∫ ω, - X ω ^ 2 + (a + b) * X ω ∂μ - ∫ _, a * b ∂μ :=
        integral_sub (by fun_prop) (integrable_const (a * b))
      _ = ∫ ω, - X ω ^ 2 + (a + b) * X ω ∂μ - a * b := by simp
      _ = - μ[X ^ 2] + (a + b) * μ[X] - a * b := by
        simp [← integral_neg, ← integral_const_mul, integral_add hX_int₂ hX_int₁]
-- 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
rw :
  ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2 ≤
    (a + b) * ∫ (x : Ω), X x ∂μ - a * b - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2
⊢ Var[X; μ] ≤ (a + b) * ∫ (x : Ω), X x ∂μ - a * b - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2

Tactic:
rw [variance_eq_sub (memLp_of_bounded h hX.aestronglyMeasurable 2)]

Premises used: AEMeasurable.aestronglyMeasurable, ProbabilityTheory.variance_eq_sub, MeasureTheory.memLp_of_bounded, OfNat.ofNat
-- 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
linarith :
  (a + b) * ∫ (x : Ω), X x ∂μ - a * b - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2 <
      ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2 →
    0 - (-∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ + (a + b) * ∫ (x : Ω), X x ∂μ - a * b) +
        ((a + b) * ∫ (x : Ω), X x ∂μ - a * b - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2 -
          (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2)) =
      0
⊢ ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2 ≤
    (a + b) * ∫ (x : Ω), X x ∂μ - a * b - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2

Tactic:
linarith
-- 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
⊢ (a + b) * ∫ (x : Ω), X x ∂μ - a * b - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2 =
    (b - ∫ (x : Ω), X x ∂μ) * (∫ (x : Ω), X x ∂μ - a)

Tactic:
ring