OAI/Dynamics/SmoothObstruction/Counting.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothObstruction.EndpointBudget.eventual_admissible line 12

   Source documentation

   The literal endpoint hypotheses, simultaneously at every rank of the unchanged ambient dimension.

   theorem eventual_admissible {α : Type*} {l : Filter α} {b n δ : α → ℝ}
       (hbpos : ∀ᶠ k in l,0<b k) (hb : Tendsto b l (𝓝 0))
       (hn : Tendsto n l atTop) (hfloor : ∀ᶠ k in l,n k^(-1/10:ℝ)≤b k)
       (d : ℕ) (Dg R C K₀ Crel C₁ c β : ℝ) (hc : 0<c) (hβ : 0<β)
       (hδ : ∀ᶠ k in l,0≤δ k ∧ δ k≤Real.exp (-c*b k^(3/4:ℝ)*n k)) :
       ∀ᶠ k in l,∀ p≤d,
         admissible d p Dg R C K₀ Crel C₁ (b k) (n k) (b k^(1/2:ℝ)) (δ k) β := by
   …

   Mentions: OAI.SmoothObstruction.EndpointBudget.admissible

2. lemma OAI.SmoothObstruction.GridCount.ceil_grid_bound line 37
3. theorem OAI.SmoothObstruction.GridCount.original_grid_count line 46

   Source documentation

   A uniform exponential count for the two original starting grids. The strip-thinning denominator N cancels from the actual grid period.

   theorem original_grid_count (d j : ℕ) (Dc Dp Dg : ℝ) (hDc : 1≤Dc) (hDp : 1≤Dp) (hDg : 0≤Dg) :
       ∃ C : ℝ,0≤C ∧ ∀ (b : ℝ) (n N : ℕ),0<b → b≤1 → 1≤b*n → 0<N →
         let B := Dg*(b*n)
   …

4. lemma OAI.SmoothObstruction.ManifoldCoordinates.interior_of_selected_ball line 115
5. theorem OAI.SmoothObstruction.ManifoldCoordinates.grid_switches line 124

   Source documentation

   Finite translates, canonical references, the original retained carrier, and the genuine global switch are compatible at all sufficiently large scales. The explicit cell cardinality counts only two starting grids, never orbit labels.

   theorem grid_switches (hclosed : IsClosed (range I))
       (μ : Measure M) [IsProbabilityMeasure μ] (hμ : SmoothPositiveDensity I μ)
       (S : Diffeomorph I I M M ∞) (hS : MeasurePreserving S μ μ)
       (a : ι → M) (K : ι → Set M) (hK : ∀ i,IsCompact (K i))
       (hKU : ∀ i,K i⊆(chartAt H (a i)).source) (c : M → ι) (hc : Measurable c)
       (hcover : ∀ x,x∈K (c x)) (V : Set M) (hV : MeasurableSet V)
       (s : ℝ) (hs : 0<s) (hcore : ∀ x∈V,∀ y,dist y x ≤ s → c y=c x)
       (η : ℝ) (hη : 0<η) (hVm : μ.real Vᶜ≤η/100)
       (b : ℕ → ℝ) (n : ℕ → ℕ) (hbpos : ∀ k,0<b k) (hb : Tendsto b atTop (𝓝 0))
       (hn : Tendsto (fun k => (n k:ℝ)) atTop atTop)
       (hfloor : ∀ k,(n k:ℝ)^(-1/10:ℝ)≤b k)
       (Dg R₀ : ℝ) (hDg : 0≤Dg) (hR₀ : 0≤R₀)
   …

   Mentions: OAI.SmoothObstruction.SmoothPositiveDensity

6. theorem OAI.SmoothObstruction.ManifoldCoordinates.switching_from_gauges line 310

   Source documentation

   Smooth switching from a good gauge and a quantitative geometric boundary collar, for Euclidean and half-space manifold models.

   theorem switching_from_gauges (hclosed : IsClosed (range I))
       (μ : ProbabilityMeasure M) (hμ : SmoothPositiveDensity I (μ : Measure M))
       (S : Diffeomorph I I M M ∞) (hS : MeasurePreserving S (μ : Measure M) (μ : Measure M))
       (hcollar : ∀ (ι : Type) [Fintype ι] (a : ι → M) (K : ι → Set M),
         (∀ i,IsCompact (K i)) → (∀ i,K i⊆(chartAt H (a i)).source) →
         ∃ Cb : ℝ,0≤Cb ∧ ∀ r : ℝ,0≤r → ∃ W : Set M,MeasurableSet W ∧
           (μ : Measure M).real W≤Cb*r ∧
           ∀ i x,x∈K i → x∉W → closedBall ((extChartAt I (a i)) x) r⊆interior (range I)) :
       SmoothSwitching (μ : Measure M) S S.symm := by
   …

   Mentions: OAI.SmoothObstruction.SmoothPositiveDensity, OAI.SmoothObstruction.SmoothSwitching