OAI/Dynamics/SmoothObstruction/SwitchScales.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothObstruction.ManifoldCoordinates.finite_product_partition_uniform line 23

   Source documentation

   The actual full finite product partition is constructed from one original gauge reference per active starting bin. Wall strips are charged to the ORIGINAL measure. No endpoint or orbit chart code is included in the cell alphabet. The recovery assertion is precisely the ideal exchange needed by both joins.

   theorem finite_product_partition_uniform (μ : Measure M) [IsProbabilityMeasure μ]
       (S : Diffeomorph I I M M ∞) (a : ι → M) (K : ι → Set M)
       (hK : ∀ i,IsCompact (K i)) (hKU : ∀ i,K i⊆(chartAt H (a i)).source)
       (c : M → ι) (hc : ∀ x,x∈K (c x)) :
       ∃ D : ℝ,1≤D ∧ ∀ (C : Type*) [Fintype C] [MeasurableSpace C] [MeasurableSingletonClass C] (P : M → C),Measurable P → ∀ (chart : C → ι),
         (∀ x,chart (P x)=c x) → ∀ (G : Set M) (n : ℕ) (B R : ℝ),0≤B →
         ∀ (A : ∀ x:G,BilateralGauge I S a c n B R x) (T : G → Finset (Fin d))
           (δ : ℝ),0<δ → ∀ N : ℕ,0<N →
         let H₀ := Real.sqrt 2*Real.exp (2*B)
   …

   Mentions: OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge

2. def OAI.SmoothObstruction.SwitchScales.shortTime line 94
3. def OAI.SmoothObstruction.SwitchScales.root line 95
4. def OAI.SmoothObstruction.SwitchScales.gap line 96
5. def OAI.SmoothObstruction.SwitchScales.shortSignal line 97
6. lemma OAI.SmoothObstruction.SwitchScales.ceil_bounds line 99
7. lemma OAI.SmoothObstruction.SwitchScales.gap_short_lower line 110
8. lemma OAI.SmoothObstruction.SwitchScales.short_eventually line 118
9. theorem OAI.SmoothObstruction.SwitchScales.short_noise_decay line 135

   Source documentation

   The genuine short-product noise with its ceiling time is swallowed by one original spatial exponent, even after a full short-gap exponential cost.

   theorem short_noise_decay {ι : 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)
       {J C : ℝ} (hJ : 0≤J) (hC : 0≤C) :
       Tendsto (fun k => n k*Real.exp (J*(shortTime (b k) (n k):ℝ)+C*b k*n k+
         shortSignal (b k) (n k)-root (b k)*n k)) l (𝓝 0) := by
   …

   Mentions: OAI.SmoothObstruction.SwitchScales.shortTime, OAI.SmoothObstruction.SwitchScales.shortSignal, OAI.SmoothObstruction.SwitchScales.root

10. theorem OAI.SmoothObstruction.SwitchScales.projector_budget line 164

    Source documentation

    All common-bin projector errors, including the true product difference L C C^(2L) h0, are exponentially small at the authentic gap×time scale.

    theorem projector_budget {ι : 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)
        {C D A : ℝ} (hC : 1≤C) (hD : 0≤D) (hA : 0≤A) :
        let L (k : ι) := shortTime (b k) (n k)
    …

    Mentions: OAI.SmoothObstruction.SwitchScales.shortTime

11. theorem OAI.SmoothObstruction.SwitchScales.reference_budget line 241

    Source documentation

    A simultaneous usable envelope for all starting/endpoint bin estimates. The short time is still the source ceiling, not an adjustable subsequence.

    theorem reference_budget {ι : 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)
        {C D A r : ℝ} (hC : 1≤C) (hD : 0≤D) (hA : 0≤A) (hr : 0<r) :
        let L (k : ι) := shortTime (b k) (n k)
    …

    Mentions: OAI.SmoothObstruction.SwitchScales.shortTime

12. def OAI.SmoothObstruction.SwitchScales.refNoise line 311

    Source documentation

    The finite-time noise is monotone in the literal chart constant.

    def refNoise (C : ℝ) (N : ℕ) (h : ℝ) : ℝ := (N:ℝ)*C*C^(2*N)*h

13. def OAI.SmoothObstruction.SwitchScales.refError line 313
14. theorem OAI.SmoothObstruction.SwitchScales.refNoise_nonneg line 316
15. theorem OAI.SmoothObstruction.SwitchScales.refNoise_mono line 319
16. theorem OAI.SmoothObstruction.SwitchScales.refNoise_add_le line 326
17. theorem OAI.SmoothObstruction.SwitchScales.refError_mono line 342
18. theorem OAI.SmoothObstruction.SwitchScales.endpoint_refError_le line 349
19. theorem OAI.SmoothObstruction.SwitchScales.reference_constants_eventually line 364

    Source documentation

    All model-dependent reference constants are absorbed without changing b,n or the source short-time, mesh and clean projector-error scales.

    theorem reference_constants_eventually {κ : 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 C₁ C₂ C₃ C₄ D D₃ D₄ r₁ r₂ r₃ r₄ : ℝ}
        (hDg : 0≤Dg) (hC₁ : 1≤C₁) (hC₂ : 1≤C₂) (hC₃ : 1≤C₃) (hC₄ : 1≤C₄)
        (hD : 1≤D) (hD₃ : 1≤D₃) (hD₄ : 1≤D₄)
        (hr₁ : 0<r₁) (hr₂ : 0<r₂) (hr₃ : 0<r₃) (hr₄ : 0<r₄) :
        let L (k : κ) := shortTime (b k) (n k)
    …

    Mentions: OAI.SmoothObstruction.SwitchScales.shortTime

20. theorem OAI.SmoothObstruction.ManifoldCoordinates.eventual_finite_references line 465

    Source documentation

    Authentic finite-bin references on every sufficiently large original scale. The constants depend on the model and atlas, not the scale, alphabets, gauges, or good set. The clean error is exp(-b^(3/4)n).

    theorem eventual_finite_references (hclosed : IsClosed (range I))
        (S : Diffeomorph I I M M ∞) (a : ι → M) (K : ι → Set M)
        (hK : ∀ i,IsCompact (K i)) (hKU : ∀ i,K i⊆(chartAt H (a i)).source)
        {κ : Type*} {l : Filter κ} {b : κ → ℝ} {n : κ → ℕ}
        (hbpos : ∀ᶠ k in l,0<b k) (hb : Tendsto b l (𝓝 0))
        (hn : Tendsto (fun k => (n k:ℝ)) l atTop)
        (hfloor : ∀ᶠ k in l,(n k:ℝ)^(-1/10:ℝ)≤b k)
        (Dg R : ℝ) (hDg : 0≤Dg) :
        ∀ᶠ k in l,∀ (C : Type*) (c : M → ι) (P : M → C) (G : Set M)
          (A : ∀ x:G,BilateralGauge I S a c (n k) (Dg*(b k*n k)) R x),
          (∀ y,y∈K (c y)) → (∀ x y,P x=P y → c x=c y) →
          (∀ x∈G,I.IsInteriorPoint x) →
    …

    Mentions: OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge