PrimitiveOperatorStability.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Uniform stability of the finite primitive inverse when its coefficient functionals, cutoffs and phase covectors all vary independently.

abbrev OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PrimitiveOperatorData line 21
def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.primitiveDataOperator line 24
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.primitiveDataOperator_smooth line 27
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.primitiveDataInverse_smoothAt line 44
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.isOpen_primitiveDataPositive line 51
theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.compact_primitiveData_stability line 70
Source documentation
On a compact family of exact reference decompositions, independent perturbations of every entry preserve invertibility and the selected positive amplitude coefficient. In particular the coefficient functionals may vary.
```
theorem compact_primitiveData_stability (i : ι)
    {K : Set (PrimitiveOperatorData ι × TensorFiber)} (hK : IsCompact K)
    (hid : ∀ w ∈ K, primitiveDataOperator w.1 = ContinuousLinearMap.id ℝ TensorFiber)
    (hpos : ∀ w ∈ K, 0 < w.1.1.1 i w.2) :
    ∃ eps : ℝ, 0 < eps ∧ ∀ w ∈ K, ∀ w' : PrimitiveOperatorData ι × TensorFiber,
      ‖w'-w‖ < eps → (primitiveDataOperator w'.1).IsInvertible ∧
        0 < w'.1.1.1 i ((primitiveDataOperator w'.1).inverse w'.2) := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PrimitiveOperatorData, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.TensorFiber, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.primitiveDataOperator

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.compact_inverse_coefficient_stability line 93

Source documentation

A local matrix and the one active coefficient are enough for compact stability. No continuity of inactive chart functionals is required.

theorem compact_inverse_coefficient_stability
    {K : Set (((TensorFiber →L[ℝ] TensorFiber) × (TensorFiber →L[ℝ] ℝ)) × TensorFiber)}
    (hK : IsCompact K)
    (hid : ∀ w ∈ K, w.1.1 = ContinuousLinearMap.id ℝ TensorFiber)
    (hpos : ∀ w ∈ K, 0 < w.1.2 w.2) :
    ∃ eps : ℝ, 0 < eps ∧ ∀ w ∈ K,
      ∀ w' : ((TensorFiber →L[ℝ] TensorFiber) × (TensorFiber →L[ℝ] ℝ)) × TensorFiber,
      ‖w'-w‖ < eps → w'.1.1.IsInvertible ∧ 0 < w'.1.2 (w'.1.1.inverse w'.2) := by
…

Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.TensorFiber