OAI/Analysis/TreePotential/SegmentPolar.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BoundedTreePotentials.Segments.atomTests line 14

    Source documentation

    The predual is the completion in the exact atom-testing norm.

    def atomTests : TestFamily Node where
…

    Mentions: OAI.BoundedTreePotentials.TestFamily, OAI.BoundedTreePotentials.Segments.Node

  2. def OAI.BoundedTreePotentials.Segments.unitTests line 28
  3. abbrev OAI.BoundedTreePotentials.Segments.Predual line 37
  4. abbrev OAI.BoundedTreePotentials.Segments.Dual line 38
  5. abbrev OAI.BoundedTreePotentials.Segments.DualCore line 42

    Source documentation

    The polar core is identified with the full continuous dual using block reflexivity and density.

    abbrev DualCore := TestCompletion unitTests

    Mentions: OAI.BoundedTreePotentials.TestCompletion, OAI.BoundedTreePotentials.Segments.unitTests

  6. lemma OAI.BoundedTreePotentials.Segments.finitePairing_profile line 44
  7. lemma OAI.BoundedTreePotentials.Segments.predual_test_bound line 70
  8. lemma OAI.BoundedTreePotentials.Segments.predual_unit_iff line 97
  9. def OAI.BoundedTreePotentials.Segments.segmentVector line 110
  10. lemma OAI.BoundedTreePotentials.Segments.segmentVector_apply line 112
  11. lemma OAI.BoundedTreePotentials.Segments.finitePairing_segmentVector line 116
  12. def OAI.BoundedTreePotentials.Segments.Atom.vector line 122
  13. lemma OAI.BoundedTreePotentials.Segments.Atom.vector_apply line 124
  14. lemma OAI.BoundedTreePotentials.Segments.Atom.finitePairing_vector line 127
  15. def OAI.BoundedTreePotentials.Segments.Atom.inCore line 131
  16. lemma OAI.BoundedTreePotentials.Segments.Atom.norm_inCore line 133
  17. lemma OAI.BoundedTreePotentials.Segments.Atom.zero_vector line 141
  18. lemma OAI.BoundedTreePotentials.Segments.Atom.zero_inCore line 142
  19. lemma OAI.BoundedTreePotentials.Segments.Atom.neg_vector line 143
  20. lemma OAI.BoundedTreePotentials.Segments.Atom.neg_inCore line 146
  21. lemma OAI.BoundedTreePotentials.Segments.Atom.coordinate_vector line 149
  22. def OAI.BoundedTreePotentials.Segments.Atom.oneSegment line 155
  23. lemma OAI.BoundedTreePotentials.Segments.Atom.oneSegment_vector line 164
  24. lemma OAI.BoundedTreePotentials.Segments.segmentVector_norm line 169
  25. lemma OAI.BoundedTreePotentials.Segments.unit_iff_pairing_atoms line 180

    Source documentation

    Normalizing the coefficients in an arbitrary family recovers the exact unit-test condition from its (absolute, or equivalently signed) atom bounds.

    lemma unit_iff_pairing_atoms (g : Node → ℝ) :
    IsUnitTest g ↔ ∀ A : Atom, |A.pairing g| ≤ 1 := by
…

    Mentions: OAI.BoundedTreePotentials.Segments.Node, OAI.BoundedTreePotentials.Segments.IsUnitTest, OAI.BoundedTreePotentials.Segments.Atom

  26. def OAI.BoundedTreePotentials.Segments.coreLift line 208
  27. def OAI.BoundedTreePotentials.Segments.functionalCoeffs line 211
  28. lemma OAI.BoundedTreePotentials.Segments.functional_coreLift line 213
  29. lemma OAI.BoundedTreePotentials.Segments.functional_atom line 223
  30. lemma OAI.BoundedTreePotentials.Segments.Atom.pairing_smul line 228
  31. lemma OAI.BoundedTreePotentials.Segments.functional_atom_bound line 236
  32. theorem OAI.BoundedTreePotentials.Segments.core_atom_hull line 271

    Source documentation

    The atom-hull fact is proved directly in the completed dual core by Hahn--Banach; no reflexivity or norm attainment is assumed here.

    theorem core_atom_hull : Metric.closedBall (0 : DualCore) 1 =
    closure (convexHull ℝ (Set.range Atom.inCore)) := by
…

    Mentions: OAI.BoundedTreePotentials.Segments.DualCore, OAI.BoundedTreePotentials.Segments.Atom.inCore