NormalizerKernelCovariance.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Covariance of the component kernel under a normalizer

The normalizer moves the component parameter as well as the component measure. The proof compares the two actual joint laws and uses uniqueness of disintegration. In particular, it does not replace covariance by the stronger assertion that every component is fixed.

theorem OAI.DukePrimeDegree.condExpKernel_equivariant line 21

theorem OAI.DukePrimeDegree.lattice_normalizer_component_covariance line 100

Source documentation

For the actual lattice action, a normalizer sends each conditional measure to the conditional measure at the moved parameter.

theorem lattice_normalizer_component_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) = μ) :
    ∀ᵐ x ∂μ.trim (actionInvariantSigma_le H (X n)),
      (condExpKernel μ (actionInvariantSigma H (X n)) x).map
        (fun y => rightAction y a) =
      condExpKernel μ (actionInvariantSigma H (X n)) (rightAction x a) := by
…