OAI/Analysis/TreePotential/StartComponent.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoundedTreePotentials.dualTransport line 16
2. lemma OAI.BoundedTreePotentials.dualTransport_apply line 19
3. lemma OAI.BoundedTreePotentials.dualTransport_bound line 22
4. lemma OAI.BoundedTreePotentials.dualTransportIsometry_norm line 33
5. def OAI.BoundedTreePotentials.dualTransportIsometry line 48
6. lemma OAI.BoundedTreePotentials.l2DualEquiv_symm_apply line 53
7. lemma OAI.BoundedTreePotentials.completedHilbertMap_upper line 60
8. abbrev OAI.BoundedTreePotentials.Segments.StartBlock line 73
9. def OAI.BoundedTreePotentials.Segments.startPiecesEquiv line 75
10. lemma OAI.BoundedTreePotentials.Segments.predualComponentEquiv_finite line 79
11. lemma OAI.BoundedTreePotentials.Segments.predualComponentEquiv_coordinate line 85
12. def OAI.BoundedTreePotentials.Segments.startBlockCoordinate line 92
13. lemma OAI.BoundedTreePotentials.Segments.startPiecesEquiv_apply line 95
14. lemma OAI.BoundedTreePotentials.Segments.startPieces_coordinate line 100
15. def OAI.BoundedTreePotentials.Segments.startBlockInclusion line 110
16. lemma OAI.BoundedTreePotentials.Segments.startPieces_inclusion line 114
17. lemma OAI.BoundedTreePotentials.Segments.startBlockInclusion_norm line 118
18. lemma OAI.BoundedTreePotentials.Segments.startBlockInclusion_coordinate line 122
19. lemma OAI.BoundedTreePotentials.Segments.startBlockInclusion_outside line 126
20. lemma OAI.BoundedTreePotentials.Segments.startBlock_reflexive line 133
21. theorem OAI.BoundedTreePotentials.Segments.start_outer_reflexive line 135
22. def OAI.BoundedTreePotentials.Segments.startBlockHilbertEquiv line 138
23. lemma OAI.BoundedTreePotentials.Segments.predualBlockHilbertEquiv_coordinate line 142
24. lemma OAI.BoundedTreePotentials.Segments.startBlockHilbertEquiv_coordinate line 154
25. lemma OAI.BoundedTreePotentials.Segments.predualBlockHilbert_bounds line 164
26. lemma OAI.BoundedTreePotentials.Segments.startBlockHilbert_bounds line 174
27. theorem OAI.BoundedTreePotentials.Segments.startBlock_norm_comparisons line 196

    Source documentation

    Finite-height comparisons on the actual component, whose coordinate norm equals the literal component infimum.

    theorem startBlock_norm_comparisons (n : ℕ) (x : StartBlock n) :
        ‖startBlockHilbertEquiv n x‖/(n+2) ≤ ‖x‖ ∧
          ‖x‖ ≤ Real.sqrt (n+2)*‖startBlockHilbertEquiv n x‖ := by
    …

    Mentions: OAI.BoundedTreePotentials.Segments.StartBlock, OAI.BoundedTreePotentials.Segments.startBlockHilbertEquiv

28. def OAI.BoundedTreePotentials.Segments.IsComponentArray line 214

    Source documentation

    Arrays on one labelled component, extended by zero to all other segments. This is exactly an array indexed by t≼v in that component.

    def IsComponentArray (n : ℕ) (a : Segment → ℝ) : Prop := ∀ S,S.start.1 ≠ n → a S=0

    Mentions: OAI.BoundedTreePotentials.Segments.Segment

29. def OAI.BoundedTreePotentials.Segments.componentArray line 216
30. lemma OAI.BoundedTreePotentials.Segments.componentArray_supported line 219
31. lemma OAI.BoundedTreePotentials.Segments.componentArray_eq_self line 223
32. lemma OAI.BoundedTreePotentials.Segments.componentArray_start line 230
33. lemma OAI.BoundedTreePotentials.Segments.eTwo_single line 249
34. def OAI.BoundedTreePotentials.Segments.componentRepresentationCost line 258

    Source documentation

    Literal cost M_{n+1} of the start masses on the component of height n+1.

    def componentRepresentationCost (n : ℕ) (a : Segment → ℝ) : ℝ≥0∞ :=
    …

    Mentions: OAI.BoundedTreePotentials.Segments.Segment

35. lemma OAI.BoundedTreePotentials.Segments.representationCost_componentArray line 261
36. lemma OAI.BoundedTreePotentials.Segments.representationCost_component_le line 283
37. lemma OAI.BoundedTreePotentials.Segments.componentCost_eq_forest line 292
38. lemma OAI.BoundedTreePotentials.Segments.representationOutput_component line 296
39. lemma OAI.BoundedTreePotentials.Segments.representationOutput_outside line 317
40. def OAI.BoundedTreePotentials.Segments.representedStart line 321
41. lemma OAI.BoundedTreePotentials.Segments.representedStart_coordinate line 324
42. lemma OAI.BoundedTreePotentials.Segments.representedStart_norm line 330
43. lemma OAI.BoundedTreePotentials.Segments.supported_representation_eq_block line 335
44. def OAI.BoundedTreePotentials.Segments.literalBlockStartNorm line 353

    Source documentation

    The infimum over precisely all countable segment representations on the specified component. The original recursive M_{n+1}, not a replacement, is used in the set of costs.

    def literalBlockStartNorm (n : ℕ) (z : BlockNode n → ℝ) : ℝ :=
    …

    Mentions: OAI.BoundedTreePotentials.Segments.BlockNode

45. lemma OAI.BoundedTreePotentials.Segments.exists_component_representation line 358
46. theorem OAI.BoundedTreePotentials.Segments.startBlock_norm_eq_infimum line 380
47. theorem OAI.BoundedTreePotentials.Segments.hilbert_coordinates_literal_norm line 404

    Source documentation

    A finite-height component is the full Hilbert coordinate set with the literal infimal norm.

    theorem hilbert_coordinates_literal_norm (n : ℕ) (z : CoordinateHilbert (BlockNode n)) :
        ‖(startBlockHilbertEquiv n).symm z‖=literalBlockStartNorm n z := by
    …

    Mentions: OAI.BoundedTreePotentials.CoordinateHilbert, OAI.BoundedTreePotentials.Segments.BlockNode, OAI.BoundedTreePotentials.Segments.startBlockHilbertEquiv, OAI.BoundedTreePotentials.Segments.literalBlockStartNorm

48. theorem OAI.BoundedTreePotentials.Segments.literalBlockStartNorm_comparisons line 412

    Source documentation

    Finite-height norm comparisons, with height n+1 and the root present.

    theorem literalBlockStartNorm_comparisons (n : ℕ) (z : CoordinateHilbert (BlockNode n)) :
        ‖z‖/(n+2) ≤ literalBlockStartNorm n z ∧ literalBlockStartNorm n z ≤ Real.sqrt (n+2)*‖z‖ := by
    …

    Mentions: OAI.BoundedTreePotentials.CoordinateHilbert, OAI.BoundedTreePotentials.Segments.BlockNode, OAI.BoundedTreePotentials.Segments.literalBlockStartNorm