BlockIncidentMautner.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A block-fixed observable is fixed along incident invariant roots

A root touching a nontrivial special linear block has nonzero weight for some diagonal inside that block. Mautner therefore fixes that root on every block-fixed vector, provided the root already acts isometrically. The lattice corollary uses only roots in the actual measure stabilizer. It does not infer invariance under a missing reverse root.

lemma OAI.DukePrimeDegree.another_mem_block line 23
lemma OAI.DukePrimeDegree.block_diagonal_fixed line 30

theorem OAI.DukePrimeDegree.incident_root_fixed_of_block_fixed line 51

Source documentation

This includes a root with only one endpoint in the fixed block. Its presence in the ambient isometric action remains essential.

theorem incident_root_fixed_of_block_fixed {n : ℕ} (S : Set (Fin n))
    (k l : Fin n) (hkl : k ≠ l) (hk : k ∈ S) (hl : l ∈ S)
    (L : Subgroup (G n)) (hSL : singleBlockRootGroup S ≤ L)
    {Y : Type*} [MetricSpace Y] [MulAction L Y] [ContinuousSMul L Y]
    [IsIsometricSMul L Y] (x : Y)
    (hfix : ∀ h : singleBlockRootGroup S,
      (⟨h.val, hSL h.property⟩ : L) • x = x)
    (p q : Fin n) (hpq : p ≠ q) (htouch : p ∈ S ∨ q ∈ S)
    (hU : ∀ t : ℝ, SpecialLinearGroup.transvection hpq t ∈ L) (t : ℝ) :
    (⟨SpecialLinearGroup.transvection hpq t, hU t⟩ : L) • x = x := by
…

Mentions: OAI.DukePrimeDegree.singleBlockRootGroup

theorem OAI.DukePrimeDegree.ae_incident_root_fixed_of_L2_block_fixed line 82

Source documentation

On the actual finite lattice-space measure, an incident root which already preserves the measure fixes every block-invariant L² observable. This is the input for transporting such invariance to block components.

theorem ae_incident_root_fixed_of_L2_block_fixed {n : ℕ}
    (S : Set (Fin n)) (k l : Fin n) (hkl : k ≠ l) (hk : k ∈ S) (hl : l ∈ S)
    (μ : Measure (X n)) [IsFiniteMeasure μ]
    (hSL : singleBlockRootGroup S ≤ invariantRightSubgroup μ)
    (f : Lp ℝ 2 μ)
    (hfix : ∀ h : singleBlockRootGroup S,
      (fun x => f (rightAction x h.val)) =ᵐ[μ] f)
    (p q : Fin n) (hpq : p ≠ q) (htouch : p ∈ S ∨ q ∈ S)
    (hU : ∀ t : ℝ, μ.map (fun x => rightAction x
      (SpecialLinearGroup.transvection hpq t)) = μ) (t : ℝ) :
    (fun x => f (rightAction x (SpecialLinearGroup.transvection hpq t))) =ᵐ[μ] f := by
…

Mentions: OAI.DukePrimeDegree.singleBlockRootGroup