OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanReverseNeighborLaw.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.reversed_neighbor_cell_limit line 27

   Source documentation

   Reversing the deterministic root step replaces the joint law by its coordinate swap, using exactly the Haar cell based at base * step.

   theorem reversed_neighbor_cell_limit
       [IsTopologicalGroup F.N.carrier]
       (haarN : NilpotentExponentialHaarInput F.N.modelSpace F.N.carrier)
       (chartN : GroupLieAlgebra (𝓘(ℝ, F.N.modelSpace)) F.N.carrier ≃ₜ F.N.carrier)
       (hchartN : ∀ x, chartN x = F.ExpN x)
       (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (E : Set W) (β : M.Bases) (scale : ℕ → ℝ) (base step : ℕ → F.N.carrier)
       {S : Type*} [TopologicalSpace S] [MeasurableSpace S] [BorelSpace S] [BorelSpace (S × S)]
       (profile : ℕ → F.N.carrier → S) (hp : ∀ n, Measurable (profile n))
       (ν : ProbabilityMeasure (S × S))
       (hν : Tendsto (fun n => ProbabilityMeasure.map
         (M.translatedGroupBoxProbability T F hunimod eW haarN chartN hchartN b₀ E β (scale n) (base n))
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.cartanRootIdeal

2. theorem OAI.PolycyclicRecognition.CartanWordModel.swapped_pair_mem_support line 60

   Source documentation

   Swapped supported profiles remain supported in the reversed law.

   theorem swapped_pair_mem_support
       {S : Type*} [TopologicalSpace S] [MeasurableSpace S] [BorelSpace S] [BorelSpace (S × S)]
       (ν : ProbabilityMeasure (S × S)) {f : S × S} (hf : f ∈ (ν : Measure (S × S)).support) :
       f.swap ∈ (ProbabilityMeasure.map ν Prod.swap : Measure (S × S)).support :=
   …

3. theorem OAI.PolycyclicRecognition.CartanWordModel.inverse_root_step line 68

   Source documentation

   The inverse of an actual root step has the same generator and negated parameter; the allowed amplitude is unchanged.

   theorem inverse_root_step (hExp : IsGroupExponential Exp)
       (i : Fin M.letterCount) (step : F.N.carrier) (time : ℝ)
       (hstep : F.inclusionN step = Exp (time • (M.letter i : GroupLieAlgebra (𝓘(ℝ, EG)) G))) :
       F.inclusionN step⁻¹ = Exp ((-time) • (M.letter i : GroupLieAlgebra (𝓘(ℝ, EG)) G)) := by
   …

4. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_reverse_neighbor_radius line 77

   Source documentation

   The new base and the inverse step lie in the same enlarged box with one common subexponential radius. This supplies the original box hypotheses when the offset volume comparison is applied in reverse.

   theorem exists_reverse_neighbor_radius
       (dynkinN : NilpotentDynkinExpansionInput F.N.modelSpace F.N.carrier)
       (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (E : Set W) (β : M.Bases)
       (hβ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
         (M.boxCost T hunimod eW E) β.val)
       (scale R : ℕ → ℝ) (hs : Tendsto scale atTop atTop) (hs0 : ∀ n, 0 ≤ scale n)
       (hR0 : ∀ n, 0 ≤ R n) (hR : HasSubexponentialUpperBoundSeq scale R)
       (base step : ℕ → F.N.carrier)
       (hbase : ∀ n, base n ∈ M.groupBox T hunimod eW (F.ExpN ∘ F.N.equiv) E β (scale n) (R n))
       (hstep : ∀ n, step n ∈ M.groupBox T hunimod eW (F.ExpN ∘ F.N.equiv) E β (scale n) (R n)) :
       ∃ R' : ℕ → ℝ, (∀ n, R n ≤ R' n) ∧ (∀ n, 0 ≤ R' n) ∧
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.HasSubexponentialUpperBoundSeq

5. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_reversed_neighbor_data line 127

   Source documentation

   Reversal preserves every original input needed by the opposite volume test, after enlarging only the subexponential radius. The limiting law is the coordinate swap of the original law, with the original supported pair swapped as well.

   theorem exists_reversed_neighbor_data
       [IsTopologicalGroup F.N.carrier]
       (hExp : IsGroupExponential Exp)
       (haarN : NilpotentExponentialHaarInput F.N.modelSpace F.N.carrier)
       (dynkinN : NilpotentDynkinExpansionInput F.N.modelSpace F.N.carrier)
       (chartN : GroupLieAlgebra (𝓘(ℝ, F.N.modelSpace)) F.N.carrier ≃ₜ F.N.carrier)
       (hchartN : ∀ x, chartN x = F.ExpN x)
       (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (E : Set W) (β : M.Bases)
       (hβ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
         (M.boxCost T hunimod eW E) β.val)
       (scale R : ℕ → ℝ) (hs : Tendsto scale atTop atTop) (hs0 : ∀ n, 0 ≤ scale n)
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates