OAI/Analysis/SeparableQuotients/PrefixNormers.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SeparableQuotient.PrefixNormers line 18

    Source documentation

    Finite prefix normers for a zero-based sequence. The existential formulation is equivalent to a maximum over the finite set.

    structure PrefixNormers (f : ā„• ā†’ StrongDual š•œ X) where
ā€¦
  2. theorem OAI.SeparableQuotient.PrefixNormers.prefix_evaluation line 29
  3. theorem OAI.SeparableQuotient.PrefixNormers.prefix_bound line 41
  4. theorem OAI.SeparableQuotient.PrefixNormers.term_bound line 54
  5. theorem OAI.SeparableQuotient.PrefixNormers.coefficient_bound line 64
  6. theorem OAI.SeparableQuotient.PrefixNormers.finsupp_coefficient_bound line 75
  7. theorem OAI.SeparableQuotient.PrefixNormers.linearIndependent line 90
  8. def OAI.SeparableQuotient.PrefixNormers.spanCoord line 100

    Source documentation

    Bounded algebraic coordinate functionals.

    noncomputable def spanCoord (a : ā„) (ha : 0 < a) (hf : āˆ€ n, a ā‰¤ ā€–f nā€–) (n : ā„•) :
    StrongDual š•œ (Submodule.span š•œ (Set.range f)) :=
ā€¦
  9. theorem OAI.SeparableQuotient.PrefixNormers.spanCoord_norm line 109
  10. theorem OAI.SeparableQuotient.PrefixNormers.spanCoord_basis line 114
  11. theorem OAI.SeparableQuotient.PrefixNormers.exists_ambientCoord line 122

    Source documentation

    Hahn--Banach extension of each coordinate; restrictions to the closed span are canonical.

    theorem exists_ambientCoord (a : ā„) (ha : 0 < a) (hf : āˆ€ n, a ā‰¤ ā€–f nā€–) :
    āˆƒ e : ā„• ā†’ StrongDual š•œ (StrongDual š•œ X),
      (āˆ€ n, ā€–e nā€– ā‰¤ 4 / a) āˆ§ (āˆ€ n, āˆ€ x : Submodule.span š•œ (Set.range f),
        e n x = H.spanCoord a ha hf n x) := by
ā€¦
  12. lemma OAI.SeparableQuotient.PrefixNormers.linearCombination_eq_sum_range line 132
  13. def OAI.SeparableQuotient.PrefixNormers.closedSpan line 142

    Source documentation

    The closed linear span of the sequence.

    def closedSpan (f : ā„• ā†’ StrongDual š•œ X) : Submodule š•œ (StrongDual š•œ X) :=
ā€¦
  14. def OAI.SeparableQuotient.PrefixNormers.ambientCoord line 145
  15. lemma OAI.SeparableQuotient.PrefixNormers.ambientCoord_spec line 149
  16. def OAI.SeparableQuotient.PrefixNormers.ambientPrefix line 155
  17. lemma OAI.SeparableQuotient.PrefixNormers.ambientPrefix_apply_span line 159
  18. lemma OAI.SeparableQuotient.PrefixNormers.ambientPrefix_bound_span line 167
  19. lemma OAI.SeparableQuotient.PrefixNormers.ambientPrefix_bound line 183
  20. lemma OAI.SeparableQuotient.PrefixNormers.ambientPrefix_eventually_span line 192
  21. lemma OAI.SeparableQuotient.PrefixNormers.ambientPrefix_tendsto line 202
  22. def OAI.SeparableQuotient.PrefixNormers.basisVector line 227
  23. def OAI.SeparableQuotient.PrefixNormers.coord line 230
  24. lemma OAI.SeparableQuotient.PrefixNormers.coord_norm line 234
  25. lemma OAI.SeparableQuotient.PrefixNormers.coord_basis line 241
  26. def OAI.SeparableQuotient.PrefixNormers.prefixOp line 247
  27. lemma OAI.SeparableQuotient.PrefixNormers.prefix_coe line 251
  28. lemma OAI.SeparableQuotient.PrefixNormers.prefix_norm line 256
  29. lemma OAI.SeparableQuotient.PrefixNormers.prefix_tendsto line 264
  30. def OAI.SeparableQuotient.PrefixNormers.schauderBasis line 271

    Source documentation

    Finite prefix normers yield a basic sequence.

    noncomputable def schauderBasis (a : ā„) (ha : 0 < a) (hf : āˆ€ n, a ā‰¤ ā€–f nā€–) :
    SchauderBasis š•œ (closedSpan f) where
ā€¦

    Mentions: OAI.SeparableQuotient.PrefixNormers.closedSpan

  31. def OAI.SeparableQuotient.PrefixNormers.evaluation line 294

    Source documentation

    Evaluation on the closed span G.

    noncomputable def evaluation (f : ā„• ā†’ StrongDual š•œ X) :
    X ā†’L[š•œ] StrongDual š•œ (closedSpan f) :=
ā€¦

    Mentions: OAI.SeparableQuotient.PrefixNormers.closedSpan

  32. lemma OAI.SeparableQuotient.PrefixNormers.evaluation_apply line 300
  33. lemma OAI.SeparableQuotient.PrefixNormers.ambientCoord_basis line 303
  34. lemma OAI.SeparableQuotient.PrefixNormers.evaluation_normer line 307
  35. def OAI.SeparableQuotient.PrefixNormers.adjointVector line 330

    Source documentation

    The coefficient vectors used in the adjoint bound.

    noncomputable def adjointVector (a : ā„) (ha : 0 < a) (hf : āˆ€ n, a ā‰¤ ā€–f nā€–)
    (h : StrongDual š•œ (StrongDual š•œ (closedSpan f))) (m : ā„•) : closedSpan f :=
ā€¦

    Mentions: OAI.SeparableQuotient.PrefixNormers.closedSpan

  36. lemma OAI.SeparableQuotient.PrefixNormers.adjointVector_bound line 334
  37. lemma OAI.SeparableQuotient.PrefixNormers.coord_adjointVector line 356
  38. lemma OAI.SeparableQuotient.PrefixNormers.linearCombination_adjointVector line 363
  39. def OAI.SeparableQuotient.PrefixNormers.coefficientSpan line 377

    Source documentation

    The closed coefficient span Z.

    noncomputable def coefficientSpan (a : ā„) (ha : 0 < a) (hf : āˆ€ n, a ā‰¤ ā€–f nā€–) :
    Submodule š•œ (StrongDual š•œ (closedSpan f)) :=
ā€¦

    Mentions: OAI.SeparableQuotient.PrefixNormers.closedSpan

  40. lemma OAI.SeparableQuotient.PrefixNormers.adjoint_bound_on_coefficientSpan line 381
  41. def OAI.SeparableQuotient.PrefixNormers.evaluationToZ line 400

    Source documentation

    Evaluation with codomain the closed coefficient span.

    noncomputable def evaluationToZ (a : ā„) (ha : 0 < a) (hf : āˆ€ n, a ā‰¤ ā€–f nā€–)
    (hZ : āˆ€ x, evaluation f x āˆˆ H.coefficientSpan a ha hf) :
    X ā†’L[š•œ] H.coefficientSpan a ha hf :=
ā€¦

    Mentions: OAI.SeparableQuotient.PrefixNormers.evaluation

  42. lemma OAI.SeparableQuotient.PrefixNormers.evaluationToZ_adjoint_bound line 405
  43. lemma OAI.SeparableQuotient.PrefixNormers.coord_linearIndependent line 421

    Source documentation

    Coefficients are linearly independent, so their closed span is infinite dimensional.

    lemma coord_linearIndependent (a : ā„) (ha : 0 < a) (hf : āˆ€ n, a ā‰¤ ā€–f nā€–) :
    LinearIndependent š•œ (H.coord a ha hf) := by
ā€¦
  44. def OAI.SeparableQuotient.PrefixNormers.coefficientVector line 429
  45. lemma OAI.SeparableQuotient.PrefixNormers.coefficientVector_linearIndependent line 434
  46. lemma OAI.SeparableQuotient.PrefixNormers.coefficientSpan_infiniteDimensional line 439
  47. lemma OAI.SeparableQuotient.PrefixNormers.coefficientSpan_isClosed line 446
  48. lemma OAI.SeparableQuotient.PrefixNormers.coefficientSpan_separable line 450
  49. theorem OAI.SeparableQuotient.PrefixNormers.evaluationToZ_surjective line 474

    Source documentation

    The adjoint lower bound implies surjectivity of evaluation.

    theorem evaluationToZ_surjective (a : ā„) (ha : 0 < a) (hf : āˆ€ n, a ā‰¤ ā€–f nā€–)
    (hZ : āˆ€ x, evaluation f x āˆˆ H.coefficientSpan a ha hf) :
    Function.Surjective (H.evaluationToZ a ha hf hZ) :=
ā€¦

    Mentions: OAI.SeparableQuotient.PrefixNormers.evaluation

  50. theorem OAI.SeparableQuotient.PrefixNormers.hasSeparableQuotient_of_range line 482

    Source documentation

    Finite prefix normers yield a separable quotient.

    theorem hasSeparableQuotient_of_range (a : ā„) (ha : 0 < a) (hf : āˆ€ n, a ā‰¤ ā€–f nā€–)
    (hZ : āˆ€ x, evaluation f x āˆˆ H.coefficientSpan a ha hf) : HasSeparableQuotient š•œ X := by
ā€¦

    Mentions: OAI.SeparableQuotient.PrefixNormers.evaluation, OAI.SeparableQuotient.HasSeparableQuotient