OAI/GroupTheory/PolycyclicRecognition/Analysis/ThreeProbeConcentration.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.bad_distance_triangle_tendsto_zero line 14

   Source documentation

   Concentration is transitive through the measured anchor profile.

   theorem bad_distance_triangle_tendsto_zero
       {X S : Type*} [MeasurableSpace X] [PseudoMetricSpace S]
       (μ : ℕ → Measure X) (f g h : ℕ → X → S)
       (hfg : ∀ ε : ℝ, 0 < ε →
         Tendsto (fun n => μ n {x | ε ≤ dist (f n x) (g n x)}) atTop (𝓝 0))
       (hgh : ∀ ε : ℝ, 0 < ε →
         Tendsto (fun n => μ n {x | ε ≤ dist (g n x) (h n x)}) atTop (𝓝 0))
       (ε : ℝ) (hε : 0 < ε) :
       Tendsto (fun n => μ n {x | ε ≤ dist (f n x) (h n x)}) atTop (𝓝 0) := by
   …

2. theorem OAI.PolycyclicRecognition.exists_supported_three_affine_probe_sequence line 41

   Source documentation

   The first chain is based at the original sheet, the second at its neighbor, and the third at the selected endpoint of the second. One compact set of probes and one original sample work for every prefix of all three.

   theorem exists_supported_three_affine_probe_sequence
       {X Z W V : Type*} [Nonempty X] [MeasurableSpace X]
       [TopologicalSpace Z] [CompactSpace Z]
       [NormedAddCommGroup W] [NormedSpace ℝ W]
       [AddCommGroup V] [Module ℝ V]
       [MeasurableSpace C(Z, W)] [BorelSpace C(Z, W)]
       [BorelSpace (C(Z, W) × C(Z, W))]
       [HasOuterApproxClosed (C(Z, W) × C(Z, W))]
       {Y : ℕ → Type*} [∀ n, TopologicalSpace (Y n)] [∀ n, CompactSpace (Y n)]
       [∀ n, T2Space (Y n)] [∀ n, MeasurableSpace (Y n)] [∀ n, BorelSpace (Y n)]
       [∀ n, Nonempty (Y n)]
       (μ : ProbabilityMeasure X) (ν : ∀ n, ProbabilityMeasure (Y n))
   …