OAI/Dynamics/SmoothObstruction/SpectralBins.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothObstruction.EuclideanSplitting.gaugeEquiv line 19
2. lemma OAI.SmoothObstruction.EuclideanSplitting.gaugeEquiv_apply line 40
3. lemma OAI.SmoothObstruction.EuclideanSplitting.gaugeEquiv_symm_apply line 44
4. def OAI.SmoothObstruction.EuclideanSplitting.coordinateSpace line 48
5. lemma OAI.SmoothObstruction.EuclideanSplitting.mem_coordinateSpace line 52
6. lemma OAI.SmoothObstruction.EuclideanSplitting.finrank_coordinateSpace line 57
7. lemma OAI.SmoothObstruction.EuclideanSplitting.mask_apply line 61
8. lemma OAI.SmoothObstruction.EuclideanSplitting.coordinateSpace_fixed line 67
9. def OAI.SmoothObstruction.EuclideanSplitting.groupSpace line 82
10. lemma OAI.SmoothObstruction.EuclideanSplitting.finrank_groupSpace line 87
11. lemma OAI.SmoothObstruction.EuclideanSplitting.groupSpace_fixed line 92
12. lemma OAI.SmoothObstruction.EuclideanSplitting.groupSpace_forward line 118
13. lemma OAI.SmoothObstruction.EuclideanSplitting.inverse_fast_product line 134
14. lemma OAI.SmoothObstruction.EuclideanSplitting.groupSpace_backward_lower line 143
15. lemma OAI.SmoothObstruction.SubspaceComparison.disjoint_of_stretch line 184

    Source documentation

    The elementary dimension/count comparison underlying finite singular rate comparison. Actual operator closeness and stretch bounds force disjointness.

    lemma disjoint_of_stretch (P Q : E →L[ℝ] E) (U V : Submodule ℝ E)
        {a b δ : ℝ} (hgap : b+δ<a) (hclose : ‖P-Q‖ ≤ δ)
        (hU : ∀ x : U, a*‖x‖ ≤ ‖P x‖) (hV : ∀ x : V, ‖Q x‖ ≤ b*‖x‖) :
        Disjoint U V := by
    …

16. lemma OAI.SmoothObstruction.SubspaceComparison.dimension_of_stretch line 201
17. lemma OAI.SmoothObstruction.SubspaceComparison.directed_of_product line 214

    Source documentation

    Product comparison controls directed distance using an actual inverse fast propagator B. K is the initial fast projector; its complementary image lies in the reference slow space.

    lemma directed_of_product (P Q B K : E →L[ℝ] E) (U V : Submodule ℝ E)
        {β σ δ : ℝ} (hβ : 0≤β)
        (hBP : B.comp P=K) (hB : ‖B‖≤β) (hclose : ‖P-Q‖≤δ)
        (hQ : ∀ x : U, ‖Q x‖≤σ*‖x‖)
        (hV : ∀ x, x-K x∈V) :
        ∀ x : U, ‖(x:E)-V.starProjection x‖ ≤ β*(σ+δ)*‖x‖ := by
    …

18. def OAI.SmoothObstruction.ShortBin.Gauge.product line 250
19. def OAI.SmoothObstruction.ShortBin.Gauge.space line 254
20. lemma OAI.SmoothObstruction.ShortBin.Gauge.rank line 258
21. lemma OAI.SmoothObstruction.ShortBin.Gauge.upper line 262
22. lemma OAI.SmoothObstruction.ShortBin.Gauge.lower line 270
23. lemma OAI.SmoothObstruction.ShortBin.count_le line 279

    Source documentation

    A count comparison from actual product closeness.

    lemma count_le (A B : Gauge d L K) {a b δ : ℝ}
        (hclose : ‖A.product-B.product‖≤δ)
        (hgap : Real.exp (b*L+2*K)+δ<Real.exp (a*L-2*K)) :
        (Finset.univ.filter (fun j => a≤A.lam j)).card ≤
          (Finset.univ.filter (fun j => b<B.lam j)).card := by
    …

    Mentions: OAI.SmoothObstruction.ShortBin.Gauge

24. lemma OAI.SmoothObstruction.ShortBin.exponential_separation line 300
25. lemma OAI.SmoothObstruction.RateThreshold.exists_candidate line 321

    Source documentation

    The manuscript's d+1 predetermined candidates. The choice is uniform over all other witnesses once short-product comparison has been applied.

    lemma exists_candidate (d : ℕ) (lam : Fin d → ℝ) {g : ℝ} (hg : 0<g) :
        ∃ j : Fin (d+1), ∀ i, 3*g < |lam i-(1+8*(j.val:ℝ))*g| := by
    …

26. lemma OAI.SmoothObstruction.RateThreshold.of_sandwich line 348

    Source documentation

    Two dimension comparisons exclude the whole intermediate rate band; no singular-value decomposition or arbitrary sorted-rate choice is needed.

    lemma of_sandwich {d p : ℕ} (lam : Fin d → ℝ) {γ g : ℝ} (hg : 0<g)
        (hlo : (Finset.univ.filter (fun j => γ-g≤lam j)).card≤p)
        (hhi : p≤(Finset.univ.filter (fun j => γ+g<lam j)).card) :
        (∀ j,lam j<γ-g ∨ γ+g<lam j) ∧
        (Finset.univ.filter (fun j => γ<lam j)).card=p := by
    …

27. theorem OAI.SmoothObstruction.ShortBin.common_gap line 395

    Source documentation

    All witnesses in one bin share the same predetermined threshold and rank. This proves the source bin threshold without singular-value minmax.

    theorem common_gap {ι : Type*} (A : ι→Gauge d L K) (e : ι) {g δ : ℝ}
        (hg : 0<g) (hclose : ∀ i,‖(A i).product-(A e).product‖≤δ)
        (hdecay : Real.exp (-2*g*L+4*K)≤1/2)
        (hnoise : δ<Real.exp (-2*K)/2) :
        ∃ j : Fin (d+1), let γ := (1+8*(j.val:ℝ))*g
    …

    Mentions: OAI.SmoothObstruction.ShortBin.Gauge

28. lemma OAI.SmoothObstruction.ManifoldCoordinates.actual_gauge_product line 458

    Source documentation

    Exact identification of the diagonal-gauge propagator with the derivative of the genuine nonautonomous chart expression. No product identity is assumed.

    lemma actual_gauge_product (S : Diffeomorph I I M M ∞) (a : ℕ → M)
        (x : M) {N : ℕ} {K : ℝ} (A : ShortBin.Gauge d N K)
        (hchart : ∀ t≤N,S^[t] x∈(chartAt H (a t)).source)
        (hint : I.IsInteriorPoint x)
        (hEq : ∀ t<N,(Matrix.toEuclideanCLM (n:=Fin d) (𝕜:=ℝ)).symm
    …

    Mentions: OAI.SmoothObstruction.ShortBin.Gauge

29. theorem OAI.SmoothObstruction.ManifoldCoordinates.uniform_actual_bin_threshold line 517

    Source documentation

    A bin threshold for an arbitrary family of actual manifold witnesses, including multiple gauges over one point. The constants are chosen uniformly from the finite compact atlas, before any bin, witness or frame is chosen. Short derivative closeness and chart carrying are proved, not assumed. Only the available finite gauge equations and the explicit scale inequalities remain as inputs.

    theorem uniform_actual_bin_threshold (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) :
        ∃ r C : ℝ,0<r ∧ 1≤C ∧
          ∀ (J : Type*) (x : J → M) (e : J) (c : ℕ → ι) (N : ℕ) (B g h : ℝ)
            (A : J → ShortBin.Gauge d N B),
            (∀ t≤N,S^[t] (x e)∈K (c t)) →
            (∀ i,I.IsInteriorPoint (x i)) →
            (∀ i,x i∈(chartAt H (a (c 0))).source) →
            (∀ i,‖(extChartAt I (a (c 0))) (x i)-(extChartAt I (a (c 0))) (x e)‖≤h) →
            C ^ N*h≤r →
            (∀ i,∀ t<N,(Matrix.toEuclideanCLM (n:=Fin d) (𝕜:=ℝ)).symm
    …

    Mentions: OAI.SmoothObstruction.ShortBin.Gauge

30. def OAI.SmoothObstruction.DirectedProjection.restrictProjection line 555
31. lemma OAI.SmoothObstruction.DirectedProjection.lower line 558
32. def OAI.SmoothObstruction.DirectedProjection.equiv line 569
33. lemma OAI.SmoothObstruction.DirectedProjection.equiv_apply line 581
34. lemma OAI.SmoothObstruction.DirectedProjection.reverse_directed line 586
35. lemma OAI.SmoothObstruction.DirectedProjection.one_sided_norm line 608
36. theorem OAI.SmoothObstruction.DirectedProjection.projector_distance line 619

    Source documentation

    A directed subspace estimate and equality of dimensions imply a full projector-distance bound. No chosen singular-vector continuity is assumed.

    theorem projector_distance (U V : Submodule ℝ E)
        (hdim : Module.finrank ℝ U=Module.finrank ℝ V) {ε : ℝ} (hε0 : 0≤ε) (hε : ε ≤ 1/2)
        (h : ∀ x : U, ‖(x:E)-V.starProjection x‖ ≤ ε*‖x‖) :
        ‖U.starProjection-V.starProjection‖ ≤ 3*ε := by
    …

37. lemma OAI.SmoothObstruction.ShortBin.Gauge.complement_mem line 649
38. lemma OAI.SmoothObstruction.ShortBin.slow_directed line 665

    Source documentation

    Actual short-product control of the slow subspace. The inverse fast propagator is constructed, rather than supplied as a desired estimate.

    lemma slow_directed (A B : Gauge d L K) (S T : Finset (Fin d)) {γ g δ : ℝ}
        (hclose : ‖A.product-B.product‖≤δ)
        (hAf : ∀ j∈Sᶜ,γ+g≤A.lam j) (hBs : ∀ j∈T,B.lam j≤γ-g) :
        ∀ x : B.space T, ‖(x:EuclideanSpace ℝ (Fin d))-(A.space S).starProjection x‖ ≤
          Real.exp (-(γ+g)*L+2*K)*(Real.exp ((γ-g)*L+2*K)+δ)*‖x‖ := by
    …

    Mentions: OAI.SmoothObstruction.ShortBin.Gauge

39. lemma OAI.SmoothObstruction.ShortBin.slow_projector_distance line 687
40. theorem OAI.SmoothObstruction.ShortBin.common_splittings line 709

    Source documentation

    A simultaneous fixed threshold and two common reference subspaces for all two-sided finite gauges in a bin. The two backward gauges are compared through their actual products, not through continuity of frame choices.

    theorem common_splittings {ι : Type*} (A Z : ι → Gauge d L K) (e : ι)
        {g δ : ℝ} (hg : 0<g) (hδ : 0≤δ)
        (hforward : ∀ i,‖(A i).product-(A e).product‖≤δ)
        (hbackward : ∀ i,‖(Z i).product-(Z e).product‖≤δ)
        (hU : ∀ i,(Z i).U 0=(A i).U 0) (hV : ∀ i,(Z i).V 0=(A i).V 0)
        (hlam : ∀ i k,(Z i).lam k= -(A i).lam k)
        (hdecay : Real.exp (-2*g*L+4*K)≤1/2)
        (hnoise : δ<Real.exp (-2*K)/2)
        (hsmall : Real.exp (-2*g*L+4*K)+δ*Real.exp ((1+8*(d:ℝ))*g*L+2*K)≤1/2) :
        ∃ j : Fin (d+1), let γ := (1+8*(j.val:ℝ))*g
    …

    Mentions: OAI.SmoothObstruction.ShortBin.Gauge

41. theorem OAI.SmoothObstruction.ManifoldCoordinates.uniform_actual_bin_splitting line 800

    Source documentation

    Uniform common reference spaces for actual two-sided smooth orbit witnesses in one bin. Neither continuity of frame choices nor short-product closeness is assumed: both comparisons are taken along the genuine forward and backward orbits, with chart carrying proved from initial closeness.

    theorem uniform_actual_bin_splitting (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) :
        ∃ rF CF rB CB : ℝ,0<rF ∧ 1≤CF ∧ 0<rB ∧ 1≤CB ∧
          ∀ (J : Type*) (x : J → M) (e : J) (cF cB : ℕ → ι) (N : ℕ) (B g h : ℝ)
            (A Z : J → ShortBin.Gauge d N B),
            cB 0=cF 0 →
            (∀ t≤N,S^[t] (x e)∈K (cF t)) →
            (∀ t≤N,S.symm^[t] (x e)∈K (cB t)) →
            (∀ i,I.IsInteriorPoint (x i)) →
            (∀ i,x i∈(chartAt H (a (cF 0))).source) →
            (∀ i,‖(extChartAt I (a (cF 0))) (x i)-(extChartAt I (a (cF 0))) (x e)‖≤h) →
    …

    Mentions: OAI.SmoothObstruction.ShortBin.Gauge