OAI/GroupTheory/PolycyclicRecognition/Analysis/ExactProfileTransport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.deterministic_distance_tendsto_zero_of_exact_transport line 15

   Source documentation

   Two deterministic approximants can be compared under a single law when their sampled profiles are related by an exact Lipschitz transport.

   theorem deterministic_distance_tendsto_zero_of_exact_transport
       {X Y Z : Type*} [MeasurableSpace X] [PseudoMetricSpace Y] [PseudoMetricSpace Z]
       (μ : ℕ → ProbabilityMeasure X) (a : ℕ → Y) (b : ℕ → Z)
       (f : ℕ → X → Y) (g : ℕ → X → Z) (H : ℕ → Z → 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))
       (hright : ∀ ε : ℝ, 0 < ε → Tendsto (fun n =>
         (μ n : Measure X) {x | ε ≤ dist (g n x) (b n)}) atTop (𝓝 0)) :
       Tendsto (fun n => dist (a n) (H n (b n))) atTop (𝓝 0) := by
   …

2. def OAI.PolycyclicRecognition.transportCompactProfile line 40

   Source documentation

   Restriction to a changed compact chart, scalar normalization and the constant change of center.

   def transportCompactProfile
       {Z Z' W : Type*} [TopologicalSpace Z] [TopologicalSpace Z']
       [CompactSpace Z] [CompactSpace Z'] [NormedAddCommGroup W] [NormedSpace ℝ W]
       (t : ℝ) (ψ : C(Z, Z')) (c : W) (f : C(Z', W)) : C(Z, W) :=
   …

3. theorem OAI.PolycyclicRecognition.dist_transportCompactProfile_le line 46
4. theorem OAI.PolycyclicRecognition.transportCompactProfile_affine line 60

   Source documentation

   The exact height identity makes the chart transport of an affine profile affine again, with its center offset explicitly identified.

   theorem transportCompactProfile_affine
       {Z Z' V W : Type*} [TopologicalSpace Z] [TopologicalSpace Z']
       [CompactSpace Z] [CompactSpace Z']
       [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W]
       (t : ℝ) (ψ : C(Z, Z')) (q : C(Z, V)) (q' : C(Z', V))
       (A : V →L[ℝ] W) (b c : W) (v : V)
       (hheight : ∀ z, t • q' (ψ z) = q z - v) :
       transportCompactProfile t ψ c ((⟨fun z => A (q' z), A.continuous.comp q'.continuous⟩ : C(Z', W)) + ContinuousMap.const Z' b) =
         (⟨fun z => A (q z), A.continuous.comp q.continuous⟩ : C(Z, W)) + ContinuousMap.const Z (t • b + c - A v) := by
   …

   Mentions: OAI.PolycyclicRecognition.transportCompactProfile