OAI/Analysis/SeparableQuotients/ColorDecomposition.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SeparableQuotient.Norming.convex_sum_le_one line 10
2. lemma OAI.SeparableQuotient.Norming.absConvex_sum_le_one line 28
3. def OAI.SeparableQuotient.Norming.colorSet line 48
4. def OAI.SeparableQuotient.Norming.colorRestrict line 50
5. lemma OAI.SeparableQuotient.Norming.colorRestrict_eq line 53
6. lemma OAI.SeparableQuotient.Norming.mixed_color_unique line 57
7. lemma OAI.SeparableQuotient.Norming.colorRestrict_sum line 87
8. lemma OAI.SeparableQuotient.Norming.colorRestrict_sum_zero line 98
9. lemma OAI.SeparableQuotient.Norming.TypeI.color_decomposition line 104
10. lemma OAI.SeparableQuotient.Norming.FinitePath.color_decomposition line 125
11. lemma OAI.SeparableQuotient.Norming.TypeII.color_mem line 148
12. def OAI.SeparableQuotient.Norming.Crop.all line 216
13. lemma OAI.SeparableQuotient.Norming.Crop.all_set line 218
14. lemma OAI.SeparableQuotient.Norming.restrict_univ line 221
15. lemma OAI.SeparableQuotient.Norming.colorRestrict_all line 225
16. lemma OAI.SeparableQuotient.Norming.pure_color_restrict line 229
17. lemma OAI.SeparableQuotient.Norming.mixedBase_crop line 242
18. lemma OAI.SeparableQuotient.Norming.mixed_stage_crop line 252
19. lemma OAI.SeparableQuotient.Norming.mixed_stage_color_hull line 257
20. lemma OAI.SeparableQuotient.Norming.full_color_hull line 289

    Source documentation

    Every mixed-stage normer restricts to the absolute convex hull of the pure norming set.

    lemma full_color_hull (k : ℕ) (x : Array) (hx : x ∈ Full) :
        restrict (colorSet k) x ∈ absConvexHull ℚ (Pure k) := by
    …

    Mentions: OAI.SeparableQuotient.Norming.Array, OAI.SeparableQuotient.Norming.Full, OAI.SeparableQuotient.Norming.restrict, OAI.SeparableQuotient.Norming.colorSet, OAI.SeparableQuotient.Norming.Pure

21. lemma OAI.SeparableQuotient.LpFinite.absConvex_norm_array line 301
22. lemma OAI.SeparableQuotient.Norming.full_color_lp_bound line 329

    Source documentation

    Full mixed normers retain the exact pure ℓr bound on each color.

    lemma full_color_lp_bound (k : ℕ) (f : Array) (hf : f ∈ Full) :
        ‖array (Family.pure k).exponent (restrict (colorSet k) f)‖ ≤ 1 :=
    …

    Mentions: OAI.SeparableQuotient.Norming.Array, OAI.SeparableQuotient.Norming.Full, OAI.SeparableQuotient.Norming.restrict, OAI.SeparableQuotient.Norming.colorSet

23. def OAI.SeparableQuotient.LpFinite.realArray line 342

    Source documentation

    Real finitely supported vectors in the usual ℓp space.

    def realArray (p : ℝ≥0∞) (x : Γ →₀ ℝ) : lp (fun _ : Γ => ℝ) p :=
    …

24. lemma OAI.SeparableQuotient.LpFinite.realArray_apply line 345
25. lemma OAI.SeparableQuotient.LpFinite.pairing_le line 348
26. def OAI.SeparableQuotient.Norming.Family.primalExponent line 365
27. instance OAI.SeparableQuotient.Norming.Family.primalExponent_fact line 366
28. lemma OAI.SeparableQuotient.Norming.Family.primalExponent_toReal line 368
29. lemma OAI.SeparableQuotient.Norming.Family.conjugate line 370