MeasureStabilizerCovariance.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Actual stabilizers of transported component measures

Right translation conjugates the measure stabilizer in the opposite direction. Combining this identity with component-kernel covariance gives the exact covariance of their spaces of matrix velocities.

lemma OAI.DukePrimeDegree.matrixVelocitySpace_map_rightAction line 20

lemma OAI.DukePrimeDegree.matrixVelocitySpace_map_rightAction_iff line 38

Source documentation

The tangent transport is an equivalence, not just an inclusion. This is the exact relation needed for a change of frame.

lemma matrixVelocitySpace_map_rightAction_iff {n : ℕ}
    (μ : Measure (X n)) (a : G n)
    (V : Matrix (Fin n) (Fin n) ℝ) :
    a⁻¹.val * V * a.val ∈
        matrixVelocitySpace (invariantRightSubgroup
          (μ.map (fun x => rightAction x a))) ↔
      V ∈ matrixVelocitySpace (invariantRightSubgroup μ) := by
…

Mentions: OAI.DukePrimeDegree.matrixVelocitySpace

theorem OAI.DukePrimeDegree.ae_component_velocity_covariance line 64

Source documentation

Normalizer covariance of the genuine conditional measures gives covariance of their genuine curve-velocity subspaces.

theorem ae_component_velocity_covariance {n : ℕ}
    (H : Subgroup (G n)) (a : G n)
    (ha : a ∈ Subgroup.normalizer (H : Set (G n)))
    (μ : Measure (X n)) [IsProbabilityMeasure μ]
    (hμ : μ.map (fun x => rightAction x a) = μ) :
    ∀ᵐ z ∂μ.trim (actionInvariantSigma_le H (X n)),
      ∀ V ∈ matrixVelocitySpace
        (invariantRightSubgroup (condExpKernel μ (actionInvariantSigma H (X n)) z)),
      a⁻¹.val * V * a.val ∈ matrixVelocitySpace
        (invariantRightSubgroup (condExpKernel μ (actionInvariantSigma H (X n))
          (rightAction z a))) := by
…

Mentions: OAI.DukePrimeDegree.matrixVelocitySpace

theorem OAI.DukePrimeDegree.ae_component_velocity_covariance_iff line 80