OAI/Analysis/TreePotential/TreeObstruction.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoundedTreePotentials.TreeCalculus.nodeArray line 13
2. def OAI.BoundedTreePotentials.TreeCalculus.pathArray line 16
3. lemma OAI.BoundedTreePotentials.TreeCalculus.finitePairing_nodeArray line 19
4. lemma OAI.BoundedTreePotentials.TreeCalculus.finitePairing_pathArray line 25
5. lemma OAI.BoundedTreePotentials.TreeCalculus.pathArray_child line 30
6. lemma OAI.BoundedTreePotentials.TreeCalculus.pathArray_apply line 34
7. lemma OAI.BoundedTreePotentials.TreeCalculus.testNorm_pathArray_le line 46
8. lemma OAI.BoundedTreePotentials.TreeCalculus.testNorm_pathArray line 53
9. def OAI.BoundedTreePotentials.TreeCalculus.treePath line 59
10. lemma OAI.BoundedTreePotentials.TreeCalculus.norm_treePath line 62
11. def OAI.BoundedTreePotentials.TreeCalculus.childCoordinate line 68
12. lemma OAI.BoundedTreePotentials.TreeCalculus.treePath_child_sub line 71
13. lemma OAI.BoundedTreePotentials.TreeCalculus.childNode_injective line 79
14. lemma OAI.BoundedTreePotentials.TreeCalculus.sibling_quadraticGroup line 83
15. lemma OAI.BoundedTreePotentials.TreeCalculus.sibling_sq_sum_le line 104
16. lemma OAI.BoundedTreePotentials.TreeCalculus.completedTestFunctional_vector line 112
17. theorem OAI.BoundedTreePotentials.TreeCalculus.sibling_hilbert_upper line 119

    Source documentation

    Siblings have the asserted Hilbert upper estimate in each different model.

    theorem sibling_hilbert_upper (r : Bool) (k : QuadraticKind) (s : Node)
        (A : Finset ℕ) (a : ℕ → ℝ) :
        ‖∑ n ∈ A, a n • coordinateVector (treeTestFamily r k) (childCoordinate r s n)‖ ≤
          Real.sqrt (∑ n ∈ A, (a n)^2) := by
    …

    Mentions: OAI.BoundedTreePotentials.TreeCalculus.QuadraticKind, OAI.BoundedTreePotentials.TreeCalculus.Node, OAI.BoundedTreePotentials.coordinateVector, OAI.BoundedTreePotentials.TreeCalculus.treeTestFamily, OAI.BoundedTreePotentials.TreeCalculus.childCoordinate

18. lemma OAI.BoundedTreePotentials.TreeCalculus.siblings_weaklyNull line 134
19. def OAI.BoundedTreePotentials.TreeCalculus.fourBoundedTree line 140

    Source documentation

    Shift by the fixed nonroot vertex [0], so the rootless row also starts at a nonzero path. No root coefficient is inserted in that row.

    def fourBoundedTree (r : Bool) (k : QuadraticKind) (h : ℕ) (s : Tree h) :
        TestCompletion (treeTestFamily r k) := treePath r k ([0] ++ s.val)

    Mentions: OAI.BoundedTreePotentials.TreeCalculus.QuadraticKind, OAI.BoundedTreePotentials.Tree, OAI.BoundedTreePotentials.TestCompletion, OAI.BoundedTreePotentials.TreeCalculus.treeTestFamily, OAI.BoundedTreePotentials.TreeCalculus.treePath

20. lemma OAI.BoundedTreePotentials.TreeCalculus.fourBoundedTree_norm line 143
21. lemma OAI.BoundedTreePotentials.TreeCalculus.fourBoundedTree_difference line 147
22. theorem OAI.BoundedTreePotentials.TreeCalculus.four_renorming_obstruction line 157

    Source documentation

    Exact zero radius for every equivalent norm represented on a continuous-linearly-equivalent real normed space.

    theorem four_renorming_obstruction (r : Bool) (k : QuadraticKind)
        {Y : Type*} [NormedAddCommGroup Y] [NormedSpace ℝ Y]
        (e : TestCompletion (treeTestFamily r k) ≃L[ℝ] Y) {α β : ℝ}
        (hα : 0 < α) (hαβ : α ≤ β)
        (he : ∀ x, α * ‖x‖ ≤ ‖e x‖ ∧ ‖e x‖ ≤ β * ‖x‖) :
        oneSidedModulus Y (α / (2 * β)) = 0 := by
    …

    Mentions: OAI.BoundedTreePotentials.TreeCalculus.QuadraticKind, OAI.BoundedTreePotentials.TestCompletion, OAI.BoundedTreePotentials.TreeCalculus.treeTestFamily, OAI.BoundedTreePotentials.oneSidedModulus

23. lemma OAI.BoundedTreePotentials.continuousEquiv_bounds line 184
24. theorem OAI.BoundedTreePotentials.TreeCalculus.four_no_equivalent_AUC line 211
25. def OAI.BoundedTreePotentials.restrictedTestFamily line 229

    Source documentation

    Restrict coefficient tests to an injected coordinate set, without imposing any condition on the omitted coefficients.

    def restrictedTestFamily (K : TestFamily I) (ι : J ↪ I) : TestFamily J where
    …

    Mentions: OAI.BoundedTreePotentials.TestFamily

26. lemma OAI.BoundedTreePotentials.finitePairing_embDomain line 244
27. lemma OAI.BoundedTreePotentials.testNorm_restricted line 248
28. def OAI.BoundedTreePotentials.restrictedVectorInclusion line 260
29. def OAI.BoundedTreePotentials.restrictedCompletionInclusion line 270
30. lemma OAI.BoundedTreePotentials.restrictedCompletionInclusion_coe line 275
31. lemma OAI.BoundedTreePotentials.restrictedCompletionInclusion_norm line 282
32. lemma OAI.BoundedTreePotentials.restrictedCompletionInclusion_vector line 291
33. def OAI.BoundedTreePotentials.pullbackFiniteCodim line 305
34. lemma OAI.BoundedTreePotentials.mem_pullbackFiniteCodim line 313
35. lemma OAI.BoundedTreePotentials.averaged_tail_bound_pullback line 318