OAI/Analysis/SeparableQuotients/CoordinateDual.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.includeFinite_injective line 12
  2. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.generator_independent line 16
  3. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.infiniteDimensional line 21
  4. def OAI.SeparableQuotient.NormConstruction.NormingSet.predual line 30

    Source documentation

    The coordinate predual.

    def predual : Submodule ℝ (StrongDual ℝ K.Space) :=
…
  5. instance OAI.SeparableQuotient.NormConstruction.NormingSet.predual_isClosed line 33
  6. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.coordinate_mem_predual line 36
  7. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.functional_mem_predual line 39
  8. def OAI.SeparableQuotient.NormConstruction.NormingSet.evaluation line 50

    Source documentation

    Canonical evaluation into the dual of the coordinate span.

    def evaluation : K.Space →L[ℝ] StrongDual ℝ K.predual :=
…
  9. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.evaluation_apply line 54
  10. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.norm_evaluation line 57
  11. def OAI.SeparableQuotient.NormConstruction.NormingSet.evaluationIsometry line 73
  12. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.projection_norm_apply_le line 85
  13. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.tendsto_projection line 92

    Source documentation

    Strong convergence of uniformly contractive coordinate crops whose sets eventually contain every coordinate.

    lemma tendsto_projection {ι : Type*} {l : Filter ι} (A : ι → Set Γ)
    (hA : ∀ i, K.CropStable (A i)) (hcover : ∀ a, ∀ᶠ i in l, a ∈ A i) (x : K.Space) :
    Tendsto (fun i => K.projection (A i) (hA i) x) l (𝓝 x) := by
…
  14. def OAI.SeparableQuotient.NormConstruction.NormingSet.predualCoordinate line 134

    Source documentation

    The coordinate functional regarded as an element of the actual predual.

    def predualCoordinate (a : Γ) : K.predual := ⟨K.coordinate a, K.coordinate_mem_predual a⟩
  15. def OAI.SeparableQuotient.NormConstruction.NormingSet.rationalPredual line 136
  16. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.rationalPredual_val line 139
  17. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.rationalPredual_eq_functional line 147
  18. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.norm_rationalPredual_le line 151
  19. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.rationalPredual_single line 157
  20. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.rationalPredual_apply line 161
  21. lemma OAI.SeparableQuotient.NormConstruction.absConvex_abs_le line 172
  22. def OAI.SeparableQuotient.NormConstruction.NormingSet.evaluateArray line 207

    Source documentation

    Evaluation of any rational array, not only chosen normers.

    def evaluateArray (x : K.Space) : (Γ →₀ ℚ) →ₗ[ℚ] ℝ where
…
  23. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.evaluateArray_eq line 212
  24. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.evaluateArray_eq_functional line 216
  25. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.norm_le_of_evaluateArray line 221
  26. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.evaluateArray_filter_of_zero line 236
  27. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.evaluateArray_projection line 247