OAI/GroupTheory/PolycyclicRecognition/Analysis/UniformProfileConcentration.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.eventually_uniform_lt_of_all_selections line 17

   Source documentation

   If every deterministic choice has vanishing bad probability, the bound is uniform over all permitted choices at each scale.

   theorem eventually_uniform_lt_of_all_selections
       {A : ℕ → Type*} [∀ n, Nonempty (A n)] (p : ∀ n, A n → ℝ≥0∞)
       (hp : ∀ a : ∀ n, A n, Tendsto (fun n => p n (a n)) atTop (𝓝 0))
       {η : ℝ≥0∞} (hη : 0 < η) :
       ∀ᶠ n in atTop, ∀ a, p n a < η := by
   …

2. theorem OAI.PolycyclicRecognition.product_bad_probability_le line 36

   Source documentation

   Averaging an independent suffix preserves a bound that holds for each of its deterministic values. The suffix law may vary arbitrarily.

   theorem product_bad_probability_le
       {A K : Type*} [MeasurableSpace A] [MeasurableSpace K]
       (μ : ProbabilityMeasure A) (ν : ProbabilityMeasure K)
       (B : Set (A × K)) (hB : MeasurableSet B) (δ : ℝ≥0∞)
       (hδ : ∀ k, (μ : Measure A) ((fun a => (a, k)) ⁻¹' B) ≤ δ) :
       (μ : Measure A).prod (ν : Measure K) B ≤ δ := by
   …

3. theorem OAI.PolycyclicRecognition.independent_bad_probability_tendsto_zero line 50

   Source documentation

   The uniform deterministic concentration conclusion survives arbitrary independent suffix distributions at each scale.

   theorem independent_bad_probability_tendsto_zero
       {A K : ℕ → Type*} [∀ n, MeasurableSpace (A n)] [∀ n, MeasurableSpace (K n)]
       [∀ n, Nonempty (K n)]
       (μ : ∀ n, ProbabilityMeasure (A n)) (ν : ∀ n, ProbabilityMeasure (K n))
       (B : ∀ n, Set (A n × K n)) (hB : ∀ n, MeasurableSet (B n))
       (hp : ∀ k : ∀ n, K n,
         Tendsto (fun n => (μ n : Measure (A n)) ((fun a => (a, k n)) ⁻¹' B n))
           atTop (𝓝 0)) :
       Tendsto (fun n => (μ n : Measure (A n)).prod (ν n : Measure (K n)) (B n))
         atTop (𝓝 0) := by
   …

4. theorem OAI.PolycyclicRecognition.exists_probe_fiber_in_event line 74

   Source documentation

   A joint failure probability smaller than the selected event's mass forces a starting sample inside that event with a good probe fiber.

   theorem exists_probe_fiber_in_event
       {A K : Type*} [MeasurableSpace A] [MeasurableSpace K]
       (μ : ProbabilityMeasure A) (ν : ProbabilityMeasure K)
       (E : Set A) (hE : MeasurableSet E) (B : Set (A × K)) (hB : MeasurableSet B)
       (η : ℝ≥0∞) (hsmall : (μ : Measure A).prod (ν : Measure K) B < η * (μ : Measure A) E) :
       ∃ a ∈ E, (ν : Measure K) (Prod.mk a ⁻¹' B) < η := by
   …

5. theorem OAI.PolycyclicRecognition.eq_zero_on_support_of_probability_tendsto_zero line 96

   Source documentation

   Vanishing bad probabilities force every supported limiting profile into the zero set of the continuous error observable.

   theorem eq_zero_on_support_of_probability_tendsto_zero
       {S : Type*} [TopologicalSpace S] [MeasurableSpace S] [BorelSpace S]
       [HasOuterApproxClosed S]
       (μn : ℕ → ProbabilityMeasure S) (μ : ProbabilityMeasure S)
       (hμ : Tendsto μn atTop (𝓝 μ)) (err : S → ℝ) (he : Continuous err)
       (hne : ∀ f, 0 ≤ err f)
       (hprob : ∀ η : ℝ, 0 < η →
         Tendsto (fun n => (μn n : Measure S) {f | η ≤ err f}) atTop (𝓝 0))
       {f : S} (hf : f ∈ (μ : Measure S).support) : err f = 0 := by
   …

6. theorem OAI.PolycyclicRecognition.affineProfileClass_of_finite_restrictions line 125

   Source documentation

   Affine restrictions on every finite set have one compatible label and offset on the entire domain. This also glues a compact exhaustion.

   theorem affineProfileClass_of_finite_restrictions
       {V W L : Type*} [TopologicalSpace V] [TopologicalSpace W]
       [AddCommGroup W] [Finite L] (A : L → C(V, W)) (f : C(V, W)) (z₀ : V)
       (h : ∀ Z : Set V, Z.Finite → ∃ a b, ∀ z ∈ Z, f z = A a z + b) :
       f ∈ affineProfileClass A := by
   …

   Mentions: OAI.PolycyclicRecognition.affineProfileClass