OAI/Analysis/TreePotential/TestNorm.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.BoundedTreePotentials.TestFamily line 15

   Source documentation

   A coefficient test family, before imposing any particular tree budget.

   Also declared: ComparatorChallenges/BoundedTreePotentials.lean:17 (same declaration text).

   structure TestFamily (I : Type*) where
   …

2. instance OAI.BoundedTreePotentials.(instance at line 22) line 22
3. instance OAI.BoundedTreePotentials.(instance at line 23) line 23
4. def OAI.BoundedTreePotentials.finitePairing line 25

   Also declared: ComparatorChallenges/BoundedTreePotentials.lean:27 (same declaration text).

5. lemma OAI.BoundedTreePotentials.finitePairing_apply line 28
6. lemma OAI.BoundedTreePotentials.finitePairing_abs_bound line 31
7. def OAI.BoundedTreePotentials.testNorm line 43

   Also declared: ComparatorChallenges/BoundedTreePotentials.lean:30 (same declaration text).

8. lemma OAI.BoundedTreePotentials.testNorm_bddAbove line 46
9. lemma OAI.BoundedTreePotentials.finitePairing_le_testNorm line 50
10. lemma OAI.BoundedTreePotentials.testNorm_nonneg line 53
11. lemma OAI.BoundedTreePotentials.testNorm_le_l1 line 56
12. lemma OAI.BoundedTreePotentials.testNorm_zero line 61
13. lemma OAI.BoundedTreePotentials.testNorm_add_le line 66
14. lemma OAI.BoundedTreePotentials.testNorm_smul_le line 74
15. def OAI.BoundedTreePotentials.testSeminorm line 82

    Also declared: ComparatorChallenges/BoundedTreePotentials.lean:33 (same declaration text).

16. lemma OAI.BoundedTreePotentials.finitePairing_single_test line 126
17. lemma OAI.BoundedTreePotentials.coordinate_le_testNorm line 135
18. lemma OAI.BoundedTreePotentials.testNorm_eq_zero line 140
19. def OAI.BoundedTreePotentials.TestVector line 149

    Source documentation

    c00(I) with its actual test norm, not the ambient Finsupp topology.

    Also declared: ComparatorChallenges/BoundedTreePotentials.lean:77 (same declaration text).

    def TestVector (_ : TestFamily I) := I →₀ ℝ

    Mentions: OAI.BoundedTreePotentials.TestFamily

20. instance OAI.BoundedTreePotentials.(instance at line 151) line 151
21. instance OAI.BoundedTreePotentials.(instance at line 152) line 152
22. instance OAI.BoundedTreePotentials.(instance at line 153) line 153
23. theorem OAI.BoundedTreePotentials.testVectorCore line 155
24. instance OAI.BoundedTreePotentials.(instance at line 161) line 161
25. instance OAI.BoundedTreePotentials.(instance at line 203) line 203
26. lemma OAI.BoundedTreePotentials.norm_TestVector line 206
27. theorem OAI.BoundedTreePotentials.testNorm_signed_sup line 210

    Source documentation

    Symmetry identifies the signed-evaluation supremum with the absolute-pairing norm.

    theorem testNorm_signed_sup (K : TestFamily I) (x : I →₀ ℝ) :
        testNorm K x = ⨆ f : K, finitePairing f.val x := by
    …

    Mentions: OAI.BoundedTreePotentials.TestFamily, OAI.BoundedTreePotentials.testNorm, OAI.BoundedTreePotentials.finitePairing