OAI/Analysis/SeparableQuotients/PathOperators.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SeparableQuotient.Norming.Family.pathExponent line 10
  2. lemma OAI.SeparableQuotient.Norming.Family.q_gt_one line 11
  3. lemma OAI.SeparableQuotient.Norming.Family.q_pos line 12
  4. instance OAI.SeparableQuotient.Norming.Family.pathExponent_fact line 13
  5. lemma OAI.SeparableQuotient.Norming.Family.pathExponent_real line 15
  6. lemma OAI.SeparableQuotient.Norming.Family.pathExponent_pos line 17
  7. lemma OAI.SeparableQuotient.Norming.Family.pathExponent_ne_top line 18
  8. abbrev OAI.SeparableQuotient.ActualSpace.W line 26
  9. def OAI.SeparableQuotient.ActualSpace.pathCoset line 31
  10. lemma OAI.SeparableQuotient.ActualSpace.coset_sum_bound line 33
  11. def OAI.SeparableQuotient.ActualSpace.finitePathMap line 46
  12. lemma OAI.SeparableQuotient.ActualSpace.finitePathMap_bound line 49
  13. def OAI.SeparableQuotient.ActualSpace.pathMap line 65

    Source documentation

    A bounded path map constructed by completion of path cosets.

    def pathMap (f : Family) : lp (fun _ : PathIndex f => ℝ) f.pathExponent →L[ℝ] W :=
…

    Mentions: OAI.SeparableQuotient.ActualSpace.W

  14. lemma OAI.SeparableQuotient.ActualSpace.norm_pathMap_le line 68
  15. lemma OAI.SeparableQuotient.ActualSpace.pathMap_finite line 74
  16. lemma OAI.SeparableQuotient.ActualSpace.pathMap_single line 81
  17. lemma OAI.SeparableQuotient.Norming.rawPath_card_le line 92
  18. lemma OAI.SeparableQuotient.Norming.pathIndex_card_le line 111
  19. def OAI.SeparableQuotient.Norming.pathLabelBase line 115
  20. def OAI.SeparableQuotient.Norming.Family.index line 118
  21. lemma OAI.SeparableQuotient.Norming.Family.index_injective line 122
  22. def OAI.SeparableQuotient.Norming.Family.sourceColor line 126
  23. def OAI.SeparableQuotient.Norming.pathLabel line 131

    Source documentation

    An inner color partitions the shared C₁ while retaining the outer color.

    def pathLabel (hCH : Cardinal.mk ℝ = Cardinal.aleph 1) (f : Family) (P : PathIndex f) : Γ :=
…

    Mentions: OAI.SeparableQuotient.Norming.Family, OAI.SeparableQuotient.Norming.PathIndex, OAI.SeparableQuotient.Norming.Γ

  24. lemma OAI.SeparableQuotient.Norming.pathLabel_color line 134
  25. lemma OAI.SeparableQuotient.Norming.pathLabel_injective line 138
  26. def OAI.SeparableQuotient.Norming.Family.sourceExponent line 157
  27. instance OAI.SeparableQuotient.Norming.Family.sourceExponent_fact line 158
  28. lemma OAI.SeparableQuotient.Norming.Family.sourceExponent_real line 160
  29. lemma OAI.SeparableQuotient.Norming.Family.sourceExponent_ne_top line 164
  30. lemma OAI.SeparableQuotient.Norming.Family.pathConjugate line 165
  31. def OAI.SeparableQuotient.Norming.pathLabelEmb line 169
  32. def OAI.SeparableQuotient.ActualSpace.finiteLabelMap line 182
  33. lemma OAI.SeparableQuotient.ActualSpace.finiteLabelMap_eq line 185
  34. lemma OAI.SeparableQuotient.ActualSpace.finiteLabelMap_bound line 190
  35. def OAI.SeparableQuotient.ActualSpace.labelMap line 207

    Source documentation

    The color synthesis operator.

    def labelMap (f : Family) : lp (fun _ : PathIndex f => ℝ) f.sourceExponent →L[ℝ] E :=
…

    Mentions: OAI.SeparableQuotient.ActualSpace.E

  36. lemma OAI.SeparableQuotient.ActualSpace.norm_labelMap_le line 210
  37. lemma OAI.SeparableQuotient.ActualSpace.labelMap_finite line 216
  38. lemma OAI.SeparableQuotient.ActualSpace.labelMap_single line 223