ExteriorPowers.lean`

27 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SmoothObstruction.ExteriorStability.exterior line 16
Source documentation
The exterior power as a continuous operator on the canonical inner product space.
```
noncomputable def exterior (p : ℕ) (A : E →L[ℝ] E) :
    (⋀[ℝ]^p E) →L[ℝ] (⋀[ℝ]^p E) :=
…
```
theorem OAI.SmoothObstruction.ExteriorStability.exterior_apply line 20

theorem OAI.SmoothObstruction.ExteriorStability.contDiff_det line 24

Source documentation

A determinant polynomial is smooth in all its entries.

theorem contDiff_det {D : Type*} [NormedAddCommGroup D] [NormedSpace ℝ D]
    {ι : Type*} [Fintype ι] [DecidableEq ι] {n : WithTop ℕ∞}
    (f : D → Matrix ι ι ℝ) (hf : ∀ i j, ContDiff ℝ n (fun x => f x i j)) :
    ContDiff ℝ n (fun x => (f x).det) := by
…

theorem OAI.SmoothObstruction.ExteriorStability.contDiff_wedge line 32
Source documentation
The canonical wedge of a fixed number of vectors is a smooth polynomial.
```
theorem contDiff_wedge (p : ℕ) :
    ContDiff ℝ ∞ (exteriorPower.ιMulti ℝ p (M := E)) := by
…
```
theorem OAI.SmoothObstruction.ExteriorStability.contDiff_exterior line 47
Source documentation
Exterior powers depend smoothly on the input operator.
```
theorem contDiff_exterior (p : ℕ) :
    ContDiff ℝ ∞ (exterior (E := E) p) := by
…
```
Mentions: OAI.SmoothObstruction.ExteriorStability.exterior

theorem OAI.SmoothObstruction.ExteriorStability.exists_exterior_lipschitz line 65

Source documentation

A uniform one-step exterior error on every bounded operator ball.

theorem exists_exterior_lipschitz (p : ℕ) (K : ℝ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (A B : E →L[ℝ] E),
      ‖A‖ ≤ K → ‖B - A‖ ≤ 1 →
      ‖exterior p B - exterior p A‖ ≤ C * ‖B - A‖ := by
…

Mentions: OAI.SmoothObstruction.ExteriorStability.exterior

theorem OAI.SmoothObstruction.ExteriorStability.exterior_one line 83
theorem OAI.SmoothObstruction.ExteriorStability.exterior_mul line 91

theorem OAI.SmoothObstruction.ExteriorStability.exists_uniform_exterior_lipschitz line 101

Source documentation

The same one-step constant works for every exterior degree up to d.

theorem exists_uniform_exterior_lipschitz (d : ℕ) (K : ℝ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (p : ℕ), p ≤ d → ∀ (A B : E →L[ℝ] E),
      ‖A‖ ≤ K → ‖B - A‖ ≤ 1 →
      ‖exterior p B - exterior p A‖ ≤ C * ‖B - A‖ := by
…

Mentions: OAI.SmoothObstruction.ExteriorStability.exterior

lemma OAI.SmoothObstruction.ExteriorStability.exterior_smul line 119
theorem OAI.SmoothObstruction.ExteriorStability.exists_power_bound line 133
Source documentation
A fixed dimensional polynomial bound sufficient to absorb changes of gauge into the source's exp(Cbn) factor, with exterior degree zero included.
```
theorem exists_power_bound (p : ℕ) : ∃ C : ℝ,1≤C ∧ ∀ A : E →L[ℝ] E,
    ‖exterior p A‖≤C*(max 1 ‖A‖)^p := by
…
```
Mentions: OAI.SmoothObstruction.ExteriorStability.exterior
lemma OAI.SmoothObstruction.ExteriorStability.norm_le_sum_basis line 160
Source documentation
A convenient basis norm bound; no singular-value theorem is needed.
```
lemma norm_le_sum_basis (b : OrthonormalBasis ι ℝ E) (T : E →L[ℝ] E) :
    ‖T‖≤∑ i,‖T (b i)‖ := by
…
```
lemma OAI.SmoothObstruction.ExteriorStability.exterior_eigen_basis line 182

lemma OAI.SmoothObstruction.ExteriorStability.exterior_diagonal_bound line 197

Source documentation

The complete exterior product estimate in a diagonal gauge depends on the SUM of selected rates, not on a coarser maximum single rate.

lemma exterior_diagonal_bound (b : OrthonormalBasis ι ℝ E) (p : ℕ)
    (T : E →L[ℝ] E) (a : ι → ℝ) (ha : ∀ i,T (b i)=a i • b i)
    {K : ℝ} (hK : ∀ s : powersetCard ι p,
      |∏ i : Fin p,a (powersetCard.ofFinEmbEquiv.symm s i)|≤K) :
    ‖exterior p T‖≤(Fintype.card (powersetCard ι p):ℝ)*K := by
…

Mentions: OAI.SmoothObstruction.ExteriorStability.exterior

lemma OAI.SmoothObstruction.ExteriorStability.exterior_eigen_lower line 218
lemma OAI.SmoothObstruction.ExteriorStability.eigen_exp_product line 228
lemma OAI.SmoothObstruction.ExteriorStability.exterior_rate_upper line 233

theorem OAI.SmoothObstruction.ExteriorStability.exterior_gauge_bound line 245

Source documentation

An explicit subinterval exterior bound after changing a finite gauge. This allows negative Λ, so that it is suitable for relative minor transfer.

theorem exterior_gauge_bound (b : OrthonormalBasis ι ℝ E) (p : ℕ)
    (U V D : E →L[ℝ] E) (lam : ι → ℝ) {l Λ G C : ℝ}
    (hl : 0≤l) (hG : 1≤G) (hC : 0≤C)
    (hpoly : ∀ A : E →L[ℝ] E,‖exterior p A‖≤C*(max 1 ‖A‖)^p)
    (hU : ‖U‖≤G) (hV : ‖V‖≤G)
    (ha : ∀ i,D (b i)=Real.exp (l*lam i) • b i)
    (hm : ∀ s : powersetCard ι p,∑ i : Fin p,lam (powersetCard.ofFinEmbEquiv.symm s i)≤Λ) :
    ‖exterior p (U*D*V)‖≤C^2*G^(2*p)*
      (Fintype.card (powersetCard ι p):ℝ)*Real.exp (l*Λ) := by
…

Mentions: OAI.SmoothObstruction.ExteriorStability.exterior

lemma OAI.SmoothObstruction.ExteriorStability.gauge_line_preimage_lower line 272
Source documentation
The fast determinant line has the exact sum rate before either endpoint change of gauge. This is the genuine volume-line lower input.
```
lemma gauge_line_preimage_lower (p : ℕ) (U V P D : E →L[ℝ] E)
    (hdiag : D=V*P*U) {a K : ℝ}
    (hV : ‖exterior p V‖≤K)
    (v : (⋀[ℝ]^p E)) (hv : exterior p D v=a • v) :
    |a| *‖v‖≤K*‖exterior p P (exterior p U v)‖ := by
…
```
Mentions: OAI.SmoothObstruction.ExteriorStability.exterior
lemma OAI.SmoothObstruction.ExteriorStability.gauge_line_lower line 284
lemma OAI.SmoothObstruction.ExteriorStability.diagonal_apply_complement line 307
lemma OAI.SmoothObstruction.ExteriorStability.wedge_leading_zero line 332
theorem OAI.SmoothObstruction.ExteriorStability.exists_wedge_bound line 343
Source documentation
A dimensional wedge constant, derived from continuity, not assumed.
```
theorem exists_wedge_bound (p : ℕ) : ∃ W : ℝ,0≤W ∧ ∀ v : Fin p → E,
    ‖exteriorPower.ιMulti ℝ p v‖≤W*∏ i,‖v i‖ := by
…
```

theorem OAI.SmoothObstruction.ExteriorStability.mixed_exterior_bound line 351

Source documentation

Nonleading p-minors, in the actual changed gauge, retain the full two-gap loss. The vanishing leading coefficient is proved from one slow vector.

theorem mixed_exterior_bound (b : OrthonormalBasis ι ℝ E) (p : ℕ)
    (s : powersetCard ι p) (U D V : E →L[ℝ] E) (a : ι → ℝ)
    (ha : ∀ i,D (b i)=a i • b i) {C G K W : ℝ}
    (hC : 0≤C) (hK : 0≤K) (hW : 0≤W)
    (hU : ‖exterior p U‖≤C) (hV : ‖V‖≤G)
    (hWb : ∀ v : Fin p → E,‖exteriorPower.ιMulti ℝ p v‖≤W*∏ i,‖v i‖)
    (hr : ∀ t : powersetCard ι p,t≠s→
      |∏ i : Fin p,a (powersetCard.ofFinEmbEquiv.symm t i)|≤K)
    (v : Fin p → E) (i₀ : Fin p)
    (hz : ∀ j : Fin p,b.repr (V (v i₀)) (powersetCard.ofFinEmbEquiv.symm s j)=0) :
    ‖exteriorPower.ιMulti ℝ p (fun i => (U*D*V) (v i))‖≤
      C*(Fintype.card (powersetCard ι p):ℝ)*K*W*G^p*(∏ i,‖v i‖) := by
…

Mentions: OAI.SmoothObstruction.ExteriorStability.exterior

lemma OAI.SmoothObstruction.RateSums.sdiff_card_eq line 397

theorem OAI.SmoothObstruction.RateSums.strict_rate_sum_gap line 406

Source documentation

Every nonfast minor of maximal fast degree loses at least two gap units. Nothing here requires positive fast rates or negative slow rates.

theorem strict_rate_sum_gap (lam : ι → ℝ) (F S : Finset ι)
    {γ g : ℝ} (hg : 0≤g) (hcard : S.card=F.card) (hne : S≠F)
    (hf : ∀ j∈F,γ+g≤lam j) (hs : ∀ j∉F,lam j≤γ-g) :
    ∑ j∈S,lam j ≤ (∑ j∈F,lam j)-2*g := by
…

theorem OAI.SmoothObstruction.RateSums.rate_sum_max line 435