OAI/Analysis/SeparableQuotients/NormCompletion.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SeparableQuotient.NormConstruction.NormingSet line 14
  2. abbrev OAI.SeparableQuotient.NormConstruction.NormingSet.BoundedSpace line 21
  3. def OAI.SeparableQuotient.NormConstruction.NormingSet.coordinateVector line 23
  4. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.coordinateVector_apply line 28
  5. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.norm_coordinateVector_le line 31
  6. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.norm_coordinateVector line 34
  7. def OAI.SeparableQuotient.NormConstruction.NormingSet.finiteMap line 40

    Source documentation

    Algebraic inclusion of the prescribed finitely supported vectors.

    def finiteMap : (Γ →₀ ℝ) →ₗ[ℝ] K.BoundedSpace :=
…
  8. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.finiteMap_single line 43
  9. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.finiteMap_apply line 47
  10. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.finiteMap_coordinate line 53
  11. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.finiteMap_injective line 59
  12. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.norm_finiteMap_le_l1 line 65
  13. def OAI.SeparableQuotient.NormConstruction.NormingSet.closedSpan line 76

    Source documentation

    The concrete Banach completion. Its norm is literally the supremum of absolute evaluations over K.

    def closedSpan : Submodule ℝ K.BoundedSpace := K.finiteMap.range.topologicalClosure
  14. abbrev OAI.SeparableQuotient.NormConstruction.NormingSet.Space line 77
  15. instance OAI.SeparableQuotient.NormConstruction.NormingSet.(instance at line 79) line 79
  16. def OAI.SeparableQuotient.NormConstruction.NormingSet.includeFinite line 84
  17. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.includeFinite_val line 88
  18. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.denseRange_includeFinite line 91
  19. def OAI.SeparableQuotient.NormConstruction.NormingSet.functional line 99
  20. def OAI.SeparableQuotient.NormConstruction.NormingSet.coordinate line 102
  21. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.functional_includeFinite line 105
  22. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.coordinate_includeFinite line 109
  23. def OAI.SeparableQuotient.NormConstruction.NormingSet.generator line 112
  24. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.norm_generator line 114
  25. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.functional_bound line 118
  26. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.norm_functional_le line 121
  27. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.coordinate_bound line 126
  28. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.norm_eq_sup line 129
  29. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.approximating_sequence line 132
  30. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.support_countable line 140

    Source documentation

    Every completed vector has countable coordinate support.

    lemma support_countable (x : K.Space) : Set.Countable {a | K.coordinate a x ≠ 0} := by
…
  31. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.functional_eq_sum line 159

    Source documentation

    Every norming functional is its finite coordinate combination even after completion; hence no nonzero completed vector can vanish at every coordinate.

    lemma functional_eq_sum (f : K.carrier) :
    K.functional f = ∑ a ∈ f.val.support, (f.val a : ℝ) • K.coordinate a := by
…
  32. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.coordinates_separate line 185
  33. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.coordinate_ext line 193
  34. def OAI.SeparableQuotient.NormConstruction.NormingSet.CropStable line 209

    Source documentation

    Stability of a norming set under the specified coordinate crop.

    def CropStable (A : Set Γ) : Prop := ∀ f ∈ K.carrier, f.filter (· ∈ A) ∈ K.carrier
…
  35. def OAI.SeparableQuotient.NormConstruction.NormingSet.cropNormer line 213
  36. def OAI.SeparableQuotient.NormConstruction.NormingSet.cropAmbient line 215
  37. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.cropAmbient_apply line 227
  38. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.cropAmbient_finiteMap line 230
  39. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.cropAmbient_mem line 240
  40. def OAI.SeparableQuotient.NormConstruction.NormingSet.projection line 250

    Source documentation

    Contractive interval/rectangle projection on the actual Banach completion.

    def projection : K.Space →L[ℝ] K.Space :=
…
  41. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.norm_projection_le line 254
  42. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.projection_includeFinite line 263
  43. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.coordinate_projection line 267
  44. lemma OAI.SeparableQuotient.NormConstruction.NormingSet.projection_idempotent line 279