GlobalSwitching.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.SmoothObstruction.EndpointFrame.GoodEndpoint.mono line 12

theorem OAI.SmoothObstruction.EndpointFrame.four_endpoint_branch_uniform line 20

Source documentation

A single endpoint minor tolerance for every possible rank in dimension d.

theorem four_endpoint_branch_uniform : ∃ δ : ℝ,0<δ ∧
    ∀ {p q : ℕ},p≤d → q≤d →
    ∀ (U V : Submodule ℝ E) (_ : IsCompl U V)
      (u : OrthonormalBasis (Fin p) ℝ U) (v : OrthonormalBasis (Fin q) ℝ V)
      (b₀ b₁ c₀ c₁ : OrthonormalBasis (Fin d) ℝ E)
      (r₀ r₁ : powersetCard (Fin d) p) (s₀ s₁ : powersetCard (Fin d) q)
      (f₀ f₁ g₀ g₁ : E → E) (x y z w : E)
      (A₀ A₁ : Matrix (Fin p) (Fin p) ℝ) (D₀ D₁ : Matrix (Fin q) (Fin q) ℝ),
      GoodEndpoint δ b₀ r₀ (fun i => (u i:E)) (fun i => (v i:E)) f₀ x A₀ →
      GoodEndpoint δ b₀ r₀ (fun i => (u i:E)) (fun i => (v i:E)) f₀ z A₀ →
      GoodEndpoint δ b₁ r₁ (fun i => (u i:E)) (fun i => (v i:E)) f₁ y A₁ →
      GoodEndpoint δ b₁ r₁ (fun i => (u i:E)) (fun i => (v i:E)) f₁ w A₁ →
…

Mentions: OAI.SmoothObstruction.EndpointFrame.GoodEndpoint

theorem OAI.SmoothObstruction.ManifoldCoordinates.controlled_original_germ_uniform line 73

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_uniform (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<β ∧
      ∀ {p q : ℕ},p≤d → q≤d →
      ∀ {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) →
…

theorem OAI.SmoothObstruction.ManifoldCoordinates.family_original_germ_uniform line 213

Source documentation

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

theorem family_original_germ_uniform (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<β ∧
      ∀ {p q : ℕ},p≤d → q≤d →
      ∀ {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) →
…

theorem OAI.SmoothObstruction.ManifoldCoordinates.bilateral_endpoint_control line 311

Source documentation

Both original endpoint families from a SINGLE bilateral gauge. The inverse family uses exactly its reversed gauge, not an unrelated certificate. All constants precede ranks, labels, gauges, and the common starting bases.

theorem bilateral_endpoint_control (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) :
    ∃ rF K₀F CreF C₁F rB K₀B CreB C₁B : ℝ,
      0<rF ∧ 1≤K₀F ∧ 0≤CreF ∧ 0≤C₁F ∧ 0<rB ∧ 1≤K₀B ∧ 0≤CreB ∧ 0≤C₁B ∧
      ∀ {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) (_ : Tᶜ.card=q),
        (∀ 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

lemma OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge.forwardSpace_compl line 371
theorem OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge.forwardSpace_bases line 380
Source documentation
The common starting bases are orthonormal within each actual gauge group; no global orthogonality or conditioning of their union is postulated.
```
theorem BilateralGauge.forwardSpace_bases (t : ℕ) (T : Finset (Fin d)) :
    Nonempty (OrthonormalBasis (Fin T.card) ℝ (A.forwardSpace I S a c t T)) ∧
    Nonempty (OrthonormalBasis (Fin (d-T.card)) ℝ (A.forwardSpace I S a c t Tᶜ)) := by
…
```
lemma OAI.SmoothObstruction.ManifoldCoordinates.OriginalEndpointControl.mono line 398

theorem OAI.SmoothObstruction.ManifoldCoordinates.gauge_original_germ_sharp line 420

Source documentation

A genuine pair germ from three bilateral gauges in the ORIGINAL atlas. All radii and minor tolerances precede the finite labels and the fast rank.

theorem gauge_original_germ_sharp (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)
    (Dg : ℝ) (hDg : 0≤Dg) :
    ∃ r Cg β K₀F CreF C₁F K₀B CreB C₁B : ℝ,
      0<r ∧ 1≤Cg ∧ 0<β ∧ 1≤K₀F ∧ 0≤CreF ∧ 0≤C₁F ∧
      1≤K₀B ∧ 0≤CreB ∧ 0≤C₁B ∧
      ∀ {A J : Type*} (c : M → ι)
        (P : M → A) (L : M → J) (R : Set M)
        (Wf Wb : A×A → Submodule ℝ E₀) (n : ℕ) (b R₀ Cext δ ε γ g ρ : ℝ)
        (Φ : M×M → M×M) (G : Set (M×M)) (x y : M),
        let σ := Real.exp (-(3/2:ℝ)*SmoothScales.B b*n)
…

Mentions: OAI.SmoothObstruction.SmoothScales.B