OAI/Analysis/TreePotential/FreeRoot.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.BoundedTreePotentials.FreeRoot.IsFreePotential line 16

   Source documentation

   Free scalar labels: the first field includes the root, but the second field only tests genuine child increments. No root label is set equal to zero.

   structure IsFreePotential (b : Node → ℝ) : Prop where
   …

2. lemma OAI.BoundedTreePotentials.FreeRoot.isFreePotential_iff line 20
3. def OAI.BoundedTreePotentials.FreeRoot.includeEdge line 28
4. lemma OAI.BoundedTreePotentials.FreeRoot.includeEdge_apply line 32
5. lemma OAI.BoundedTreePotentials.FreeRoot.includeEdge_child line 35
6. def OAI.BoundedTreePotentials.FreeRoot.freeTestFamily line 40

   Source documentation

   The defining free-root norm uses only genuine edges. It is a restriction of the rooted-sibling test family, NOT the anchored rootless sibling family.

   def freeTestFamily : TestFamily (TreeCoordinate false) :=
   …

   Mentions: OAI.BoundedTreePotentials.TestFamily

7. theorem OAI.BoundedTreePotentials.FreeRoot.mem_freeTestFamily_iff line 45

   Source documentation

   The free-root test and norm correspondence retains the existence of a free root value.

   theorem mem_freeTestFamily_iff (f : TreeCoordinate false → ℝ) :
       f ∈ freeTestFamily.carrier ↔ ∃ b : Node → ℝ, IsFreePotential b ∧
         ∀ s : TreeCoordinate false, f s = b s.val - b s.val.dropLast := by
   …

   Mentions: OAI.BoundedTreePotentials.FreeRoot.IsFreePotential

8. abbrev OAI.BoundedTreePotentials.FreeRoot.Space line 70
9. def OAI.BoundedTreePotentials.FreeRoot.rootedInclusion line 72
10. lemma OAI.BoundedTreePotentials.FreeRoot.rootedInclusion_norm line 75
11. lemma OAI.BoundedTreePotentials.FreeRoot.rootedInclusion_vector line 78
12. theorem OAI.BoundedTreePotentials.FreeRoot.freeRoot_stronger_modulus line 86

    Source documentation

    The edge space embeds isometrically as the root-coordinate-zero subspace of the rooted sibling model. The inherited estimate implies the free-root bound.

    theorem freeRoot_stronger_modulus {t : ℝ} (ht : 0 < t) (ht1 : t < 1) :
        ((Real.sqrt (1+t^2/4)-1 : ℝ) : EReal) ≤ averagedModulus Space t := by
    …

    Mentions: OAI.BoundedTreePotentials.averagedModulus, OAI.BoundedTreePotentials.FreeRoot.Space

13. lemma OAI.BoundedTreePotentials.FreeRoot.distinct_bound_le_common line 92
14. theorem OAI.BoundedTreePotentials.FreeRoot.freeRoot_averaged_modulus line 101
15. lemma OAI.BoundedTreePotentials.FreeRoot.rootless_restricted_potential line 105
16. def OAI.BoundedTreePotentials.FreeRoot.path line 118
17. lemma OAI.BoundedTreePotentials.FreeRoot.norm_path_bounds line 121
18. lemma OAI.BoundedTreePotentials.FreeRoot.path_child_sub line 136
19. lemma OAI.BoundedTreePotentials.FreeRoot.free_sibling_hilbert_upper line 142
20. lemma OAI.BoundedTreePotentials.FreeRoot.free_siblings_weaklyNull line 149
21. def OAI.BoundedTreePotentials.FreeRoot.boundedTree line 153
22. lemma OAI.BoundedTreePotentials.FreeRoot.boundedTree_difference line 155
23. theorem OAI.BoundedTreePotentials.FreeRoot.freeRoot_renorming_obstruction line 161
24. theorem OAI.BoundedTreePotentials.FreeRoot.freeRoot_no_equivalent_AUC line 182