JaxLean.Stdlib.FiniteLaw

JaxLean
Stdlib
FiniteLaw

import JaxLean.Stdlib.Batch
import Mathlib.Data.Real.Basic
import Mathlib.Data.Fintype.BigOperators
import Mathlib.Tactic

Exact finite probability, separate from any particular sampler or program. A random variable is a function on outcomes. Reusing that function preserves dependence; prod explicitly constructs independent sample spaces.

namespace JaxLeanopen scoped BigOperators

structure FiniteLaw (Ω : Type) [Fintype Ω] where
  mass : Ω → ℝ
  nonneg : ∀ ω, 0 ≤ mass ω
  total : ∑ ω, mass ω = 1

namespace FiniteLawvariable {Ω Ξ : Type} [Fintype Ω] [Fintype Ξ]

noncomputable def mean (p : FiniteLaw Ω) (X : Ω → ℝ) : ℝ :=
  ∑ ω, p.mass ω * X ω

noncomputable def variance (p : FiniteLaw Ω) (X : Ω → ℝ) : ℝ :=
  p.mean (fun ω => (X ω - p.mean X) ^ 2)

noncomputable def covariance (p : FiniteLaw Ω) (X Y : Ω → ℝ) : ℝ :=
  p.mean (fun ω => (X ω - p.mean X) * (Y ω - p.mean Y))

@[simp] theorem mean_const (p : FiniteLaw Ω) (c : ℝ) :
    p.mean (fun _ => c) = c := byΩ:Typeinst✝:Fintype Ωp:FiniteLaw Ωc:ℝ⊢ (p.mean fun x => c) = c
  simp [mean, ← Finset.sum_mul, p.total]All goals completed! 🐙

theorem mean_add (p : FiniteLaw Ω) (X Y : Ω → ℝ) :
    p.mean (fun ω => X ω + Y ω) = p.mean X + p.mean Y := byΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝY:Ω → ℝ⊢ (p.mean fun ω => X ω + Y ω) = p.mean X + p.mean Y
  simp [mean, mul_add, Finset.sum_add_distrib]All goals completed! 🐙

theorem mean_sub (p : FiniteLaw Ω) (X Y : Ω → ℝ) :
    p.mean (fun ω => X ω - Y ω) = p.mean X - p.mean Y := byΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝY:Ω → ℝ⊢ (p.mean fun ω => X ω - Y ω) = p.mean X - p.mean Y
  simp [mean, mul_sub, Finset.sum_sub_distrib]All goals completed! 🐙

theorem mean_scale (p : FiniteLaw Ω) (a : ℝ) (X : Ω → ℝ) :
    p.mean (fun ω => a * X ω) = a * p.mean X := byΩ:Typeinst✝:Fintype Ωp:FiniteLaw Ωa:ℝX:Ω → ℝ⊢ (p.mean fun ω => a * X ω) = a * p.mean X
  simp [mean, mul_left_comm, Finset.mul_sum]All goals completed! 🐙

Expectation is just a linear functional on a space of value functions.

noncomputable def meanLinear (p : FiniteLaw Ω) : (Ω → ℝ) →ₗ[ℝ] ℝ where
  toFun := p.mean
  map_add' := p.mean_add
  map_smul' := p.mean_scale

Reduction commutation is generic linear algebra, without independence.


theorem mean_sum {ι : Type} [Fintype ι] (p : FiniteLaw Ω) (X : ι → Ω → ℝ) :
    p.mean (fun ω => ∑ i, X i ω) = ∑ i, p.mean (X i) := byΩ:Typeinst✝¹:Fintype Ωι:Typeinst✝:Fintype ιp:FiniteLaw ΩX:ι → Ω → ℝ⊢ (p.mean fun ω => ∑ i, X i ω) = ∑ i, p.mean (X i)
  have h : (fun ω => ∑ i, X i ω) = ∑ i, X i := by
    funext ωΩ:Typeinst✝¹:Fintype Ωι:Typeinst✝:Fintype ιp:FiniteLaw ΩX:ι → Ω → ℝω:Ω⊢ ∑ i, X i ω = (∑ i, X i) ωΩ:Typeinst✝¹:Fintype Ωι:Typeinst✝:Fintype ιp:FiniteLaw ΩX:ι → Ω → ℝh:(fun ω => ∑ i, X i ω) = ∑ i, X i⊢ (p.mean fun ω => ∑ i, X i ω) = ∑ i, p.mean (X i)
    simp only [Finset.sum_apply]Ω:Typeinst✝¹:Fintype Ωι:Typeinst✝:Fintype ιp:FiniteLaw ΩX:ι → Ω → ℝh:(fun ω => ∑ i, X i ω) = ∑ i, X i⊢ (p.mean fun ω => ∑ i, X i ω) = ∑ i, p.mean (X i)Ω:Typeinst✝¹:Fintype Ωι:Typeinst✝:Fintype ιp:FiniteLaw ΩX:ι → Ω → ℝh:(fun ω => ∑ i, X i ω) = ∑ i, X i⊢ (p.mean fun ω => ∑ i, X i ω) = ∑ i, p.mean (X i)
  rw [hΩ:Typeinst✝¹:Fintype Ωι:Typeinst✝:Fintype ιp:FiniteLaw ΩX:ι → Ω → ℝh:(fun ω => ∑ i, X i ω) = ∑ i, X i⊢ p.mean (∑ i, X i) = ∑ i, p.mean (X i)Ω:Typeinst✝¹:Fintype Ωι:Typeinst✝:Fintype ιp:FiniteLaw ΩX:ι → Ω → ℝh:(fun ω => ∑ i, X i ω) = ∑ i, X i⊢ p.mean (∑ i, X i) = ∑ i, p.mean (X i)]Ω:Typeinst✝¹:Fintype Ωι:Typeinst✝:Fintype ιp:FiniteLaw ΩX:ι → Ω → ℝh:(fun ω => ∑ i, X i ω) = ∑ i, X i⊢ p.mean (∑ i, X i) = ∑ i, p.mean (X i)
  exact Batch.linear_reduceSum p.meanLinear XAll goals completed! 🐙



theorem mean_affine (p : FiniteLaw Ω) (X : Ω → ℝ) (a b : ℝ) :
    p.mean (fun ω => a * X ω + b) = a * p.mean X + b := byΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝb:ℝ⊢ (p.mean fun ω => a * X ω + b) = a * p.mean X + b
  rw [mean_add,Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝb:ℝ⊢ ((p.mean fun ω => a * X ω) + p.mean fun ω => b) = a * p.mean X + bAll goals completed! 🐙 mean_scale,Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝb:ℝ⊢ (a * p.mean X + p.mean fun ω => b) = a * p.mean X + bAll goals completed! 🐙 mean_constΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝb:ℝ⊢ a * p.mean X + b = a * p.mean X + bAll goals completed! 🐙]All goals completed! 🐙

theorem variance_nonneg (p : FiniteLaw Ω) (X : Ω → ℝ) :
    0 ≤ p.variance X := byΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝ⊢ 0 ≤ p.variance X
  exact Finset.sum_nonneg (fun ω _ => mul_nonneg (p.nonneg ω) (sq_nonneg _))All goals completed! 🐙

Useful after a nonlinear operation: retain the second moment, not just the mean.


theorem variance_eq_second_moment (p : FiniteLaw Ω) (X : Ω → ℝ) :
    p.variance X = p.mean (fun ω => X ω ^ 2) - p.mean X ^ 2 := byΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝ⊢ p.variance X = (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2
  unfold varianceΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝ⊢ (p.mean fun ω => (X ω - p.mean X) ^ 2) = (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2
  have h : (fun ω => (X ω - p.mean X) ^ 2) =
      (fun ω => X ω ^ 2 - (2 * p.mean X) * X ω + p.mean X ^ 2) := byΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝ⊢ p.variance X = (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝh:(fun ω => (X ω - p.mean X) ^ 2) = fun ω => X ω ^ 2 - 2 * p.mean X * X ω + p.mean X ^ 2⊢ (p.mean fun ω => (X ω - p.mean X) ^ 2) = (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2
    funext ωΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝω:Ω⊢ (X ω - p.mean X) ^ 2 = X ω ^ 2 - 2 * p.mean X * X ω + p.mean X ^ 2Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝh:(fun ω => (X ω - p.mean X) ^ 2) = fun ω => X ω ^ 2 - 2 * p.mean X * X ω + p.mean X ^ 2⊢ (p.mean fun ω => (X ω - p.mean X) ^ 2) = (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2
    ringΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝh:(fun ω => (X ω - p.mean X) ^ 2) = fun ω => X ω ^ 2 - 2 * p.mean X * X ω + p.mean X ^ 2⊢ (p.mean fun ω => (X ω - p.mean X) ^ 2) = (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝh:(fun ω => (X ω - p.mean X) ^ 2) = fun ω => X ω ^ 2 - 2 * p.mean X * X ω + p.mean X ^ 2⊢ (p.mean fun ω => (X ω - p.mean X) ^ 2) = (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2
  rw [h,Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝh:(fun ω => (X ω - p.mean X) ^ 2) = fun ω => X ω ^ 2 - 2 * p.mean X * X ω + p.mean X ^ 2⊢ (p.mean fun ω => X ω ^ 2 - 2 * p.mean X * X ω + p.mean X ^ 2) = (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝh:(fun ω => (X ω - p.mean X) ^ 2) = fun ω => X ω ^ 2 - 2 * p.mean X * X ω + p.mean X ^ 2⊢ (p.mean fun ω => X ω ^ 2) - 2 * p.mean X * p.mean X + p.mean X ^ 2 = (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2 mean_add,Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝh:(fun ω => (X ω - p.mean X) ^ 2) = fun ω => X ω ^ 2 - 2 * p.mean X * X ω + p.mean X ^ 2⊢ ((p.mean fun ω => X ω ^ 2 - 2 * p.mean X * X ω) + p.mean fun ω => p.mean X ^ 2) =
  (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝh:(fun ω => (X ω - p.mean X) ^ 2) = fun ω => X ω ^ 2 - 2 * p.mean X * X ω + p.mean X ^ 2⊢ (p.mean fun ω => X ω ^ 2) - 2 * p.mean X * p.mean X + p.mean X ^ 2 = (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2 mean_sub,Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝh:(fun ω => (X ω - p.mean X) ^ 2) = fun ω => X ω ^ 2 - 2 * p.mean X * X ω + p.mean X ^ 2⊢ (((p.mean fun ω => X ω ^ 2) - p.mean fun ω => 2 * p.mean X * X ω) + p.mean fun ω => p.mean X ^ 2) =
  (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝh:(fun ω => (X ω - p.mean X) ^ 2) = fun ω => X ω ^ 2 - 2 * p.mean X * X ω + p.mean X ^ 2⊢ (p.mean fun ω => X ω ^ 2) - 2 * p.mean X * p.mean X + p.mean X ^ 2 = (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2 mean_scale,Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝh:(fun ω => (X ω - p.mean X) ^ 2) = fun ω => X ω ^ 2 - 2 * p.mean X * X ω + p.mean X ^ 2⊢ ((p.mean fun ω => X ω ^ 2) - 2 * p.mean X * p.mean X + p.mean fun ω => p.mean X ^ 2) =
  (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝh:(fun ω => (X ω - p.mean X) ^ 2) = fun ω => X ω ^ 2 - 2 * p.mean X * X ω + p.mean X ^ 2⊢ (p.mean fun ω => X ω ^ 2) - 2 * p.mean X * p.mean X + p.mean X ^ 2 = (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2 mean_constΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝh:(fun ω => (X ω - p.mean X) ^ 2) = fun ω => X ω ^ 2 - 2 * p.mean X * X ω + p.mean X ^ 2⊢ (p.mean fun ω => X ω ^ 2) - 2 * p.mean X * p.mean X + p.mean X ^ 2 = (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝh:(fun ω => (X ω - p.mean X) ^ 2) = fun ω => X ω ^ 2 - 2 * p.mean X * X ω + p.mean X ^ 2⊢ (p.mean fun ω => X ω ^ 2) - 2 * p.mean X * p.mean X + p.mean X ^ 2 = (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2]Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝh:(fun ω => (X ω - p.mean X) ^ 2) = fun ω => X ω ^ 2 - 2 * p.mean X * X ω + p.mean X ^ 2⊢ (p.mean fun ω => X ω ^ 2) - 2 * p.mean X * p.mean X + p.mean X ^ 2 = (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2
  ringAll goals completed! 🐙



theorem variance_affine (p : FiniteLaw Ω) (X : Ω → ℝ) (a b : ℝ) :
    p.variance (fun ω => a * X ω + b) = a ^ 2 * p.variance X := byΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝb:ℝ⊢ (p.variance fun ω => a * X ω + b) = a ^ 2 * p.variance X
  unfold varianceΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝb:ℝ⊢ (p.mean fun ω => ((fun ω => a * X ω + b) ω - p.mean fun ω => a * X ω + b) ^ 2) =
  a ^ 2 * p.mean fun ω => (X ω - p.mean X) ^ 2
  rw [mean_affineΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝb:ℝ⊢ (p.mean fun ω => ((fun ω => a * X ω + b) ω - (a * p.mean X + b)) ^ 2) = a ^ 2 * p.mean fun ω => (X ω - p.mean X) ^ 2Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝb:ℝ⊢ (p.mean fun ω => ((fun ω => a * X ω + b) ω - (a * p.mean X + b)) ^ 2) = a ^ 2 * p.mean fun ω => (X ω - p.mean X) ^ 2]Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝb:ℝ⊢ (p.mean fun ω => ((fun ω => a * X ω + b) ω - (a * p.mean X + b)) ^ 2) = a ^ 2 * p.mean fun ω => (X ω - p.mean X) ^ 2
  have h : (fun ω => (a * X ω + b - (a * p.mean X + b)) ^ 2) =
      (fun ω => a ^ 2 * (X ω - p.mean X) ^ 2) := byΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝb:ℝ⊢ (p.variance fun ω => a * X ω + b) = a ^ 2 * p.variance XΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝb:ℝh:(fun ω => (a * X ω + b - (a * p.mean X + b)) ^ 2) = fun ω => a ^ 2 * (X ω - p.mean X) ^ 2⊢ (p.mean fun ω => ((fun ω => a * X ω + b) ω - (a * p.mean X + b)) ^ 2) = a ^ 2 * p.mean fun ω => (X ω - p.mean X) ^ 2
    funext ωΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝb:ℝω:Ω⊢ (a * X ω + b - (a * p.mean X + b)) ^ 2 = a ^ 2 * (X ω - p.mean X) ^ 2Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝb:ℝh:(fun ω => (a * X ω + b - (a * p.mean X + b)) ^ 2) = fun ω => a ^ 2 * (X ω - p.mean X) ^ 2⊢ (p.mean fun ω => ((fun ω => a * X ω + b) ω - (a * p.mean X + b)) ^ 2) = a ^ 2 * p.mean fun ω => (X ω - p.mean X) ^ 2
    ringΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝb:ℝh:(fun ω => (a * X ω + b - (a * p.mean X + b)) ^ 2) = fun ω => a ^ 2 * (X ω - p.mean X) ^ 2⊢ (p.mean fun ω => ((fun ω => a * X ω + b) ω - (a * p.mean X + b)) ^ 2) = a ^ 2 * p.mean fun ω => (X ω - p.mean X) ^ 2Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝb:ℝh:(fun ω => (a * X ω + b - (a * p.mean X + b)) ^ 2) = fun ω => a ^ 2 * (X ω - p.mean X) ^ 2⊢ (p.mean fun ω => ((fun ω => a * X ω + b) ω - (a * p.mean X + b)) ^ 2) = a ^ 2 * p.mean fun ω => (X ω - p.mean X) ^ 2
  rw [h,Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝb:ℝh:(fun ω => (a * X ω + b - (a * p.mean X + b)) ^ 2) = fun ω => a ^ 2 * (X ω - p.mean X) ^ 2⊢ (p.mean fun ω => a ^ 2 * (X ω - p.mean X) ^ 2) = a ^ 2 * p.mean fun ω => (X ω - p.mean X) ^ 2All goals completed! 🐙 mean_scaleΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝb:ℝh:(fun ω => (a * X ω + b - (a * p.mean X + b)) ^ 2) = fun ω => a ^ 2 * (X ω - p.mean X) ^ 2⊢ (a ^ 2 * p.mean fun ω => (X ω - p.mean X) ^ 2) = a ^ 2 * p.mean fun ω => (X ω - p.mean X) ^ 2All goals completed! 🐙]All goals completed! 🐙

No independence assumption: reusing a draw contributes covariance.


theorem variance_add (p : FiniteLaw Ω) (X Y : Ω → ℝ) :
    p.variance (fun ω => X ω + Y ω) =
      p.variance X + p.variance Y + 2 * p.covariance X Y := byΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝY:Ω → ℝ⊢ (p.variance fun ω => X ω + Y ω) = p.variance X + p.variance Y + 2 * p.covariance X Y
  unfold variance covarianceΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝY:Ω → ℝ⊢ (p.mean fun ω => ((fun ω => X ω + Y ω) ω - p.mean fun ω => X ω + Y ω) ^ 2) =
  ((p.mean fun ω => (X ω - p.mean X) ^ 2) + p.mean fun ω => (Y ω - p.mean Y) ^ 2) +
    2 * p.mean fun ω => (X ω - p.mean X) * (Y ω - p.mean Y)
  rw [mean_addΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝY:Ω → ℝ⊢ (p.mean fun ω => ((fun ω => X ω + Y ω) ω - (p.mean X + p.mean Y)) ^ 2) =
  ((p.mean fun ω => (X ω - p.mean X) ^ 2) + p.mean fun ω => (Y ω - p.mean Y) ^ 2) +
    2 * p.mean fun ω => (X ω - p.mean X) * (Y ω - p.mean Y)Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝY:Ω → ℝ⊢ (p.mean fun ω => ((fun ω => X ω + Y ω) ω - (p.mean X + p.mean Y)) ^ 2) =
  ((p.mean fun ω => (X ω - p.mean X) ^ 2) + p.mean fun ω => (Y ω - p.mean Y) ^ 2) +
    2 * p.mean fun ω => (X ω - p.mean X) * (Y ω - p.mean Y)]Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝY:Ω → ℝ⊢ (p.mean fun ω => ((fun ω => X ω + Y ω) ω - (p.mean X + p.mean Y)) ^ 2) =
  ((p.mean fun ω => (X ω - p.mean X) ^ 2) + p.mean fun ω => (Y ω - p.mean Y) ^ 2) +
    2 * p.mean fun ω => (X ω - p.mean X) * (Y ω - p.mean Y)
  have h : (fun ω => (X ω + Y ω - (p.mean X + p.mean Y)) ^ 2) =
      (fun ω => (X ω - p.mean X) ^ 2 + (Y ω - p.mean Y) ^ 2 +
        2 * ((X ω - p.mean X) * (Y ω - p.mean Y))) := byΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝY:Ω → ℝ⊢ (p.variance fun ω => X ω + Y ω) = p.variance X + p.variance Y + 2 * p.covariance X YΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝY:Ω → ℝh:(fun ω => (X ω + Y ω - (p.mean X + p.mean Y)) ^ 2) = fun ω =>
  (X ω - p.mean X) ^ 2 + (Y ω - p.mean Y) ^ 2 + 2 * ((X ω - p.mean X) * (Y ω - p.mean Y))⊢ (p.mean fun ω => ((fun ω => X ω + Y ω) ω - (p.mean X + p.mean Y)) ^ 2) =
  ((p.mean fun ω => (X ω - p.mean X) ^ 2) + p.mean fun ω => (Y ω - p.mean Y) ^ 2) +
    2 * p.mean fun ω => (X ω - p.mean X) * (Y ω - p.mean Y)
    funext ωΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝY:Ω → ℝω:Ω⊢ (X ω + Y ω - (p.mean X + p.mean Y)) ^ 2 =
  (X ω - p.mean X) ^ 2 + (Y ω - p.mean Y) ^ 2 + 2 * ((X ω - p.mean X) * (Y ω - p.mean Y))Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝY:Ω → ℝh:(fun ω => (X ω + Y ω - (p.mean X + p.mean Y)) ^ 2) = fun ω =>
  (X ω - p.mean X) ^ 2 + (Y ω - p.mean Y) ^ 2 + 2 * ((X ω - p.mean X) * (Y ω - p.mean Y))⊢ (p.mean fun ω => ((fun ω => X ω + Y ω) ω - (p.mean X + p.mean Y)) ^ 2) =
  ((p.mean fun ω => (X ω - p.mean X) ^ 2) + p.mean fun ω => (Y ω - p.mean Y) ^ 2) +
    2 * p.mean fun ω => (X ω - p.mean X) * (Y ω - p.mean Y)
    ringΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝY:Ω → ℝh:(fun ω => (X ω + Y ω - (p.mean X + p.mean Y)) ^ 2) = fun ω =>
  (X ω - p.mean X) ^ 2 + (Y ω - p.mean Y) ^ 2 + 2 * ((X ω - p.mean X) * (Y ω - p.mean Y))⊢ (p.mean fun ω => ((fun ω => X ω + Y ω) ω - (p.mean X + p.mean Y)) ^ 2) =
  ((p.mean fun ω => (X ω - p.mean X) ^ 2) + p.mean fun ω => (Y ω - p.mean Y) ^ 2) +
    2 * p.mean fun ω => (X ω - p.mean X) * (Y ω - p.mean Y)Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝY:Ω → ℝh:(fun ω => (X ω + Y ω - (p.mean X + p.mean Y)) ^ 2) = fun ω =>
  (X ω - p.mean X) ^ 2 + (Y ω - p.mean Y) ^ 2 + 2 * ((X ω - p.mean X) * (Y ω - p.mean Y))⊢ (p.mean fun ω => ((fun ω => X ω + Y ω) ω - (p.mean X + p.mean Y)) ^ 2) =
  ((p.mean fun ω => (X ω - p.mean X) ^ 2) + p.mean fun ω => (Y ω - p.mean Y) ^ 2) +
    2 * p.mean fun ω => (X ω - p.mean X) * (Y ω - p.mean Y)
  rw [h,Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝY:Ω → ℝh:(fun ω => (X ω + Y ω - (p.mean X + p.mean Y)) ^ 2) = fun ω =>
  (X ω - p.mean X) ^ 2 + (Y ω - p.mean Y) ^ 2 + 2 * ((X ω - p.mean X) * (Y ω - p.mean Y))⊢ (p.mean fun ω => (X ω - p.mean X) ^ 2 + (Y ω - p.mean Y) ^ 2 + 2 * ((X ω - p.mean X) * (Y ω - p.mean Y))) =
  ((p.mean fun ω => (X ω - p.mean X) ^ 2) + p.mean fun ω => (Y ω - p.mean Y) ^ 2) +
    2 * p.mean fun ω => (X ω - p.mean X) * (Y ω - p.mean Y)All goals completed! 🐙 mean_add,Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝY:Ω → ℝh:(fun ω => (X ω + Y ω - (p.mean X + p.mean Y)) ^ 2) = fun ω =>
  (X ω - p.mean X) ^ 2 + (Y ω - p.mean Y) ^ 2 + 2 * ((X ω - p.mean X) * (Y ω - p.mean Y))⊢ ((p.mean fun ω => (X ω - p.mean X) ^ 2 + (Y ω - p.mean Y) ^ 2) +
    p.mean fun ω => 2 * ((X ω - p.mean X) * (Y ω - p.mean Y))) =
  ((p.mean fun ω => (X ω - p.mean X) ^ 2) + p.mean fun ω => (Y ω - p.mean Y) ^ 2) +
    2 * p.mean fun ω => (X ω - p.mean X) * (Y ω - p.mean Y)All goals completed! 🐙 mean_add,Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝY:Ω → ℝh:(fun ω => (X ω + Y ω - (p.mean X + p.mean Y)) ^ 2) = fun ω =>
  (X ω - p.mean X) ^ 2 + (Y ω - p.mean Y) ^ 2 + 2 * ((X ω - p.mean X) * (Y ω - p.mean Y))⊢ (((p.mean fun ω => (X ω - p.mean X) ^ 2) + p.mean fun ω => (Y ω - p.mean Y) ^ 2) +
    p.mean fun ω => 2 * ((X ω - p.mean X) * (Y ω - p.mean Y))) =
  ((p.mean fun ω => (X ω - p.mean X) ^ 2) + p.mean fun ω => (Y ω - p.mean Y) ^ 2) +
    2 * p.mean fun ω => (X ω - p.mean X) * (Y ω - p.mean Y)All goals completed! 🐙 mean_scaleΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝY:Ω → ℝh:(fun ω => (X ω + Y ω - (p.mean X + p.mean Y)) ^ 2) = fun ω =>
  (X ω - p.mean X) ^ 2 + (Y ω - p.mean Y) ^ 2 + 2 * ((X ω - p.mean X) * (Y ω - p.mean Y))⊢ (((p.mean fun ω => (X ω - p.mean X) ^ 2) + p.mean fun ω => (Y ω - p.mean Y) ^ 2) +
    2 * p.mean fun ω => (X ω - p.mean X) * (Y ω - p.mean Y)) =
  ((p.mean fun ω => (X ω - p.mean X) ^ 2) + p.mean fun ω => (Y ω - p.mean Y) ^ 2) +
    2 * p.mean fun ω => (X ω - p.mean X) * (Y ω - p.mean Y)All goals completed! 🐙]All goals completed! 🐙

Independent draws use product probabilities. This is an explicit construction.

noncomputable def prod (p : FiniteLaw Ω) (q : FiniteLaw Ξ) : FiniteLaw (Ω × Ξ) where
  mass ω := p.mass ω.1 * q.mass ω.2
  nonneg ω := mul_nonneg (p.nonneg _) (q.nonneg _)
  total := byΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw Ξ⊢ ∑ ω, p.mass ω.1 * q.mass ω.2 = 1
    simp [Fintype.sum_prod_type, ← Finset.mul_sum, q.total, p.total]All goals completed! 🐙

@[simp] theorem mean_prod_left (p : FiniteLaw Ω) (q : FiniteLaw Ξ) (X : Ω → ℝ) :
    (p.prod q).mean (fun ω => X ω.1) = p.mean X := byΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝ⊢ ((p.prod q).mean fun ω => X ω.1) = p.mean X
  simp [mean, prod, Fintype.sum_prod_type, mul_right_comm,
    ← Finset.mul_sum, q.total]All goals completed! 🐙

@[simp] theorem mean_prod_right (p : FiniteLaw Ω) (q : FiniteLaw Ξ) (Y : Ξ → ℝ) :
    (p.prod q).mean (fun ω => Y ω.2) = q.mean Y := byΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞY:Ξ → ℝ⊢ ((p.prod q).mean fun ω => Y ω.2) = q.mean Y
  simp [mean, prod, Fintype.sum_prod_type, mul_assoc,
    ← Finset.mul_sum, ← Finset.sum_mul, p.total]All goals completed! 🐙



theorem mean_prod_mul (p : FiniteLaw Ω) (q : FiniteLaw Ξ)
    (X : Ω → ℝ) (Y : Ξ → ℝ) :
    (p.prod q).mean (fun ω => X ω.1 * Y ω.2) = p.mean X * q.mean Y := byΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝ⊢ ((p.prod q).mean fun ω => X ω.1 * Y ω.2) = p.mean X * q.mean Y
  simp only [mean, prod, Fintype.sum_prod_type, Finset.sum_mul, Finset.mul_sum]Ω:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝ⊢ ∑ x, ∑ x_1, p.mass x * q.mass x_1 * (X x * Y x_1) = ∑ x, ∑ i, p.mass i * X i * (q.mass x * Y x)
  rw [Finset.sum_commΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝ⊢ ∑ y, ∑ x, p.mass x * q.mass y * (X x * Y y) = ∑ x, ∑ i, p.mass i * X i * (q.mass x * Y x)Ω:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝ⊢ ∑ y, ∑ x, p.mass x * q.mass y * (X x * Y y) = ∑ x, ∑ i, p.mass i * X i * (q.mass x * Y x)]Ω:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝ⊢ ∑ y, ∑ x, p.mass x * q.mass y * (X x * Y y) = ∑ x, ∑ i, p.mass i * X i * (q.mass x * Y x)
  apply Finset.sum_congr rflΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝ⊢ ∀ x ∈ Finset.univ, ∑ x_1, p.mass x_1 * q.mass x * (X x_1 * Y x) = ∑ i, p.mass i * X i * (q.mass x * Y x)
  intro ω _Ω:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝω:Ξa✝:ω ∈ Finset.univ⊢ ∑ x, p.mass x * q.mass ω * (X x * Y ω) = ∑ i, p.mass i * X i * (q.mass ω * Y ω)
  apply Finset.sum_congr rflΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝω:Ξa✝:ω ∈ Finset.univ⊢ ∀ x ∈ Finset.univ, p.mass x * q.mass ω * (X x * Y ω) = p.mass x * X x * (q.mass ω * Y ω)
  intro ξ _Ω:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝω:Ξa✝¹:ω ∈ Finset.univξ:Ωa✝:ξ ∈ Finset.univ⊢ p.mass ξ * q.mass ω * (X ξ * Y ω) = p.mass ξ * X ξ * (q.mass ω * Y ω)
  ringAll goals completed! 🐙



theorem variance_independent_add (p : FiniteLaw Ω) (q : FiniteLaw Ξ)
    (X : Ω → ℝ) (Y : Ξ → ℝ) :
    (p.prod q).variance (fun ω => X ω.1 + Y ω.2) = p.variance X + q.variance Y := byΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝ⊢ ((p.prod q).variance fun ω => X ω.1 + Y ω.2) = p.variance X + q.variance Y
  rw [variance_eq_second_moment,Ω:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝ⊢ ((p.prod q).mean fun ω => (X ω.1 + Y ω.2) ^ 2) - ((p.prod q).mean fun ω => X ω.1 + Y ω.2) ^ 2 =
  p.variance X + q.variance YΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝ⊢ ((p.prod q).mean fun ω => (X ω.1 + Y ω.2) ^ 2) - (p.mean X + q.mean Y) ^ 2 = p.variance X + q.variance Y mean_add,Ω:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝ⊢ ((p.prod q).mean fun ω => (X ω.1 + Y ω.2) ^ 2) -
    (((p.prod q).mean fun ω => X ω.1) + (p.prod q).mean fun ω => Y ω.2) ^ 2 =
  p.variance X + q.variance YΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝ⊢ ((p.prod q).mean fun ω => (X ω.1 + Y ω.2) ^ 2) - (p.mean X + q.mean Y) ^ 2 = p.variance X + q.variance Y mean_prod_left,Ω:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝ⊢ ((p.prod q).mean fun ω => (X ω.1 + Y ω.2) ^ 2) - (p.mean X + (p.prod q).mean fun ω => Y ω.2) ^ 2 =
  p.variance X + q.variance YΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝ⊢ ((p.prod q).mean fun ω => (X ω.1 + Y ω.2) ^ 2) - (p.mean X + q.mean Y) ^ 2 = p.variance X + q.variance Y mean_prod_rightΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝ⊢ ((p.prod q).mean fun ω => (X ω.1 + Y ω.2) ^ 2) - (p.mean X + q.mean Y) ^ 2 = p.variance X + q.variance YΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝ⊢ ((p.prod q).mean fun ω => (X ω.1 + Y ω.2) ^ 2) - (p.mean X + q.mean Y) ^ 2 = p.variance X + q.variance Y]Ω:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝ⊢ ((p.prod q).mean fun ω => (X ω.1 + Y ω.2) ^ 2) - (p.mean X + q.mean Y) ^ 2 = p.variance X + q.variance Y
  have h : (fun ω : Ω × Ξ => (X ω.1 + Y ω.2) ^ 2) =
      (fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)) := byΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝ⊢ ((p.prod q).variance fun ω => X ω.1 + Y ω.2) = p.variance X + q.variance YΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝh:(fun ω => (X ω.1 + Y ω.2) ^ 2) = fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)⊢ ((p.prod q).mean fun ω => (X ω.1 + Y ω.2) ^ 2) - (p.mean X + q.mean Y) ^ 2 = p.variance X + q.variance Y
    funext ωΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝω:Ω × Ξ⊢ (X ω.1 + Y ω.2) ^ 2 = X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)Ω:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝh:(fun ω => (X ω.1 + Y ω.2) ^ 2) = fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)⊢ ((p.prod q).mean fun ω => (X ω.1 + Y ω.2) ^ 2) - (p.mean X + q.mean Y) ^ 2 = p.variance X + q.variance Y
    ringΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝh:(fun ω => (X ω.1 + Y ω.2) ^ 2) = fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)⊢ ((p.prod q).mean fun ω => (X ω.1 + Y ω.2) ^ 2) - (p.mean X + q.mean Y) ^ 2 = p.variance X + q.variance YΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝh:(fun ω => (X ω.1 + Y ω.2) ^ 2) = fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)⊢ ((p.prod q).mean fun ω => (X ω.1 + Y ω.2) ^ 2) - (p.mean X + q.mean Y) ^ 2 = p.variance X + q.variance Y
  rw [h,Ω:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝh:(fun ω => (X ω.1 + Y ω.2) ^ 2) = fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)⊢ ((p.prod q).mean fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)) - (p.mean X + q.mean Y) ^ 2 =
  p.variance X + q.variance YΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝh:(fun ω => (X ω.1 + Y ω.2) ^ 2) = fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)⊢ ((p.mean fun ω => X ω ^ 2) + q.mean fun ω => Y ω ^ 2) + 2 * (p.mean X * q.mean Y) - (p.mean X + q.mean Y) ^ 2 =
  (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2 + ((q.mean fun ω => Y ω ^ 2) - q.mean Y ^ 2) mean_add,Ω:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝh:(fun ω => (X ω.1 + Y ω.2) ^ 2) = fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)⊢ (((p.prod q).mean fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2) + (p.prod q).mean fun ω => 2 * (X ω.1 * Y ω.2)) -
    (p.mean X + q.mean Y) ^ 2 =
  p.variance X + q.variance YΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝh:(fun ω => (X ω.1 + Y ω.2) ^ 2) = fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)⊢ ((p.mean fun ω => X ω ^ 2) + q.mean fun ω => Y ω ^ 2) + 2 * (p.mean X * q.mean Y) - (p.mean X + q.mean Y) ^ 2 =
  (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2 + ((q.mean fun ω => Y ω ^ 2) - q.mean Y ^ 2) mean_add,Ω:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝh:(fun ω => (X ω.1 + Y ω.2) ^ 2) = fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)⊢ ((((p.prod q).mean fun ω => X ω.1 ^ 2) + (p.prod q).mean fun ω => Y ω.2 ^ 2) +
      (p.prod q).mean fun ω => 2 * (X ω.1 * Y ω.2)) -
    (p.mean X + q.mean Y) ^ 2 =
  p.variance X + q.variance YΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝh:(fun ω => (X ω.1 + Y ω.2) ^ 2) = fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)⊢ ((p.mean fun ω => X ω ^ 2) + q.mean fun ω => Y ω ^ 2) + 2 * (p.mean X * q.mean Y) - (p.mean X + q.mean Y) ^ 2 =
  (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2 + ((q.mean fun ω => Y ω ^ 2) - q.mean Y ^ 2) mean_scale,Ω:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝh:(fun ω => (X ω.1 + Y ω.2) ^ 2) = fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)⊢ ((((p.prod q).mean fun ω => X ω.1 ^ 2) + (p.prod q).mean fun ω => Y ω.2 ^ 2) +
      2 * (p.prod q).mean fun ω => X ω.1 * Y ω.2) -
    (p.mean X + q.mean Y) ^ 2 =
  p.variance X + q.variance YΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝh:(fun ω => (X ω.1 + Y ω.2) ^ 2) = fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)⊢ ((p.mean fun ω => X ω ^ 2) + q.mean fun ω => Y ω ^ 2) + 2 * (p.mean X * q.mean Y) - (p.mean X + q.mean Y) ^ 2 =
  (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2 + ((q.mean fun ω => Y ω ^ 2) - q.mean Y ^ 2) mean_prod_mul,Ω:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝh:(fun ω => (X ω.1 + Y ω.2) ^ 2) = fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)⊢ (((p.prod q).mean fun ω => X ω.1 ^ 2) + (p.prod q).mean fun ω => Y ω.2 ^ 2) + 2 * (p.mean X * q.mean Y) -
    (p.mean X + q.mean Y) ^ 2 =
  p.variance X + q.variance YΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝh:(fun ω => (X ω.1 + Y ω.2) ^ 2) = fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)⊢ ((p.mean fun ω => X ω ^ 2) + q.mean fun ω => Y ω ^ 2) + 2 * (p.mean X * q.mean Y) - (p.mean X + q.mean Y) ^ 2 =
  (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2 + ((q.mean fun ω => Y ω ^ 2) - q.mean Y ^ 2)
    mean_prod_left p q (fun ω => X ω ^ 2),Ω:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝh:(fun ω => (X ω.1 + Y ω.2) ^ 2) = fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)⊢ ((p.mean fun ω => X ω ^ 2) + (p.prod q).mean fun ω => Y ω.2 ^ 2) + 2 * (p.mean X * q.mean Y) -
    (p.mean X + q.mean Y) ^ 2 =
  p.variance X + q.variance YΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝh:(fun ω => (X ω.1 + Y ω.2) ^ 2) = fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)⊢ ((p.mean fun ω => X ω ^ 2) + q.mean fun ω => Y ω ^ 2) + 2 * (p.mean X * q.mean Y) - (p.mean X + q.mean Y) ^ 2 =
  (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2 + ((q.mean fun ω => Y ω ^ 2) - q.mean Y ^ 2) mean_prod_right p q (fun ω => Y ω ^ 2),Ω:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝh:(fun ω => (X ω.1 + Y ω.2) ^ 2) = fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)⊢ ((p.mean fun ω => X ω ^ 2) + q.mean fun ω => Y ω ^ 2) + 2 * (p.mean X * q.mean Y) - (p.mean X + q.mean Y) ^ 2 =
  p.variance X + q.variance YΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝh:(fun ω => (X ω.1 + Y ω.2) ^ 2) = fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)⊢ ((p.mean fun ω => X ω ^ 2) + q.mean fun ω => Y ω ^ 2) + 2 * (p.mean X * q.mean Y) - (p.mean X + q.mean Y) ^ 2 =
  (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2 + ((q.mean fun ω => Y ω ^ 2) - q.mean Y ^ 2)
    variance_eq_second_moment,Ω:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝh:(fun ω => (X ω.1 + Y ω.2) ^ 2) = fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)⊢ ((p.mean fun ω => X ω ^ 2) + q.mean fun ω => Y ω ^ 2) + 2 * (p.mean X * q.mean Y) - (p.mean X + q.mean Y) ^ 2 =
  (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2 + q.variance YΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝh:(fun ω => (X ω.1 + Y ω.2) ^ 2) = fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)⊢ ((p.mean fun ω => X ω ^ 2) + q.mean fun ω => Y ω ^ 2) + 2 * (p.mean X * q.mean Y) - (p.mean X + q.mean Y) ^ 2 =
  (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2 + ((q.mean fun ω => Y ω ^ 2) - q.mean Y ^ 2) variance_eq_second_momentΩ:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝh:(fun ω => (X ω.1 + Y ω.2) ^ 2) = fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)⊢ ((p.mean fun ω => X ω ^ 2) + q.mean fun ω => Y ω ^ 2) + 2 * (p.mean X * q.mean Y) - (p.mean X + q.mean Y) ^ 2 =
  (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2 + ((q.mean fun ω => Y ω ^ 2) - q.mean Y ^ 2)Ω:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝh:(fun ω => (X ω.1 + Y ω.2) ^ 2) = fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)⊢ ((p.mean fun ω => X ω ^ 2) + q.mean fun ω => Y ω ^ 2) + 2 * (p.mean X * q.mean Y) - (p.mean X + q.mean Y) ^ 2 =
  (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2 + ((q.mean fun ω => Y ω ^ 2) - q.mean Y ^ 2)]Ω:TypeΞ:Typeinst✝¹:Fintype Ωinst✝:Fintype Ξp:FiniteLaw Ωq:FiniteLaw ΞX:Ω → ℝY:Ξ → ℝh:(fun ω => (X ω.1 + Y ω.2) ^ 2) = fun ω => X ω.1 ^ 2 + Y ω.2 ^ 2 + 2 * (X ω.1 * Y ω.2)⊢ ((p.mean fun ω => X ω ^ 2) + q.mean fun ω => Y ω ^ 2) + 2 * (p.mean X * q.mean Y) - (p.mean X + q.mean Y) ^ 2 =
  (p.mean fun ω => X ω ^ 2) - p.mean X ^ 2 + ((q.mean fun ω => Y ω ^ 2) - q.mean Y ^ 2)
  ringAll goals completed! 🐙

Constant division scales variance by the squared divisor.


theorem variance_div (p : FiniteLaw Ω) (X : Ω → ℝ) (a : ℝ) :
    p.variance (fun ω => X ω / a) = p.variance X / a ^ 2 := byΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝ⊢ (p.variance fun ω => X ω / a) = p.variance X / a ^ 2
  have h : (fun ω => X ω / a) = (fun ω => a⁻¹ * X ω + 0) := by
    funext ωΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝω:Ω⊢ X ω / a = a⁻¹ * X ω + 0Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝh:(fun ω => X ω / a) = fun ω => a⁻¹ * X ω + 0⊢ (p.variance fun ω => X ω / a) = p.variance X / a ^ 2
    simp [div_eq_mul_inv, mul_comm]Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝh:(fun ω => X ω / a) = fun ω => a⁻¹ * X ω + 0⊢ (p.variance fun ω => X ω / a) = p.variance X / a ^ 2Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝh:(fun ω => X ω / a) = fun ω => a⁻¹ * X ω + 0⊢ (p.variance fun ω => X ω / a) = p.variance X / a ^ 2
  rw [h,Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝh:(fun ω => X ω / a) = fun ω => a⁻¹ * X ω + 0⊢ (p.variance fun ω => a⁻¹ * X ω + 0) = p.variance X / a ^ 2Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝh:(fun ω => X ω / a) = fun ω => a⁻¹ * X ω + 0⊢ a⁻¹ ^ 2 * p.variance X = p.variance X / a ^ 2 variance_affineΩ:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝh:(fun ω => X ω / a) = fun ω => a⁻¹ * X ω + 0⊢ a⁻¹ ^ 2 * p.variance X = p.variance X / a ^ 2Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝh:(fun ω => X ω / a) = fun ω => a⁻¹ * X ω + 0⊢ a⁻¹ ^ 2 * p.variance X = p.variance X / a ^ 2]Ω:Typeinst✝:Fintype Ωp:FiniteLaw ΩX:Ω → ℝa:ℝh:(fun ω => X ω / a) = fun ω => a⁻¹ * X ω + 0⊢ a⁻¹ ^ 2 * p.variance X = p.variance X / a ^ 2
  simp [div_eq_mul_inv, mul_comm]All goals completed! 🐙

end FiniteLawend JaxLean