OAI/Analysis/TreePotential/Moduli.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.BoundedTreePotentials.ClosedFiniteCodim line 15

   Source documentation

   Closed finite-codimensional subspaces for asymptotic moduli.

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

   structure ClosedFiniteCodim where
   …

2. def OAI.BoundedTreePotentials.averagedModulus line 23

   Source documentation

   We take these infima and suprema in the extended reals, so their definitions are meaningful without tacit boundedness side conditions. On infinite dimensional normed spaces their values at positive radii are finite.

   def averagedModulus (t : ℝ) : EReal :=
   …

3. def OAI.BoundedTreePotentials.oneSidedModulus line 28
4. def OAI.BoundedTreePotentials.IsAUC line 33
5. lemma OAI.BoundedTreePotentials.ereal_le_of_forall_pos_sub_le line 37
6. lemma OAI.BoundedTreePotentials.averagedModulus_lower_bound line 45
7. lemma OAI.BoundedTreePotentials.midpoint_center_perturbation line 61
8. lemma OAI.BoundedTreePotentials.optimal_pair_parameters line 73
9. def OAI.BoundedTreePotentials.testVectorBasis line 99
10. instance OAI.BoundedTreePotentials.testVector_separable line 102
11. lemma OAI.BoundedTreePotentials.coordinates_linearlyIndependent line 108
12. lemma OAI.BoundedTreePotentials.testCompletion_infiniteDimensional line 115
13. instance OAI.BoundedTreePotentials.TreeCalculus.treeCoordinate_infinite line 127
14. theorem OAI.BoundedTreePotentials.TreeCalculus.four_completed_tail_bound line 133

    Source documentation

    Uniform quantitative tail estimate at every unit center, including centers in the completion. The finite codimensional space may depend on ε.

    theorem four_completed_tail_bound {r : Bool} {k : QuadraticKind}
        {t : ℝ} (ht : 0 < t) (ht1 : t < 1)
        (x : TestCompletion (treeTestFamily r k)) (hx : ‖x‖ = 1)
        {ε : ℝ} (hε : 0 < ε) :
        ∃ F : ClosedFiniteCodim (TestCompletion (treeTestFamily r k)),
          ∀ y, y ∈ F.space → 1 ≤ ‖y‖ →
          Real.sqrt (1 + t^2/4) - 1 - ε ≤ (‖x + t • y‖ + ‖x - t • y‖) / 2 - 1 := by
    …

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

15. theorem OAI.BoundedTreePotentials.TreeCalculus.four_averaged_modulus line 165

    Source documentation

    The common lower bound, with each root convention and quadratic budget kept distinct.

    theorem four_averaged_modulus (r : Bool) (k : QuadraticKind)
        {t : ℝ} (ht : 0 < t) (ht1 : t < 1) :
        ((Real.sqrt (1 + t^2/4) - 1 : ℝ) : EReal) ≤
          averagedModulus (TestCompletion (treeTestFamily r k)) t := by
    …

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