RegularRootInvariance.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Root invariance from the finite regular entropy tests

The prime-degree application needs balance and one positive coefficient. The symmetry argument below uses only the explicit regular test weights, not an entropy formula at arbitrary or singular weights.

lemma OAI.DukePrimeDegree.canonical_atomless_of_pos line 26
lemma OAI.DukePrimeDegree.canonical_two_step line 35

theorem OAI.DukePrimeDegree.canonical_root_invariant_of_balance line 53

Source documentation

Actual root invariance follows from coefficient balance, using the proved commutator and isolated-root shearing alternatives.

theorem canonical_root_invariant_of_balance (hd : 2 < d+1)
    (hbalance : ∀ i, ∑ j, canonicalRootCoefficient d μ i j =
      ∑ j, canonicalRootCoefficient d μ j i)
    {i j : Fin (d+1)} (hij : i ≠ j)
    (hpos : 0 < canonicalRootCoefficient d μ i j) :
    ∀ t : ℝ, μ.map (fun x => rightAction x
      (Matrix.SpecialLinearGroup.transvection hij t)) = μ := by
…

Mentions: OAI.DukePrimeDegree.canonicalRootCoefficient

theorem OAI.DukePrimeDegree.canonical_root_invariant_of_regular_tests line 102

Source documentation

Only the finite family of regular entropy identities is needed to turn any positive actual coefficient into ambient root invariance.

theorem canonical_root_invariant_of_regular_tests (hd : 2 < d+1)
    (htests : ∀ a : Option (Fin (d+1)),
      measureEntropy μ (fun x => rightAction x
        (diagonalOneParameter (regularEntropyTest d a) (regularEntropyTest_sum d a) 1)) =
          ENNReal.ofReal (rootEntropyForm (canonicalRootCoefficient d μ) (regularEntropyTest d a)) ∧
      measureEntropy μ (fun x => rightAction x
        (diagonalOneParameter (regularEntropyTest d a) (regularEntropyTest_sum d a) (-1))) =
          ENNReal.ofReal (rootEntropyForm (canonicalRootCoefficient d μ)
            (fun i => -regularEntropyTest d a i)))
    {i j : Fin (d+1)} (hij : i ≠ j) (hpos : 0 < canonicalRootCoefficient d μ i j) :
    ∀ t : ℝ, μ.map (fun x => rightAction x
      (Matrix.SpecialLinearGroup.transvection hij t)) = μ := by
…

Mentions: OAI.DukePrimeDegree.regularEntropyTest, OAI.DukePrimeDegree.regularEntropyTest_sum, OAI.DukePrimeDegree.rootEntropyForm, OAI.DukePrimeDegree.canonicalRootCoefficient

theorem OAI.DukePrimeDegree.exists_invariant_root_of_regular_tests line 122

Source documentation

Positive entropy for the original regular diagonal map supplies an actual invariant root subgroup once the finite regular test identities have been identified. No formula at singular weights is used.

theorem exists_invariant_root_of_regular_tests (hd : 2 < d+1)
    (hpos : 0 < measureEntropy μ (fun x => rightAction x
      (diagonalOneParameter (regularDiagonalWeights d) (regularDiagonalWeights_sum d) 1)))
    (htests : ∀ a : Option (Fin (d+1)),
      measureEntropy μ (fun x => rightAction x
        (diagonalOneParameter (regularEntropyTest d a) (regularEntropyTest_sum d a) 1)) =
          ENNReal.ofReal (rootEntropyForm (canonicalRootCoefficient d μ) (regularEntropyTest d a)) ∧
      measureEntropy μ (fun x => rightAction x
        (diagonalOneParameter (regularEntropyTest d a) (regularEntropyTest_sum d a) (-1))) =
          ENNReal.ofReal (rootEntropyForm (canonicalRootCoefficient d μ)
            (fun i => -regularEntropyTest d a i))) :
    ∃ (i j : Fin (d+1)) (hij : i ≠ j), ∀ t : ℝ, μ.map (fun x => rightAction x
…

Mentions: OAI.DukePrimeDegree.regularEntropyTest, OAI.DukePrimeDegree.regularEntropyTest_sum, OAI.DukePrimeDegree.rootEntropyForm, OAI.DukePrimeDegree.canonicalRootCoefficient