OAI/GroupTheory/PolycyclicRecognition/Geometry/NormalizedPairHeightTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.uniform_affine_height_of_bounded_pair_representatives line 22

   Source documentation

   Bounded perturbations of both evaluation points cost at most twice the height-Lipschitz constant times the perturbation radius. No continuity of the original coarse maps is used.

   theorem uniform_affine_height_of_bounded_pair_representatives
       (D : SupportDatum W I B₀) (π : G →* Multiplicative W)
       {L : ℝ} (hL : 0 ≤ L)
       (hπ : ∀ x y, ‖(π x).toAdd - (π y).toAdd‖ ≤ L * dist x y)
       {Λ : ℝ≥0} (label : NormalizedPair G Λ → templateSymmetryGroup D)
       {K : ℝ} (hK : 0 ≤ K)
       (hbound : ∀ p x, ‖(π (p.val.1 x)).toAdd - (label p).val (π x).toAdd‖ ≤ K)
       (f : P → G → G) (rep : P → C(G, G) × C(G, G))
       (hrep : ∀ p, LipschitzPairBounds G Λ (rep p))
       {E : ℝ} (hE : 0 ≤ E) (hclose : ∀ p x, dist ((rep p).1 x) (f p x) ≤ E) :
       ∃ (A : P → templateSymmetryGroup D) (B : ℝ), 0 ≤ B ∧ ∀ p x,
         ‖(π (f p x)).toAdd - ((π (f p 1)).toAdd + (A p).val (π x).toAdd)‖ ≤ B := by
   …

   Mentions: OAI.PolycyclicRecognition.SupportDatum, OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.templateSymmetryGroup, OAI.PolycyclicRecognition.LipschitzPairBounds