FiniteRankGap.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Finite-rank gap and determinant perturbations

The coercivity argument for the moment matrix in Stationary instability and nonuniqueness for axisymmetric swirl-free Navier–Stokes, Section 2, gives a lower norm bound in terms of the residual map. Perturbations smaller than this bound preserve injectivity and, in finite dimensions over the reals, the sign of the determinant.

def OAI.StationaryNS.momentMatrix line 29
Source documentation
The moment matrix I + BC, expressed without choosing coordinates.
```
def momentMatrix (B : E →L[ℝ] F) (C : F →L[ℝ] E) : F →L[ℝ] F :=
…
```

theorem OAI.StationaryNS.finite_rank_gap line 34

Source documentation

The algebraic least-singular-value estimate for the moment matrix. The residual map R and the coercivity hypothesis give a lower norm bound without a finite-dimensional assumption.

theorem finite_rank_gap (B : E →L[ℝ] F) (C : F →L[ℝ] E)
    (R : F →L[ℝ] E →L[ℝ] ℝ) {ε β δ : ℝ}
    (hε : 0 < ε) (hB : ‖B‖ ≤ β) (hR : ‖R‖ ≤ δ)
    (hcoercive : ∀ y, ε * ‖C y‖ ^ 2 ≤ R (momentMatrix B C y) (C y)) (y : F) :
    ε / (ε + β * δ) * ‖y‖ ≤ ‖momentMatrix B C y‖ := by
…

Mentions: OAI.StationaryNS.momentMatrix

theorem OAI.StationaryNS.injective_of_perturbation line 74

Source documentation

A perturbation smaller than a lower norm bound is injective, in any dimension.

theorem injective_of_perturbation (J P : E →L[ℝ] E) {γ : ℝ}
    (hgap : ∀ x, γ * ‖x‖ ≤ ‖J x‖) (hpert : ‖P - J‖ < γ) :
    Function.Injective P := by
…

theorem OAI.StationaryNS.injective_segment line 88

Source documentation

The straight segment to a perturbation smaller than a lower norm bound remains injective.

theorem injective_segment (J P : E →L[ℝ] E) {γ : ℝ}
    (hgap : ∀ x, γ * ‖x‖ ≤ ‖J x‖) (hpert : ‖P - J‖ < γ)
    {t : ℝ} (ht : t ∈ Set.Icc (0 : ℝ) 1) :
    Function.Injective (J + t • (P - J)) := by
…

theorem OAI.StationaryNS.same_sign_endpoints line 101
Source documentation
A continuous real function that never vanishes on the unit interval has the same strict sign at its endpoints.
```
theorem same_sign_endpoints {f : ℝ → ℝ}
    (hcont : ContinuousOn f (Set.Icc 0 1))
    (hne : ∀ t ∈ Set.Icc (0 : ℝ) 1, f t ≠ 0) : 0 < f 0 * f 1 := by
…
```

theorem OAI.StationaryNS.determinant_sign_of_perturbation line 123

Source documentation

Finite-dimensional real determinant signs are preserved by perturbations smaller than a lower norm bound.

theorem determinant_sign_of_perturbation [FiniteDimensional ℝ E]
    (J P : E →L[ℝ] E) {γ : ℝ}
    (hgap : ∀ x, γ * ‖x‖ ≤ ‖J x‖) (hpert : ‖P - J‖ < γ) :
    0 < J.det * P.det := by
…