QuotientPerturbation.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SeparableQuotient.quotient_lift line 17

Source documentation

A quotient lift with norm bounded by 11/10 times the quotient norm.

theorem quotient_lift (Y : Submodule 𝕜 M) [IsClosed (Y : Set M)] (w : M ⧸ Y) :
    ∃ y : M, Y.mkQL y = w ∧ ‖y‖ ≤ (11 / 10 : ℝ) * ‖w‖ := by
…

def OAI.SeparableQuotient.quotientRightInverse line 27
def OAI.SeparableQuotient.liftConstant line 36
Source documentation
Quantitative lift constant for a perturbed quotient map.
```
noncomputable def liftConstant (b : ℝ) : ℝ := (11 / 10) / (1 - (11 / 10) * b)
```
theorem OAI.SeparableQuotient.liftConstant_properties line 38

theorem OAI.SeparableQuotient.perturbed_quotient_lift line 54

Source documentation

A 1/10 perturbation of a quotient map is onto, with a quantitative nonlinear lift bound.

theorem perturbed_quotient_lift [CompleteSpace M]
    (Y : Submodule 𝕜 M) [IsClosed (Y : Set M)]
    (B : M →L[𝕜] M ⧸ Y) (hB : ‖B‖ ≤ 1 / 10) (w : M ⧸ Y) :
    ∃ y : M, (Y.mkQL - B) y = w ∧ ‖y‖ ≤ liftConstant ‖B‖ * ‖w‖ := by
…

Mentions: OAI.SeparableQuotient.liftConstant

theorem OAI.SeparableQuotient.perturbed_quotient_dense line 79

Source documentation

The image of the perturbed kernel is dense in the closure of the image of the original kernel.

theorem perturbed_quotient_dense [CompleteSpace M]
    (Y : Submodule 𝕜 M) [IsClosed (Y : Set M)]
    (B : M →L[𝕜] M ⧸ Y) (hB : ‖B‖ ≤ 1 / 10)
    (hBV : ∀ y : M, B y ∈ (Y.map B.toLinearMap).topologicalClosure) :
    ((Y.mkQL - B).ker.map B.toLinearMap).topologicalClosure =
      (Y.map B.toLinearMap).topologicalClosure := by
…

def OAI.SeparableQuotient.equivOfBijective line 147
def OAI.SeparableQuotient.evalOn line 164
Source documentation
Restriction of the canonical evaluation embedding to a subspace of the dual.
```
noncomputable def evalOn (Y : Submodule 𝕜 (StrongDual 𝕜 E)) :
    E →L[𝕜] StrongDual 𝕜 Y :=
…
```
theorem OAI.SeparableQuotient.evalOn_apply line 168

theorem OAI.SeparableQuotient.twisted_eval_surjective line 173

Source documentation

Surjectivity from the adjoint-range hypothesis and Hahn–Banach, using a quotient lift of the graph map.

theorem twisted_eval_surjective
    (Y : Submodule 𝕜 (StrongDual 𝕜 E)) [IsClosed (Y : Set (StrongDual 𝕜 E))]
    (hY : Function.Surjective (evalOn Y))
    (B : StrongDual 𝕜 E →L[𝕜] (StrongDual 𝕜 E) ⧸ Y)
    (hBadj : ∀ w : StrongDual 𝕜 ((StrongDual 𝕜 E) ⧸ Y),
      ∃ e : E, w.comp B = NormedSpace.inclusionInDoubleDual 𝕜 E e) :
    Function.Surjective (evalOn (Y.mkQL - B).ker) := by
…

Mentions: OAI.SeparableQuotient.evalOn

theorem OAI.SeparableQuotient.twisted_eval_injective line 206

Source documentation

The small quotient perturbation preserves injectivity of evaluation.

theorem twisted_eval_injective
    (Y : Submodule 𝕜 (StrongDual 𝕜 E)) [IsClosed (Y : Set (StrongDual 𝕜 E))]
    (hY : Isometry (evalOn Y))
    (B : StrongDual 𝕜 E →L[𝕜] (StrongDual 𝕜 E) ⧸ Y) (hB : ‖B‖ ≤ 1 / 10) :
    Function.Injective (evalOn (Y.mkQL - B).ker) := by
…

Mentions: OAI.SeparableQuotient.evalOn

def OAI.SeparableQuotient.twisted_eval_equiv line 244

theorem OAI.SeparableQuotient.twist line 259

Source documentation

A small perturbation of a quotient map produces an isomorphic dual of the perturbed kernel.

theorem twist [CompleteSpace E]
    (Y : Submodule 𝕜 (StrongDual 𝕜 E)) [IsClosed (Y : Set (StrongDual 𝕜 E))]
    (hYiso : Isometry (evalOn Y)) (hYsurj : Function.Surjective (evalOn Y))
    (B : StrongDual 𝕜 E →L[𝕜] (StrongDual 𝕜 E) ⧸ Y) (hB : ‖B‖ ≤ 1 / 10)
    (hBadj : ∀ w : StrongDual 𝕜 ((StrongDual 𝕜 E) ⧸ Y),
      ∃ e : E, w.comp B = NormedSpace.inclusionInDoubleDual 𝕜 E e)
    (hBrange : B.range ≤ (Y.map B.toLinearMap).topologicalClosure) :
    CompleteSpace (Y.mkQL - B).ker ∧
      (∃ T : E ≃L[𝕜] StrongDual 𝕜 (Y.mkQL - B).ker,
        ∀ (e : E) (x : (Y.mkQL - B).ker), T e x = (x : StrongDual 𝕜 E) e) ∧
      (((Y.mkQL - B).ker).map B.toLinearMap).topologicalClosure =
        (Y.map B.toLinearMap).topologicalClosure := by
…

Mentions: OAI.SeparableQuotient.evalOn