OAI/GroupTheory/PolycyclicRecognition/Analysis/RescaledAffineComparison.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.bad_probability_tendsto_zero_of_dist_le line 20
2. theorem OAI.PolycyclicRecognition.deterministic_distance_tendsto_zero_of_rescaled_profiles line 39

   Source documentation

   A mixed sampling comparison transports deterministic approximants through any uniformly Lipschitz exact change of coordinates.

   theorem deterministic_distance_tendsto_zero_of_rescaled_profiles
       {X Y : Type*} [MeasurableSpace X] [PseudoMetricSpace Y]
       (μ ν : ℕ → ProbabilityMeasure X) (a b : ℕ → Y)
       (f g : ℕ → X → Y) (H : ℕ → Y → Y) {K : ℝ} (hK : 0 < K)
       (hH : ∀ n u v, dist (H n u) (H n v) ≤ K * dist u v)
       (hmatch : ∀ n x, f n x = H n (g n x))
       (hleft : ∀ ε : ℝ, 0 < ε → Tendsto (fun n =>
         (μ n : Measure X) {x | ε ≤ dist (a n) (f n x)}) atTop (𝓝 0))
       (hpair : ∀ ε : ℝ, 0 < ε → Tendsto (fun n =>
         (μ n : Measure X).prod (ν n : Measure X)
           {p | ε ≤ dist (f n p.1) (f n p.2)}) atTop (𝓝 0))
       (hright : ∀ ε : ℝ, 0 < ε → Tendsto (fun n =>
   …

3. def OAI.PolycyclicRecognition.rescaleCompactProfile line 76

   Source documentation

   The operator on compact profiles induced by a change of chart.

   def rescaleCompactProfile {Z W : Type*} [TopologicalSpace Z] [CompactSpace Z]
       [NormedAddCommGroup W] [NormedSpace ℝ W]
       (t : ℝ) (φ : C(Z, Z)) (f : C(Z, W)) : C(Z, W) := t • f.comp φ

4. theorem OAI.PolycyclicRecognition.dist_rescaleCompactProfile_le line 80
5. theorem OAI.PolycyclicRecognition.rescaleCompactProfile_affine line 93

   Source documentation

   A linear profile transforms exactly; only its constant offset changes.

   theorem rescaleCompactProfile_affine
       {Z W : Type*} [TopologicalSpace Z] [CompactSpace Z]
       [NormedAddCommGroup W] [NormedSpace ℝ W]
       (t : ℝ) (φ : C(Z, Z)) (A : C(Z, W)) (b : W)
       (hA : ∀ z, t • A (φ z) = A z) :
       rescaleCompactProfile t φ (A + ContinuousMap.const Z b) =
         A + ContinuousMap.const Z (t • b) := by
   …

   Mentions: OAI.PolycyclicRecognition.rescaleCompactProfile

6. theorem OAI.PolycyclicRecognition.affine_labels_and_offsets_of_distance_tendsto_zero line 105

   Source documentation

   Vanishing affine discrepancy identifies finite labels and their offsets.

   theorem affine_labels_and_offsets_of_distance_tendsto_zero
       {Z W L : Type*} [TopologicalSpace Z] [CompactSpace Z]
       [NormedAddCommGroup W] [Fintype L] [Nonempty L]
       (A : L → C(Z, W)) (hA : Function.Injective A)
       (z₀ : Z) (hzero : ∀ a, A a z₀ = 0)
       (a a' : ℕ → L) (b b' : ℕ → W)
       (hd : Tendsto (fun n => dist (A (a n) + ContinuousMap.const Z (b n))
         (A (a' n) + ContinuousMap.const Z (b' n))) atTop (𝓝 0)) :
       (∀ᶠ n in atTop, a n = a' n) ∧
         Tendsto (fun n => dist (b n) (b' n)) atTop (𝓝 0) := by
   …