Cochran's theorem

TheoremRank criterion#✓fully proved

Rank criterion (Cochran 1934): square matrices A k over a field that sum to the identity have ranks adding up to the size iff they are idempotent and pairwise annihilating.

theorem cochran_rank_criterion {R : Type*} [Field R] {n : Type*} [Fintype n] [DecidableEq n]
    {κ : Type*} [Fintype κ] (A : κ → Matrix n n R) (hsum : ∑ k, A k = 1) :
    ∑ k, (A k).rank = Fintype.card n ↔
      (∀ k, A k * A k = A k) ∧ Pairwise fun k l => A k * A l = 0

Used by 1

Used byCochran's theorem

TheoremIndependence of orthogonal projections of a standard Gaussian#✓fully proved

Under the standard Gaussian law, orthogonal projections onto pairwise orthogonal subspaces are mutually independent.

theorem iIndepFun_starProjection_stdGaussian {κ : Type*} [Finite κ] (K : κ → Submodule ℝ E)
    (hK : Pairwise fun k l => K k ⟂ K l) :
    iIndepFun (fun k x => (K k).starProjection x) (stdGaussian E)

Used by 1

Used byIndependence of squared lengths of orthogonal Gaussian projections

TheoremIndependence of squared lengths of orthogonal Gaussian projections#✓fully proved

Under the standard Gaussian law, the squared lengths ‖P_{K k} Z‖² of the projections onto pairwise orthogonal subspaces are mutually independent.

theorem iIndepFun_norm_sq_starProjection_stdGaussian {κ : Type*} [Finite κ]
    (K : κ → Submodule ℝ E) (hK : Pairwise fun k l => K k ⟂ K l) :
    iIndepFun (fun k x => ‖(K k).starProjection x‖ ^ 2) (stdGaussian E)

Uses 1

Proof usesIndependence of orthogonal projections of a standard Gaussian

DefinitionGroup mean of observations#✓fully proved

The mean of the observations x i with grp i = g (0 for an empty group).

noncomputable def groupMean {ι G : Type*} [Fintype ι] [DecidableEq G] (grp : ι → G)
    (x : ι → ℝ) (g : G) : ℝ :=
  (∑ i with grp i = g, x i) / (#{i | grp i = g} : ℕ)

Used by 4

Used byLaw of the Gaussian sample mean · Gaussian one-way layout · Independence of the Gaussian sample mean and residuals · One-way analysis of variance

TheoremGaussian one-way layout#✓fully proved

For i.i.d. N(μ, v) observations xᵢ labelled by groups grp i, the vector of group means is independent of the vector of within-group residuals xᵢ - x̄_{grp i}.

theorem indepFun_groupMean_residual {G : Type*} [Finite G] [DecidableEq G] (grp : ι → G)
    (μ : ℝ) (v : NNReal) :
    IndepFun (fun x g => groupMean grp x g) (fun x i => x i - groupMean grp x (grp i))
      (Measure.pi fun _ : ι => gaussianReal μ v)

Uses 1 · Used by 2

Statement usesGroup mean of observations

Used byIndependence of the Gaussian sample mean and residuals · One-way analysis of variance

TheoremOne-way analysis of variance#✓fully proved

For i.i.d. N(μ, v) observations labelled by groups, the between-group sum of squares ∑ᵢ (x̄_{grp i} - x̄)² is independent of the within-group sum of squares ∑ᵢ (xᵢ - x̄_{grp i})².

theorem indepFun_sumSqBetween_sumSqWithin {G : Type*} [Finite G] [DecidableEq G]
    (grp : ι → G) (μ : ℝ) (v : NNReal) :
    IndepFun (fun x => ∑ i, (groupMean grp x (grp i) - (∑ j, x j) / Fintype.card ι) ^ 2)
      (fun x => ∑ i, (x i - groupMean grp x (grp i)) ^ 2)
      (Measure.pi fun _ : ι => gaussianReal μ v)

Uses 2

Statement usesGroup mean of observations

Proof usesGaussian one-way layout

TheoremLaw of the Gaussian sample mean#✓fully proved

For an i.i.d. sample X₁, …, Xₙ ~ N(μ, v) with n ≥ 1, the sample mean has the law N(μ, v / n).

theorem hasLaw_sampleMean {n : ℕ} (hn : 0 < n) (μ : ℝ) (v : NNReal) :
    HasLaw (fun x : Fin n → ℝ => (∑ i, x i) / n) (gaussianReal μ (v / n))
      (Measure.pi fun _ : Fin n => gaussianReal μ v)

Uses 1

Proof usesGroup mean of observations

TheoremCochran's theorem#✓fully proved

Cochran's theorem, independence part: if Z has independent standard normal coordinates and symmetric matrices A k sum to the identity with ranks adding up to the dimension, the quadratic forms Zᵀ (A k) Z are mutually independent.

theorem iIndepFun_dotProduct_mulVec_pi_gaussianReal {ι : Type*} [Fintype ι] [DecidableEq ι]
    {κ : Type*} [Fintype κ] (A : κ → Matrix ι ι ℝ) (hA : ∀ k, (A k).IsHermitian)
    (hsum : ∑ k, A k = 1) (hrank : ∑ k, (A k).rank = Fintype.card ι) :
    iIndepFun (fun k (x : ι → ℝ) => x ⬝ᵥ A k *ᵥ x)
      (Measure.pi fun _ : ι => gaussianReal 0 1)

Uses 1

Proof usesRank criterion

TheoremIndependence of the Gaussian sample mean and residuals#✓fully proved

For an i.i.d. sample X₁, …, Xₙ ~ N(μ, v), the sample mean is independent of the residual vector (Xᵢ - X̄)ᵢ.

theorem indepFun_sampleMean_residual {n : ℕ} (μ : ℝ) (v : NNReal) :
    IndepFun (fun x : Fin n → ℝ => (∑ i, x i) / n)
      (fun x : Fin n → ℝ => fun i => x i - (∑ j, x j) / n)
      (Measure.pi fun _ : Fin n => gaussianReal μ v)

Uses 2 · Used by 1

Proof usesGroup mean of observations · Gaussian one-way layout

Used byIndependence of the Gaussian sample mean and sum of squared deviations

TheoremIndependence of the Gaussian sample mean and sum of squared deviations#✓fully proved

For an i.i.d. sample X₁, …, Xₙ ~ N(μ, v), the sample mean X̄ is independent of the sum of squared deviations ∑ (Xᵢ - X̄)² = (n - 1) S².

theorem indepFun_sampleMean_sumSqDev {n : ℕ} (μ : ℝ) (v : NNReal) :
    IndepFun (fun x : Fin n → ℝ => (∑ i, x i) / n)
      (fun x : Fin n → ℝ => ∑ i, (x i - (∑ j, x j) / n) ^ 2)
      (Measure.pi fun _ : Fin n => gaussianReal μ v)

Uses 1

Proof usesIndependence of the Gaussian sample mean and residuals

TheoremSum of squares of independent standard normals is chi-square#✓fully proved

For independent standard normal coordinates, the sum of the squares of the coordinates in a nonempty finite set s has the chi-square law with |s| degrees of freedom.

theorem pi_gaussianReal_map_sum_sq {ι : Type*} [Fintype ι] {s : Finset ι} (hs : s.Nonempty) :
    (Measure.pi fun _ : ι => gaussianReal 0 1).map (fun x => ∑ i ∈ s, x i ^ 2) =
      chiSquareMeasure s.card

Uses 5 · Used by 1

Statement usesChi-square distribution

Proof usesMoment generating function determines the gamma law · Exponential moments of the gamma law are finite exactly below the rate · Moment generating function of the chi-square distribution · Moment generating function of the square of a standard normal

Used bySquared orthonormal coordinates of a standard Gaussian are chi-square

TheoremSquared orthonormal coordinates of a standard Gaussian are chi-square#✓fully proved

Coordinates of the standard Gaussian law in an orthonormal basis b: the sum of the squared coordinates ⟪b i, x⟫ over a nonempty set s of indices is chi-square with |s| degrees of freedom.

theorem stdGaussian_map_sum_sq_inner {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {ι : Type*} [Fintype ι] (b : OrthonormalBasis ι ℝ E) {s : Finset ι} (hs : s.Nonempty) :
    (stdGaussian E).map (fun x => ∑ i ∈ s, ⟪b i, x⟫ ^ 2) = chiSquareMeasure s.card

Uses 2 · Used by 1

Statement usesChi-square distribution

Proof usesSum of squares of independent standard normals is chi-square

Used byCochran's theorem

TheoremCochran's theorem#✓fully proved

Cochran's theorem, projection form: for the standard Gaussian law on a finite-dimensional real inner product space E and a subspace K of positive dimension, the squared norm of the orthogonal projection onto K is chi-square with dim K degrees of freedom.

theorem stdGaussian_map_norm_sq_starProjection {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (K : Submodule ℝ E) (hK : 0 < finrank ℝ K) :
    (stdGaussian E).map (fun x => ‖K.starProjection x‖ ^ 2) = chiSquareMeasure (finrank ℝ K)

Uses 2 · Used by 2

Statement usesChi-square distribution

Proof usesSquared orthonormal coordinates of a standard Gaussian are chi-square

Used byCochran (1954) · Cochran's theorem

TheoremCochran's theorem#✓fully proved

Cochran's theorem, matrix form: if Z has independent standard normal coordinates and A is a symmetric idempotent matrix of positive rank, the quadratic form Zᵀ A Z is chi-square with rank A degrees of freedom.

theorem pi_gaussianReal_map_dotProduct_mulVec {ι : Type*} [Fintype ι]
    {A : Matrix ι ι ℝ} (hA : A.IsHermitian) (hAA : A * A = A) (hr : 0 < A.rank) :
    (Measure.pi fun _ : ι => gaussianReal 0 1).map (fun x => x ⬝ᵥ A *ᵥ x) =
      chiSquareMeasure A.rank

Uses 2

Statement usesChi-square distribution

Proof usesCochran's theorem

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.