OAI/Analysis/TreePotential/Completion.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BoundedTreePotentials.testVectorEquiv line 14
  2. lemma OAI.BoundedTreePotentials.norm_testVector_equiv line 18
  3. lemma OAI.BoundedTreePotentials.norm_test_single line 21
  4. def OAI.BoundedTreePotentials.finiteTestFunctional line 29
  5. lemma OAI.BoundedTreePotentials.finiteTestFunctional_apply line 34
  6. lemma OAI.BoundedTreePotentials.finiteTestFunctional_norm_le line 37
  7. abbrev OAI.BoundedTreePotentials.TestCompletion line 44

    Source documentation

    The completion used in the test-space constructions.

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

    abbrev TestCompletion (K : TestFamily I) := UniformSpace.Completion (TestVector K)

    Mentions: OAI.BoundedTreePotentials.TestFamily, OAI.BoundedTreePotentials.TestVector

  8. def OAI.BoundedTreePotentials.completedTestFunctional line 46
  9. lemma OAI.BoundedTreePotentials.completedTestFunctional_coe line 49
  10. lemma OAI.BoundedTreePotentials.completedTestFunctional_norm_le line 54
  11. lemma OAI.BoundedTreePotentials.completedTestFunctional_abs_le line 63
  12. lemma OAI.BoundedTreePotentials.exists_completed_test_near_norm line 70

    Source documentation

    Extended tests really remain norming; this is established, not postulated as an extra hypothesis on the completion.

    lemma exists_completed_test_near_norm (K : TestFamily I) (x : TestCompletion K)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ f : K, ‖x‖ - ε < completedTestFunctional K f x := by
…

    Mentions: OAI.BoundedTreePotentials.TestFamily, OAI.BoundedTreePotentials.TestCompletion, OAI.BoundedTreePotentials.completedTestFunctional

  13. theorem OAI.BoundedTreePotentials.completed_tests_norming line 92