OAI/Dynamics/SmoothObstruction/EndpointMass.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SmoothObstruction.SmoothScales.tendsto_zero_of_square_summable line 15
2. lemma OAI.SmoothObstruction.SmoothScales.summable_B_sixteen line 20
3. lemma OAI.SmoothObstruction.SmoothScales.dyadic_floor line 24
4. theorem OAI.SmoothObstruction.ExteriorStability.relative_exterior_dyadic line 39

   Source documentation

   Full asymptotic conclusion in source Lemma lem:relative-exterior, at the literal dyadic scales and with the literal summable chord sequence. The same proof supplies one rate of convergence for every matrix family satisfying the fixed displayed constants, since the bounding sequence in uniform_relative_small depends only on those constants and b.

   theorem relative_exterior_dyadic (d : ℕ) (_hd : 1 ≤ d) (K : ℝ) (_hK : 1 ≤ K)
       (p : ℕ) (hp : p ≤ d)
       (b : ℕ → ℝ) (hbpos : ∀ k, 0 < b k) (hbsum : Summable (fun k => (b k)^2))
       (hbfloor : ∀ k : ℕ, (2 : ℝ)^(-(k : ℝ) / 10) ≤ b k)
       (m : ℕ → ℕ)
       (A B : ℕ → ℕ → EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d))
       (σ a ε : ℕ → ℝ) (C₀ C₁ C₂ C₃ : ℝ) (hC₀ : 0 < C₀) (hC₃ : 0 ≤ C₃)
       (hdata : ∀ᶠ k in atTop,
         1 ≤ m k ∧ (m k : ℝ) ≤ 2 * (2 : ℝ)^k ∧
         0 ≤ a k ∧ a k ≤ C₁ * b k * (2 : ℝ)^k ∧ |σ k| ≤ C₂ ∧
         0 ≤ ε k ∧ ε k ≤ 1 ∧
         ε k ≤ C₃ * Real.exp (-(3 / 2 : ℝ) * SmoothScales.B (b k) * (2 : ℝ)^k) ∧
   …

   Mentions: OAI.SmoothObstruction.SmoothScales.B

5. theorem OAI.SmoothObstruction.RelativeAsymptotics.weighted_envelope_tendsto line 84

   Source documentation

   Exterior relative errors absorb every fixed exponential gauge cost. The multiplicative nonlinear error remains the authentic envelope times its exponential, not a dimension- or bin-dependent replacement.

   theorem weighted_envelope_tendsto {α : 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 C₁ C₂ C₃ A K : ℝ) :
       Tendsto (fun k => A*Real.exp (K*b k*n k)*
         (envelope C 0 C₁ C₂ C₃ (b k) (n k)*
           Real.exp (envelope C 0 C₁ C₂ C₃ (b k) (n k)))) l (𝓝 0) := by
   …

   Mentions: OAI.SmoothObstruction.RelativeAsymptotics.envelope

6. theorem OAI.SmoothObstruction.RelativeAsymptotics.common_relative_budget line 106

   Source documentation

   Literal leading-minor relative perturbation parameter tends to zero.

   theorem common_relative_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 Crel C₁ C₂ C₃ D W : ℝ) (p : ℕ) :
       Tendsto (fun k => 2*((C*(Real.exp (D*b k*n k))^p)^2*(C*2^p))*C*
         (envelope Crel 0 C₁ C₂ C₃ (b k) (n k)*
           Real.exp (envelope Crel 0 C₁ C₂ C₃ (b k) (n k)))*W) l (𝓝 0) := by
   …

   Mentions: OAI.SmoothObstruction.RelativeAsymptotics.envelope

7. def OAI.SmoothObstruction.EndpointBudget.leading line 127
8. def OAI.SmoothObstruction.EndpointBudget.normCost line 128
9. def OAI.SmoothObstruction.EndpointBudget.mixedCost line 129
10. def OAI.SmoothObstruction.EndpointBudget.relative line 130
11. def OAI.SmoothObstruction.EndpointBudget.graph line 134
12. theorem OAI.SmoothObstruction.EndpointBudget.all_ranks line 140

    Source documentation

    One eventual scalar budget works at ALL ranks, before choosing any starting cell, endpoint label, good gauge, or input frame.

    theorem all_ranks {α : 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 : ℕ) (C Crel C₁ C₂ C₃ D c : ℝ) (hc : 0<c)
        (F N V W β : Fin (d+1) → ℝ)
        (hF : ∀ p,0≤F p) (hN : ∀ p,0≤N p) (hV : ∀ p,0≤V p)
        (hW : ∀ p,0≤W p) (hβ : ∀ p,0<β p)
        (hδ : ∀ᶠ k in l,0≤δ k ∧ δ k≤Real.exp (-c*b k^(3/4:ℝ)*n k)) :
        ∀ᶠ k in l,∀ p : Fin (d+1),
          (F p*δ k)*(1+leading C (D*b k*n k) p.val*normCost C (D*b k*n k) (N p) p.val)≤1/2 ∧
          relative C Crel C₁ C₂ C₃ D (V p) (b k) (n k) p.val≤1/100 ∧
          (graph C D (N p) (V p) (W p) (b k) (n k) (δ k) p.val+
    …

    Mentions: OAI.SmoothObstruction.EndpointBudget.leading, OAI.SmoothObstruction.EndpointBudget.normCost, OAI.SmoothObstruction.EndpointBudget.relative, OAI.SmoothObstruction.EndpointBudget.graph

13. theorem OAI.SmoothObstruction.AtlasCores.closed_selector_germ line 176

    Source documentation

    A finite closed atlas selector can only approach charts whose compact carrier contains the limiting point. It need not be a continuous selector.

    theorem closed_selector_germ (K : ι → Set Y) (hK : ∀ i,IsClosed (K i))
        (q : Y → ι) (hq : ∀ y,y∈K (q y)) (y : Y) :
        ∀ᶠ z in 𝓝 y,y∈K (q z) := by
    …

14. theorem OAI.SmoothObstruction.AtlasCores.eventually_selected line 190

    Source documentation

    Local analytic branches may be checked simultaneously in finitely many possible chart codes, without adding those codes to any global partition.

    theorem eventually_selected (K : ι → Set Y) (hK : ∀ i,IsClosed (K i))
        (q : Y → ι) (hq : ∀ y,y∈K (q y)) (f : X → Y) (x : X)
        (hf : ContinuousAt f x) (V : ι → Set X)
        (hV : ∀ i,f x∈K i → V i∈𝓝 x) :
        ∀ᶠ u in 𝓝 x,u∈V (q (f u)) := by
    …

15. theorem OAI.SmoothObstruction.AtlasCores.selected_tube_germ line 214

    Source documentation

    A smooth local branch in all possible old charts satisfies the selected canonical tube relation on a whole relative neighborhood. No regularity of the finite chart selector is asserted and no intermediate chart pattern is recorded in the partition.

    theorem selected_tube_germ (K U : ι → Set Y) (hK : ∀ i,IsClosed (K i))
        (hU : ∀ i,IsOpen (U i)) (hKU : ∀ i,K i⊆U i)
        (q : Y → ι) (hq : ∀ y,y∈K (q y))
        (φ : ι → Y → E) (hφ : ∀ i,ContinuousOn (φ i) (U i))
        (f g : X → Y) (x : X) (hf : ContinuousAt f x) (hg : ContinuousAt g x)
        (δ : ℝ) (hbase : ∀ i,f x∈K i →
          g x∈U i ∧ ‖φ i (g x)-φ i (f x)‖<δ) :
        ∀ᶠ u in 𝓝 x,g u∈U (q (f u)) ∧
          ‖φ (q (f u)) (g u)-φ (q (f u)) (f u)‖≤δ := by
    …

16. theorem OAI.SmoothObstruction.AtlasCores.selected_path_tube_germ line 238

    Source documentation

    Finitely many positive and negative iterate charts may be handled at once. The number of cases affects only a local neighborhood, never the number of partition labels or an error/mass bound.

    theorem selected_path_tube_germ {T : Type*} [Finite T]
        (K U : ι → Set Y) (hK : ∀ i,IsClosed (K i))
        (hU : ∀ i,IsOpen (U i)) (hKU : ∀ i,K i⊆U i)
        (q : Y → ι) (hq : ∀ y,y∈K (q y))
        (φ : ι → Y → E) (hφ : ∀ i,ContinuousOn (φ i) (U i))
        (f g : T → X → Y) (x : X)
        (hf : ∀ t,ContinuousAt (f t) x) (hg : ∀ t,ContinuousAt (g t) x)
        (δ : ℝ) (hbase : ∀ t i,f t x∈K i →
          g t x∈U i ∧ ‖φ i (g t x)-φ i (f t x)‖<δ) :
        ∀ᶠ u in 𝓝 x,∀ t,g t u∈U (q (f t u)) ∧
          ‖φ (q (f t u)) (g t u)-φ (q (f t u)) (f t u)‖≤δ := by
    …

17. theorem OAI.SmoothObstruction.ManifoldCoordinates.actual_selected_tube_germ line 264

    Source documentation

    A genuine sharp orbit tube persists in all selected old charts along a continuous local branch. Intermediate chart selectors need not be locally constant; their finite compact cores suffice.

    theorem actual_selected_tube_germ (hclosed : IsClosed (range I))
        (a : ι → M) (K : ι → Set M)
        (hK : ∀ i,IsCompact (K i)) (hKU : ∀ i,K i⊆(chartAt H (a i)).source) :
        ∃ r C : ℝ,0<r ∧ 1≤C ∧
          ∀ {X T : Type*} [TopologicalSpace X] [Finite T]
            (c : M → ι) (_ : ∀ z,z∈K (c z))
            (f g : T → X → M) (x : X) (ρ δ : ℝ),
            (∀ t,ContinuousAt (f t) x) → (∀ t,ContinuousAt (g t) x) →
            0≤ρ → ρ≤r → C*ρ<δ →
            (∀ t,closedBall ((extChartAt I (a (c (f t x)))) (f t x)) ρ⊆interior (range I)) →
            (∀ t,g t x∈(extChartAt I (a (c (f t x)))).source ∧
              ‖(extChartAt I (a (c (f t x)))) (g t x)-
    …

18. theorem OAI.SmoothObstruction.ManifoldCoordinates.original_tube_germ line 306

    Source documentation

    Actual orbit tubes persist locally under continuous input and output branches without continuity of the atlas selector.

    theorem original_tube_germ (hclosed : IsClosed (range I))
        (a : ι → M) (K : ι → Set M)
        (hK : ∀ i,IsCompact (K i)) (hKU : ∀ i,K i⊆(chartAt H (a i)).source) :
        ∃ r C : ℝ,0<r ∧ 1≤C ∧
          ∀ {X : Type*} [TopologicalSpace X] (S : Diffeomorph I I M M ∞)
            (c : M → ι) (_ : ∀ z,z∈K (c z))
            (f g : X → M) (x : X) (n : ℕ) (ρ δ : ℝ),
            ContinuousAt f x → ContinuousAt g x →
            0≤ρ → ρ≤r → C*ρ<δ →
            (∀ t : Fin (n+1),closedBall ((extChartAt I (a (c (S^[t.val] (f x))))) (S^[t.val] (f x))) ρ
              ⊆interior (range I)) →
            originalTube I S a c (n:=n) ρ (f x) (g x) →
    …

    Mentions: OAI.SmoothObstruction.ManifoldCoordinates.originalTube

19. theorem OAI.SmoothObstruction.ManifoldCoordinates.original_pair_germ line 341

    Source documentation

    The authentic smooth local pair branch agrees with the canonical switch on a relative neighborhood of the retained set. No regularity of good gauge witnesses or intermediate chart labels enters this assertion.

    theorem original_pair_germ (hclosed : IsClosed (range I))
        (a : ι → M) (K : ι → Set M)
        (hK : ∀ i,IsCompact (K i)) (hKU : ∀ i,K i⊆(chartAt H (a i)).source) :
        ∃ r C : ℝ,0<r ∧ 1≤C ∧
          ∀ {X J A : Type*} [TopologicalSpace X]
            (S : Diffeomorph I I M M ∞) (c : M → ι) (_ : ∀ z,z∈K (c z))
            (P : M → A) (L : M → J) (R : Set M)
            (Wf Wb : A×A → Submodule ℝ (EuclideanSpace ℝ (Fin d)))
            (n : ℕ) (ρ δ : ℝ) (Φ : M×M → M×M)
            (e Ψ : X → M×M) (x : X),
            ContinuousAt e x → ContinuousAt Ψ x → 0≤ρ → ρ≤r → C*ρ<δ →
            (∀ t : Fin (n+1),
    …

20. lemma OAI.SmoothObstruction.ChartDensity.inverse_germ line 408

    Source documentation

    Measurable total chart extensions agree with the authentic inverse chart on a neighborhood of every interior coordinate point.

    lemma inverse_germ (a : M) (u : E₀) (hu : u∈(extChartAt I a).target)
        (hi : u∈interior (range I)) :
        ContinuousAt (extChartAt I a).symm u ∧
        ∀ᶠ v in 𝓝 u,inverse I a v=(extChartAt I a).symm v ∧
          coordinates I a ((extChartAt I a).symm v)=v := by
    …

    Mentions: OAI.SmoothObstruction.ChartDensity.inverse, OAI.SmoothObstruction.ChartDensity.coordinates

21. lemma OAI.SmoothObstruction.ChartDensity.pair_inverse_germ line 421
22. theorem OAI.SmoothObstruction.ChartDensity.retained_pair_germ line 438

    Source documentation

    Physical agreement on retained inputs gives the exact coordinate germ required for change of variables, despite arbitrary chart extensions away from their sources. Only the original retained set is used.

    theorem retained_pair_germ (a : M) (G : Set (M×M)) (Φ : M×M → M×M)
        (Ψ : E₀×E₀ → E₀×E₀) (u : E₀×E₀) (hΨ : ContinuousAt Ψ u)
        (hu₁ : u.1∈(extChartAt I a).target) (hu₂ : u.2∈(extChartAt I a).target)
        (iu₁ : u.1∈interior (range I)) (iu₂ : u.2∈interior (range I))
        (hv₁ : (Ψ u).1∈(extChartAt I a).target) (hv₂ : (Ψ u).2∈(extChartAt I a).target)
        (iv₁ : (Ψ u).1∈interior (range I)) (iv₂ : (Ψ u).2∈interior (range I))
        (hag : let r₀ := Prod.map (extChartAt I a).symm (extChartAt I a).symm
    …

23. lemma OAI.SmoothObstruction.ManifoldCoordinates.original_endpoint_iff_coordinates line 477

    Source documentation

    Endpoint rows in a fixed old chart are exactly the canonical projected equation when the ORIGINAL endpoint label is retained.

    lemma original_endpoint_iff_coordinates (S : Diffeomorph I I M M ∞)
        (a : ι → M) (c : M → ι) (P : M → A)
        (hPc : ∀ x y,P x=P y → c x=c y) (W : A×A → Submodule ℝ E₀)
        (a₀ x : M) (n : ℕ) (u v : E₀)
        (b : OrthonormalBasis (Fin d) ℝ E₀) (r : powersetCard (Fin d) p)
        (hr : ∀ j∈r,b j∈W (P x,P (S^[n] x)))
        (hz : ∀ z∈W (P x,P (S^[n] x)),∀ j∉r,b.repr z j=0)
        (hP₀ : P ((extChartAt I a₀).symm u)=P x)
        (hP₁ : P (S^[n] ((extChartAt I a₀).symm u))=P (S^[n] x)) :
        originalEndpoint I S a c (n:=n)
    …

    Mentions: OAI.SmoothObstruction.ManifoldCoordinates.originalEndpoint

24. lemma OAI.SmoothObstruction.ManifoldCoordinates.inverse_continuousAt_interior line 496
25. theorem OAI.SmoothObstruction.ManifoldCoordinates.original_equations_germ line 506

    Source documentation

    The four original endpoint equations of a smooth pair branch follow from the four IFT row equations, using only the OLD starting and endpoint labels. No intermediate orbit label is frozen or added to the cell.

    theorem original_equations_germ {q : ℕ}
        (S : Diffeomorph I I M M ∞) (a : ι → M) (c : M → ι) (P : M → A)
        (hPc : ∀ x y,P x=P y → c x=c y)
        (Wf Wb : A×A → Submodule ℝ E₀) (a₀ x y : M) (n : ℕ)
        (b₀ b₁ c₀ c₁ : OrthonormalBasis (Fin d) ℝ E₀)
        (r₀ r₁ : powersetCard (Fin d) p) (s₀ s₁ : powersetCard (Fin d) q)
        (hb₀ : ∀ j∈r₀,b₀ j∈Wf (P x,P (S^[n] x)))
        (hz₀ : ∀ z∈Wf (P x,P (S^[n] x)),∀ j∉r₀,b₀.repr z j=0)
        (hb₁ : ∀ j∈r₁,b₁ j∈Wf (P y,P (S^[n] y)))
        (hz₁ : ∀ z∈Wf (P y,P (S^[n] y)),∀ j∉r₁,b₁.repr z j=0)
        (hc₀ : ∀ j∈s₀,c₀ j∈Wb (P x,P (S.symm^[n] x)))
        (hv₀ : ∀ z∈Wb (P x,P (S.symm^[n] x)),∀ j∉s₀,c₀.repr z j=0)
    …

26. theorem OAI.SmoothObstruction.ManifoldCoordinates.controlled_original_germ line 563

    Source documentation

    The authentic eight endpoint minors give the local Jacobian germ of the ORIGINAL measurable switch. Rank-zero blocks are included. The agreement is relative to retained original inputs, not an extension or a different law.

    theorem controlled_original_germ (hclosed : IsClosed (range I))
        (a : ι → M) (K : ι → Set M)
        (hK : ∀ i,IsCompact (K i)) (hKU : ∀ i,K i⊆(chartAt H (a i)).source) :
        ∃ r C β : ℝ,0<r ∧ 1≤C ∧ 0<β ∧
          ∀ {A J : Type*} (S : Diffeomorph I I M M ∞) (c : M → ι)
            (P : M → A) (L : M → J) (R : Set M)
            (Wf Wb : A×A → Submodule ℝ E₀) (n : ℕ) (ρ δ : ℝ)
            (Φ : M×M → M×M) (G : Set (M×M)) (x y : M),
            (∀ z,z∈K (c z)) → (∀ u v,P u=P v → c u=c v) → c x=c y →
            0≤ρ → ρ≤r → C*ρ<δ →
            (∀ u∈G,u.1∈R ∧ u.2∈R ∧ L u.1=L u.2) →
            (∀ u∈R,∀ v∈R,L u=L v → ∀ z,
    …

27. theorem OAI.SmoothObstruction.ManifoldCoordinates.gauge_endpoint_minor line 703

    Source documentation

    The original orbit-tube endpoint minor, now with the actual bilateral finite-time gauge. This is uniform in every starting bin and every rank.

    theorem gauge_endpoint_minor (hclosed : IsClosed (range I))
        (S : Diffeomorph I I M M ∞) (a : ι → M) (L : ι → Set M)
        (hL : ∀ i,IsCompact (L i)) (hLU : ∀ i,L i⊆(chartAt H (a i)).source)
        (Dg : ℝ) (hDg : 0≤Dg) :
        ∃ r K₀ Crel C₁ : ℝ,0<r ∧ 1≤K₀ ∧ 0≤Crel ∧ 0≤C₁ ∧
          ∀ {p q : ℕ} (c : M → ι) (x y : M) (n : ℕ) (b R C δ β γ g : ℝ)
            (A : BilateralGauge I S a c n (Dg*(b*n)) R x)
            (T : Finset (Fin d)) (_ : T.card=p),
            (∀ z,z∈L (c z)) → 0≤b → 1≤b*n → 0≤R → 0≤g → 0≤C → 0≤δ →
            (∀ j∈T,γ+g≤A.lam j) → (∀ j∉T,A.lam j≤γ-g) →
            let ρ := Real.exp (-(3/2:ℝ)*SmoothScales.B b*n)
    …

    Mentions: OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge, OAI.SmoothObstruction.SmoothScales.B

28. def OAI.SmoothObstruction.EndpointBudget.admissible line 752

    Source documentation

    Literal three errors entering the actual endpoint-minor theorem.

    def admissible (d p : ℕ) (Dg R C K₀ Crel C₁ b n g δ β : ℝ) : Prop :=
    …

29. theorem OAI.SmoothObstruction.ManifoldCoordinates.gauge_endpoint_family line 777

    Source documentation

    One authentic frame and one original leading matrix control the whole old-chart orbit tube. Neither the frame nor the normalization is reselected at the perturbed point.

    theorem gauge_endpoint_family (hclosed : IsClosed (range I))
        (S : Diffeomorph I I M M ∞) (a : ι → M) (L : ι → Set M)
        (hL : ∀ i,IsCompact (L i)) (hLU : ∀ i,L i⊆(chartAt H (a i)).source)
        (Dg : ℝ) (hDg : 0≤Dg) :
        ∃ r K₀ Crel C₁ : ℝ,0<r ∧ 1≤K₀ ∧ 0≤Crel ∧ 0≤C₁ ∧
          ∀ {p q : ℕ} (c : M → ι) (x : M) (n : ℕ) (b R C δ β γ g : ℝ)
            (A : BilateralGauge I S a c n (Dg*(b*n)) R x)
            (T : Finset (Fin d)) (_ : T.card=p),
            (∀ z,z∈L (c z)) → 0≤b → 1≤b*n → 0≤R → 0≤g → 0≤C → 0≤δ →
            (∀ j∈T,γ+g≤A.lam j) → (∀ j∉T,A.lam j≤γ-g) →
            let ρ := Real.exp (-(3/2:ℝ)*SmoothScales.B b*n)
    …

    Mentions: OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge, OAI.SmoothObstruction.SmoothScales.B

30. lemma OAI.SmoothObstruction.ManifoldCoordinates.originalTube_self line 823
31. def OAI.SmoothObstruction.ManifoldCoordinates.OriginalEndpointControl line 839
32. lemma OAI.SmoothObstruction.ManifoldCoordinates.originalEndpoint_coordinates line 850
33. theorem OAI.SmoothObstruction.ManifoldCoordinates.family_original_germ line 864

    Source documentation

    Fixed old-chart endpoint families give the actual retained-set relative germ.

    theorem family_original_germ (hclosed : IsClosed (range I))
        (a : ι → M) (K : ι → Set M)
        (hK : ∀ i,IsCompact (K i)) (hKU : ∀ i,K i⊆(chartAt H (a i)).source) :
        ∃ r C β : ℝ,0<r ∧ 1≤C ∧ 0<β ∧
          ∀ {A J : Type*} (S : Diffeomorph I I M M ∞) (c : M → ι)
            (P : M → A) (L : M → J) (R : Set M)
            (Wf Wb : A×A → Submodule ℝ E₀) (n : ℕ) (ρ δ : ℝ)
            (Φ : M×M → M×M) (G : Set (M×M)) (x y : M),
            (∀ z,z∈K (c z)) → (∀ u v,P u=P v → c u=c v) → c x=c y →
            0≤ρ → ρ≤r → C*ρ<δ →
            (∀ u∈G,u.1∈R ∧ u.2∈R ∧ L u.1=L u.2) →
            (∀ u∈R,∀ v∈R,L u=L v → ∀ z,
    …

34. lemma OAI.SmoothObstruction.finite_positive_bound line 950