OAI/Analysis/DiamondDistortion/Incomparable.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DiamondDistortion.IncomparableModel.Incomparable line 19

   Source documentation

   Every node of one admissible segment is incomparable with every node of another. This is strictly more restrictive than disjointness.

   def Incomparable (F : forestSegments.Family) : Prop :=
   …

2. def OAI.DiamondDistortion.IncomparableModel.Family line 22
3. instance OAI.DiamondDistortion.IncomparableModel.(instance at line 23) line 23
4. lemma OAI.DiamondDistortion.IncomparableModel.families_bddAbove line 28
5. def OAI.DiamondDistortion.IncomparableModel.primalSeminorm line 33

   Source documentation

   The exact incomparable-segment primal norm, not its disjoint-segment analogue.

   def primalSeminorm : Seminorm ℝ (ForestNode →₀ ℝ) := ⨆ F : Family,F.val.seminorm

   Mentions: OAI.DiamondDistortion.ForestNode, OAI.DiamondDistortion.IncomparableModel.Family

6. lemma OAI.DiamondDistortion.IncomparableModel.test_le_primal line 34
7. lemma OAI.DiamondDistortion.IncomparableModel.primal_le_disjoint line 39
8. def OAI.DiamondDistortion.IncomparableModel.singletonFamily line 42
9. lemma OAI.DiamondDistortion.IncomparableModel.coordinate_le_primal line 47
10. def OAI.DiamondDistortion.IncomparableModel.primalData line 53
11. abbrev OAI.DiamondDistortion.IncomparableModel.PrimalSpace line 56
12. abbrev OAI.DiamondDistortion.IncomparableModel.Space line 58

    Source documentation

    The full Banach dual of the incomparable-segment primal completion.

    abbrev Space := StrongDual ℝ PrimalSpace

    Mentions: OAI.DiamondDistortion.IncomparableModel.PrimalSpace

13. lemma OAI.DiamondDistortion.IncomparableModel.family_energy line 60
14. lemma OAI.DiamondDistortion.IncomparableModel.primal_sq_le line 65
15. def OAI.DiamondDistortion.IncomparableModel.familyOfFintype line 81
16. lemma OAI.DiamondDistortion.IncomparableModel.test_energy line 92
17. lemma OAI.DiamondDistortion.IncomparableModel.block_square line 100
18. lemma OAI.DiamondDistortion.IncomparableModel.block_filter line 124
19. lemma OAI.DiamondDistortion.IncomparableModel.singleton_test line 147
20. lemma OAI.DiamondDistortion.IncomparableModel.local_lower line 170
21. lemma OAI.DiamondDistortion.IncomparableModel.blocks line 183
22. def OAI.DiamondDistortion.IncomparableModel.Head line 192
23. def OAI.DiamondDistortion.IncomparableModel.heads line 194
24. theorem OAI.DiamondDistortion.IncomparableModel.graph line 203