SplittingStability.lean`

29 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.SmoothObstruction.EuclideanSplitting.rate_eigen line 13
lemma OAI.SmoothObstruction.EuclideanSplitting.selected_sum line 24

theorem OAI.SmoothObstruction.EuclideanSplitting.transition_exterior_bound line 35

Source documentation

The dominant exterior estimate of the actual matrix transition uses the sum over the selected fast rates on every subinterval, not a coarse norm.

theorem transition_exterior_bound
    (U V : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ)
    (S : Finset (Fin d)) {s t : ℕ} (hst : s≤t) {γ g K C : ℝ}
    (hg : 0≤g) (hK : 0≤K) (hC : 0≤C)
    (hfast : ∀ j∈S,γ+g≤lam j) (hslow : ∀ j∉S,lam j≤γ-g)
    (hU : ‖U t‖≤Real.exp K) (hV : ‖V s‖≤Real.exp K)
    (hpoly : ∀ A : (EuclideanSpace ℝ (Fin d)) →L[ℝ] _,
      ‖exterior S.card A‖≤C*(max 1 ‖A‖)^S.card) :
    ‖exterior S.card (Matrix.toEuclideanCLM (n:=Fin d) (𝕜:=ℝ) (transition U V lam s t))‖≤
…

Mentions: OAI.SmoothObstruction.EuclideanSplitting.transition

lemma OAI.SmoothObstruction.EuclideanSplitting.nonleading_rate_product line 63

Source documentation

The actual nonleading diagonal eigenvalue is smaller by exp(-2g l). This is valid when the slow rates are positive as well as when negative.

lemma nonleading_rate_product (lam : Fin d → ℝ) (S : Finset (Fin d))
    {γ g l : ℝ} (hg : 0≤g) (hl : 0≤l)
    (hfast : ∀ j∈S,γ+g≤lam j) (hslow : ∀ j∉S,lam j≤γ-g)
    (q : powersetCard (Fin d) S.card) (hq : q.val≠S) :
    |∏ i : Fin S.card,Real.exp (l*lam (powersetCard.ofFinEmbEquiv.symm q i))|≤
      Real.exp (l*((∑ j∈S,lam j)-2*g)) := by
…

def OAI.SmoothObstruction.ExteriorStability.projectedMinor line 83
Source documentation
Actual projected maximal minor in fixed orthonormal endpoint coordinates. The rows use the selected projection coordinates and the columns are arbitrary starting vectors; starting bases need not be orthogonal.
```
noncomputable def projectedMinor (b : OrthonormalBasis ι ℝ E) (p : ℕ)
    (s : powersetCard ι p) (A : E →L[ℝ] E) (v : Fin p → E) : ℝ :=
…
```
lemma OAI.SmoothObstruction.ExteriorStability.projectedMinor_eq_det line 87
lemma OAI.SmoothObstruction.ExteriorStability.projectedMinor_transfer line 97

lemma OAI.SmoothObstruction.ExteriorStability.projectedMinor_basis_transfer line 112

Source documentation

Basis-change and orbit-transfer errors are paid against the true exterior operator norm. No coarse n-step C² estimate is substituted.

lemma projectedMinor_basis_transfer (b : OrthonormalBasis ι ℝ E) (p : ℕ)
    (s : powersetCard ι p) (A B : E →L[ℝ] E) (v w : Fin p → E) :
    |projectedMinor b p s B w-projectedMinor b p s A v|≤
      ‖exterior p B-exterior p A‖*‖exteriorPower.ιMulti ℝ p w‖+
      ‖exterior p A‖*‖exteriorPower.ιMulti ℝ p w-exteriorPower.ιMulti ℝ p v‖ := by
…

Mentions: OAI.SmoothObstruction.ExteriorStability.projectedMinor, OAI.SmoothObstruction.ExteriorStability.exterior

theorem OAI.SmoothObstruction.ExteriorStability.exists_wedge_lipschitz line 132
Source documentation
A uniform local modulus for the wedge of a fixed number of vectors. This is used when replacing actual subspaces by fixed frame-bin references.
```
theorem exists_wedge_lipschitz (p : ℕ) (R : ℝ) :
    ∃ C : ℝ,0≤C ∧ ∀ v w : Fin p → E,
      ‖v‖≤R → ‖w‖≤R →
      ‖exteriorPower.ιMulti ℝ p v-exteriorPower.ιMulti ℝ p w‖≤C*‖v-w‖ := by
…
```
lemma OAI.SmoothObstruction.ExteriorStability.projected_wedge_line line 153
Source documentation
A projected top wedge actually lies on the selected determinant line. In particular its coefficient is its norm, including the empty group.
```
lemma projected_wedge_line (b : OrthonormalBasis ι ℝ E) (p : ℕ)
    (s : powersetCard ι p) (v : Fin p → E)
    (hv : ∀ i j,j∉s → b.repr (v i) j=0) :
    exteriorPower.ιMulti ℝ p v=
      projectedMinor b p s (ContinuousLinearMap.id ℝ E) v • (b.exteriorPower p) s := by
…
```
Mentions: OAI.SmoothObstruction.ExteriorStability.projectedMinor
lemma OAI.SmoothObstruction.ExteriorStability.projected_wedge_norm line 184

theorem OAI.SmoothObstruction.ExteriorStability.projected_gauge_lower line 195

Source documentation

Quantitative projected leading-volume lower bound from the actual finite gauge and a left inverse of the endpoint projection on the fast vectors. The eigenvalue may converge to zero; it is never replaced by 1.

theorem projected_gauge_lower (b : OrthonormalBasis ι ℝ E) (p : ℕ)
    (s : powersetCard ι p) (U V D A Q J : E →L[ℝ] E)
    (v : Fin p → E) (a K H : ℝ) (hK : 0≤K)
    (hdiag : D=V*A*U)
    (hU : ‖exterior p U‖≤K) (hV : ‖exterior p V‖≤K)
    (hJ : ‖exterior p J‖≤H)
    (heigen : exterior p D (exteriorPower.ιMulti ℝ p v)=
      a • exteriorPower.ιMulti ℝ p v)
    (hleft : ∀ i,J (Q (A (U (v i))))=A (U (v i)))
    (hrange : ∀ i j,j∉s → b.repr (Q (A (U (v i)))) j=0) :
    |a| *‖exterior p U (exteriorPower.ιMulti ℝ p v)‖≤
      K^2*H*|projectedMinor b p s (Q*A*U) v| := by
…

Mentions: OAI.SmoothObstruction.ExteriorStability.exterior, OAI.SmoothObstruction.ExteriorStability.projectedMinor

theorem OAI.SmoothObstruction.EuclideanSplitting.finite_projected_volume line 244

Source documentation

Exact sum-rate lower bound for a genuine finite-gauge propagator followed by an endpoint projection. The input is its actual fast determinant line; the dimensional exterior bound is produced by exists_power_bound.

theorem finite_projected_volume
    (U V : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ)
    (hVU : ∀ t,V t*U t=1) (s t p : ℕ) (q : powersetCard (Fin d) p)
    (b : OrthonormalBasis (Fin d) ℝ (EuclideanSpace ℝ (Fin d)))
    (r : powersetCard (Fin d) p)
    (Q J : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d))
    {K C : ℝ} (hK : 0≤K) (hC : 0≤C)
    (hpoly : ∀ A : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d),
      ‖exterior p A‖≤C*(max 1 ‖A‖)^p)
    (hU : ‖U s‖≤Real.exp K) (hV : ‖V t‖≤Real.exp K) (hJ : ‖J‖≤2)
    (hleft : ∀ i,J (Q (Matrix.toEuclideanCLM (n:=Fin d) (𝕜:=ℝ)
…

def OAI.SmoothObstruction.CloseProjection.ambientInverse line 317
Source documentation
Extend the inverse endpoint restriction back to an ambient linear map. It is a left inverse on the actual moving fast space, with uniform norm 2.
```
noncomputable def ambientInverse (U V : Submodule ℝ E)
    (hdim : Module.finrank ℝ U=Module.finrank ℝ V)
    (hclose : ‖U.starProjection-V.starProjection‖≤1/2) : E →L[ℝ] E :=
…
```
lemma OAI.SmoothObstruction.CloseProjection.ambientInverse_left line 323
lemma OAI.SmoothObstruction.CloseProjection.norm_ambientInverse line 336
lemma OAI.SmoothObstruction.EuclideanSplitting.transition_group line 353
lemma OAI.SmoothObstruction.EuclideanSplitting.gauge_column_mem line 375

theorem OAI.SmoothObstruction.EuclideanSplitting.projected_fast_lower line 389

Source documentation

A true old fast leading minor, with the endpoint left inverse BUILT from the common-bin projection closeness, rather than assumed. The estimate retains exp(sum rates * length) even for contracting determinant lines.

theorem projected_fast_lower
    (U V : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ)
    (hUV : ∀ t,U t*V t=1) (hVU : ∀ t,V t*U t=1)
    (s t p : ℕ) (q : powersetCard (Fin d) p)
    (W : Submodule ℝ (EuclideanSpace ℝ (Fin d)))
    (hdim : Module.finrank ℝ W=p)
    (hclose : ‖(groupSpace (U t) (V t) (hUV t) (hVU t) q.val).starProjection-W.starProjection‖≤1/2)
    (b : OrthonormalBasis (Fin d) ℝ (EuclideanSpace ℝ (Fin d)))
    (r : powersetCard (Fin d) p)
    (hcoords : ∀ x∈W,∀ j∉r,b.repr x j=0)
    {K C : ℝ} (hK : 0≤K) (hC : 0≤C)
    (hpoly : ∀ A : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d),
…

Mentions: OAI.SmoothObstruction.EuclideanSplitting.groupSpace

lemma OAI.SmoothObstruction.ExteriorStability.norm_wedge_orthonormal line 431
Source documentation
The empty as well as every orthonormal determinant line has unit volume.
```
lemma norm_wedge_orthonormal (p : ℕ) (v : Fin p → E) (hv : Orthonormal ℝ v) :
    ‖exteriorPower.ιMulti ℝ p v‖=1 := by
…
```
lemma OAI.SmoothObstruction.EuclideanSplitting.rate_coordinate_wedge line 446

theorem OAI.SmoothObstruction.EuclideanSplitting.orthonormal_fast_minor_lower line 466

Source documentation

Leading fast minor in an ACTUAL orthonormal starting frame. The input columns are not the Lyapunov gauge columns. This yields a relative lower bound at the true sum-exponent scale, whether it expands or contracts.

theorem orthonormal_fast_minor_lower
    (U V : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ)
    (hUV : ∀ t,U t*V t=1) (hVU : ∀ t,V t*U t=1)
    (s t p : ℕ) (q : powersetCard (Fin d) p)
    (W : Submodule ℝ (EuclideanSpace ℝ (Fin d)))
    (hdim : Module.finrank ℝ W=p)
    (hclose : ‖(groupSpace (U t) (V t) (hUV t) (hVU t) q.val).starProjection-W.starProjection‖≤1/2)
    (b : OrthonormalBasis (Fin d) ℝ (EuclideanSpace ℝ (Fin d)))
    (r : powersetCard (Fin d) p)
    (hcoords : ∀ x∈W,∀ j∉r,b.repr x j=0)
    (w : Fin p → EuclideanSpace ℝ (Fin d)) (horth : Orthonormal ℝ w)
    (hw : ∀ i,w i∈groupSpace (U s) (V s) (hUV s) (hVU s) q.val)
…

Mentions: OAI.SmoothObstruction.EuclideanSplitting.groupSpace

lemma OAI.SmoothObstruction.ExteriorStability.diagonal_missing_line_bound line 556

Source documentation

A diagonal map on the orthogonal complement of one determinant line.

lemma diagonal_missing_line_bound (b : OrthonormalBasis ι ℝ E)
    (T : E →L[ℝ] E) (a : ι → ℝ) (ha : ∀ i,T (b i)=a i • b i)
    (i₀ : ι) (x : E) (hx : b.repr x i₀=0)
    {K : ℝ} (hK : 0≤K) (hbound : ∀ i,i≠i₀ → |a i|≤K) :
    ‖T x‖≤(Fintype.card ι:ℝ)*K*‖x‖ := by
…

lemma OAI.SmoothObstruction.EuclideanSplitting.coordinate_wedge_missing_fast line 590
lemma OAI.SmoothObstruction.EuclideanSplitting.rate_nonleading_volume line 611
Source documentation
True nonleading volume suppression for the diagonal propagator, applied to arbitrary vectors including one slow vector, not merely coordinate columns. The loss is the exact spectral gap exp(-2g length).
```
lemma rate_nonleading_volume (lam : Fin d → ℝ) (S : Finset (Fin d))
    {γ g l : ℝ} (hg : 0≤g) (hl : 0≤l)
    (hfast : ∀ j∈S,γ+g≤lam j) (hslow : ∀ j∉S,lam j≤γ-g)
    (v : Fin S.card → EuclideanSpace ℝ (Fin d))
    (i₀ : Fin S.card) (hv : v i₀∈coordinateSpace Sᶜ) :
    ‖exterior S.card (Matrix.toEuclideanCLM (n:=Fin d) (𝕜:=ℝ) (rate lam l))
…
```
Mentions: OAI.SmoothObstruction.EuclideanSplitting.coordinateSpace, OAI.SmoothObstruction.EuclideanSplitting.rate

theorem OAI.SmoothObstruction.EuclideanSplitting.transition_nonleading_volume line 632

Source documentation

The actual finite-gauge transition suppresses every maximal starting wedge containing a slow vector relative to its true fast sum-rate.

theorem transition_nonleading_volume
    (U V : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ)
    (hUV : ∀ t,U t*V t=1) (hVU : ∀ t,V t*U t=1)
    (S : Finset (Fin d)) {s t : ℕ} (hst : s≤t) {γ g K C : ℝ}
    (hg : 0≤g) (hK : 0≤K) (hC : 0≤C)
    (hfast : ∀ j∈S,γ+g≤lam j) (hslow : ∀ j∉S,lam j≤γ-g)
    (hU : ‖U t‖≤Real.exp K) (hV : ‖V s‖≤Real.exp K)
    (hpoly : ∀ A : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d),
      ‖exterior S.card A‖≤C*(max 1 ‖A‖)^S.card)
    (w : Fin S.card → EuclideanSpace ℝ (Fin d))
    (i₀ : Fin S.card) (hw : w i₀∈groupSpace (U s) (V s) (hUV s) (hVU s) Sᶜ) :
    ‖exterior S.card (Matrix.toEuclideanCLM (n:=Fin d) (𝕜:=ℝ) (transition U V lam s t))
…

Mentions: OAI.SmoothObstruction.EuclideanSplitting.groupSpace, OAI.SmoothObstruction.EuclideanSplitting.transition

def OAI.SmoothObstruction.ExteriorStability.continuousWedge line 698
Source documentation
Continuity is proved from the actual determinant polynomial.
```
noncomputable def continuousWedge (p : ℕ) :
    ContinuousMultilinearMap ℝ (fun _ : Fin p => E) (⋀[ℝ]^p E) where
…
```
lemma OAI.SmoothObstruction.ExteriorStability.unit_wedge_bound line 703
lemma OAI.SmoothObstruction.ExteriorStability.projectedMinor_norm_le line 711