OAI/GroupTheory/PolycyclicRecognition/Analysis/SequenceCellProfilePairs.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_good_cell_profile_pairs_sequence line 20

   Source documentation

   A supported pair of profile limits gives a common good set in each original recurrence cell, with both uniform errors tending to zero.

   theorem exists_good_cell_profile_pairs_sequence
       {V W N : Type*} [TopologicalSpace V] [NormedAddCommGroup W] [MeasurableSpace N]
       (S : Set C(V, W)) [MeasurableSpace S] [BorelSpace S]
       [BorelSpace (S × S)] [HasOuterApproxClosed (S × S)]
       (K : Set V) (hK : IsCompact K)
       (scale : ℕ → ℝ) (hs : Tendsto scale atTop atTop)
       (μ : Measure N) (Q : ℕ → Set N) (hQ : ∀ n, MeasurableSet (Q n))
       (hQ0 : ∀ n, μ (Q n) ≠ 0) (hQfin : ∀ n, μ (Q n) ≠ ∞)
       (profile : ℕ → N → S × S) (hp : ∀ n, Measurable (profile n))
       (ν : ProbabilityMeasure (S × S))
       (hν : Tendsto (fun n => ProbabilityMeasure.map
         (cellProbabilityMeasure μ (Q n) (hQ0 n) (hQfin n)) (profile n)) atTop (𝓝 ν))
   …

   Mentions: OAI.PolycyclicRecognition.cellProbabilityMeasure

2. theorem OAI.PolycyclicRecognition.exists_positive_good_cell_profile_pairs line 73

   Source documentation

   Retain only good scales once, before applying the coupled recurrence. Both the actual scales and their indices remain strictly increasing.

   theorem exists_positive_good_cell_profile_pairs
       {V W N : Type*} [TopologicalSpace V] [NormedAddCommGroup W] [MeasurableSpace N]
       (S : Set C(V, W)) [MeasurableSpace S] [BorelSpace S]
       [BorelSpace (S × S)] [HasOuterApproxClosed (S × S)]
       (K : Set V) (hK : IsCompact K)
       (scale : ℕ → ℝ) (hs : Tendsto scale atTop atTop)
       (μ : Measure N) (Q : ℕ → Set N) (hQ : ∀ n, MeasurableSet (Q n))
       (hQ0 : ∀ n, μ (Q n) ≠ 0) (hQfin : ∀ n, μ (Q n) ≠ ∞)
       (profile : ℕ → N → S × S) (hp : ∀ n, Measurable (profile n))
       (ν : ProbabilityMeasure (S × S))
       (hν : Tendsto (fun n => ProbabilityMeasure.map
         (cellProbabilityMeasure μ (Q n) (hQ0 n) (hQfin n)) (profile n)) atTop (𝓝 ν))
   …

   Mentions: OAI.PolycyclicRecognition.cellProbabilityMeasure

3. theorem OAI.PolycyclicRecognition.exists_positive_eventually_good_cell_profile_pairs line 108

   Source documentation

   Replace the finitely many zero-measure good cells by their whole cells. The scale sequence is preserved, which keeps both already chosen polynomial limits and the chart selected by the geometric comparison unchanged.

   theorem exists_positive_eventually_good_cell_profile_pairs
       {V W N : Type*} [TopologicalSpace V] [NormedAddCommGroup W] [MeasurableSpace N]
       (S : Set C(V, W)) [MeasurableSpace S] [BorelSpace S]
       [BorelSpace (S × S)] [HasOuterApproxClosed (S × S)]
       (K : Set V) (hK : IsCompact K)
       (scale : ℕ → ℝ) (hs : Tendsto scale atTop atTop)
       (μ : Measure N) (Q : ℕ → Set N) (hQ : ∀ n, MeasurableSet (Q n))
       (hQ0 : ∀ n, μ (Q n) ≠ 0) (hQfin : ∀ n, μ (Q n) ≠ ∞)
       (profile : ℕ → N → S × S) (hp : ∀ n, Measurable (profile n))
       (ν : ProbabilityMeasure (S × S))
       (hν : Tendsto (fun n => ProbabilityMeasure.map
         (cellProbabilityMeasure μ (Q n) (hQ0 n) (hQfin n)) (profile n)) atTop (𝓝 ν))
   …

   Mentions: OAI.PolycyclicRecognition.cellProbabilityMeasure