BlockIncidentComponents.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Incident invariant roots preserve canonical block components

Mautner fixes every block-invariant L² indicator along an incident ambient invariant root. Almost invariance of the conditioning sigma algebra then implies invariance of the same canonical component kernel. No normalizer assertion and no reverse-root invariance is inserted.

lemma OAI.DukePrimeDegree.ae_incident_root_fixes_block_invariant_set line 23

theorem OAI.DukePrimeDegree.ae_block_component_incident_root_invariant line 68

Source documentation

The same full-subgroup conditional measures used by the geometric endpoint inherit all real parameters of the incident invariant root.

theorem ae_block_component_incident_root_invariant {n : ℕ}
    (S : Set (Fin n)) (k l : Fin n) (hkl : k ≠ l) (hk : k ∈ S) (hl : l ∈ S)
    (μ : Measure (X n)) [IsProbabilityMeasure μ]
    (hSL : singleBlockRootGroup S ≤ invariantRightSubgroup μ)
    (p q : Fin n) (hpq : p ≠ q) (htouch : p ∈ S ∨ q ∈ S)
    (hU : ∀ t : ℝ, μ.map (fun x => rightAction x
      (SpecialLinearGroup.transvection hpq t)) = μ) :
    ∀ᵐ z ∂μ.trim (actionInvariantSigma_le (singleBlockRootGroup S) (X n)),
      ∀ t : ℝ, (condExpKernel μ (actionInvariantSigma (singleBlockRootGroup S) (X n)) z).map
        (fun x => rightAction x (SpecialLinearGroup.transvection hpq t)) =
        condExpKernel μ (actionInvariantSigma (singleBlockRootGroup S) (X n)) z := by
…

Mentions: OAI.DukePrimeDegree.singleBlockRootGroup