OAI/Analysis/TreePotential/TreeTests.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.BoundedTreePotentials.TreeCalculus.QuadraticKind line 13

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

  2. def OAI.BoundedTreePotentials.TreeCalculus.QuadraticGroup line 19

    Source documentation

    Exactly the coordinate groups used by the three distinct quadratic budgets. Quantifying over finite subsets is equivalent to the countable-sum convention.

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

    def QuadraticGroup : QuadraticKind → Finset Node → Prop
  | .sibling, B => ∃ r, ∀ s ∈ B, ∃ j, s = r ++ [j]
  | .antichain, B => (B : Set Node).Pairwise (fun s t => ¬s <+: t ∧ ¬t <+: s)
  | .global, _ => True

    Mentions: OAI.BoundedTreePotentials.TreeCalculus.QuadraticKind, OAI.BoundedTreePotentials.TreeCalculus.Node

  3. def OAI.BoundedTreePotentials.TreeCalculus.QuadraticBudget line 24

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

  4. def OAI.BoundedTreePotentials.TreeCalculus.CoefficientSupport line 29

    Source documentation

    The antichain model really requires finite support, and the global model really requires square summability. Neither condition is discarded.

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

    def CoefficientSupport : QuadraticKind → (Node → ℝ) → Prop
  | .sibling, _ => True
  | .antichain, f => (Function.support f).Finite
  | .global, f => Memℓp f 2

    Mentions: OAI.BoundedTreePotentials.TreeCalculus.QuadraticKind, OAI.BoundedTreePotentials.TreeCalculus.Node

  5. structure OAI.BoundedTreePotentials.TreeCalculus.IsTreeTest line 34

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

  6. lemma OAI.BoundedTreePotentials.TreeCalculus.quadratic_singleton line 40
  7. lemma OAI.BoundedTreePotentials.TreeCalculus.test_coefficient_bound line 54
  8. lemma OAI.BoundedTreePotentials.TreeCalculus.quadraticBudget_dominate line 61
  9. lemma OAI.BoundedTreePotentials.TreeCalculus.coefficientSupport_dominate line 69
  10. lemma OAI.BoundedTreePotentials.TreeCalculus.coefficientSupport_combine line 85
  11. lemma OAI.BoundedTreePotentials.TreeCalculus.zero_isTreeTest line 100
  12. lemma OAI.BoundedTreePotentials.TreeCalculus.neg_isTreeTest line 112
  13. lemma OAI.BoundedTreePotentials.TreeCalculus.inits_nodup line 123
  14. lemma OAI.BoundedTreePotentials.TreeCalculus.potential_single line 136
  15. lemma OAI.BoundedTreePotentials.TreeCalculus.single_isTreeTest line 146
  16. abbrev OAI.BoundedTreePotentials.TreeCalculus.TreeCoordinate line 169

    Source documentation

    Coordinate type: the root is omitted only in the rootless sibling row.

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

    abbrev TreeCoordinate (includeRoot : Bool) := {s : Node // includeRoot = true ∨ s ≠ []}

    Mentions: OAI.BoundedTreePotentials.TreeCalculus.Node

  17. def OAI.BoundedTreePotentials.TreeCalculus.liftCoefficients line 171

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

  18. lemma OAI.BoundedTreePotentials.TreeCalculus.liftCoefficients_coord line 174
  19. lemma OAI.BoundedTreePotentials.TreeCalculus.liftCoefficients_zero line 177
  20. lemma OAI.BoundedTreePotentials.TreeCalculus.liftCoefficients_neg line 180
  21. lemma OAI.BoundedTreePotentials.TreeCalculus.liftCoefficients_single line 185
  22. def OAI.BoundedTreePotentials.TreeCalculus.treeTestFamily line 195

    Source documentation

    The four rows are specializations of this construction, not identified norms.

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

    def treeTestFamily (r : Bool) (k : QuadraticKind) : TestFamily (TreeCoordinate r) := by
…

    Mentions: OAI.BoundedTreePotentials.TreeCalculus.QuadraticKind, OAI.BoundedTreePotentials.TestFamily, OAI.BoundedTreePotentials.TreeCalculus.TreeCoordinate

  23. abbrev OAI.BoundedTreePotentials.TreeCalculus.rootlessSiblingTests line 342
  24. abbrev OAI.BoundedTreePotentials.TreeCalculus.rootedSiblingTests line 343
  25. abbrev OAI.BoundedTreePotentials.TreeCalculus.antichainTests line 344
  26. abbrev OAI.BoundedTreePotentials.TreeCalculus.globalTests line 345
  27. abbrev OAI.BoundedTreePotentials.TreeCalculus.RootlessSiblingSpace line 347
  28. abbrev OAI.BoundedTreePotentials.TreeCalculus.RootedSiblingSpace line 348
  29. abbrev OAI.BoundedTreePotentials.TreeCalculus.AntichainSpace line 349
  30. abbrev OAI.BoundedTreePotentials.TreeCalculus.GlobalTestSpace line 350
  31. lemma OAI.BoundedTreePotentials.TreeCalculus.headPart_abs_le line 353
  32. lemma OAI.BoundedTreePotentials.TreeCalculus.head_isTreeTest line 356
  33. lemma OAI.BoundedTreePotentials.TreeCalculus.lift_restrict line 365
  34. def OAI.BoundedTreePotentials.TreeCalculus.asTreeTest line 375
  35. lemma OAI.BoundedTreePotentials.TreeCalculus.inwardOne_isTreeTest line 379
  36. lemma OAI.BoundedTreePotentials.TreeCalculus.inwardTwo_isTreeTest line 408
  37. def OAI.BoundedTreePotentials.TreeCalculus.treePairing line 439
  38. lemma OAI.BoundedTreePotentials.TreeCalculus.treePairing_lift line 442
  39. lemma OAI.BoundedTreePotentials.TreeCalculus.treePairing_add_coeff line 449
  40. lemma OAI.BoundedTreePotentials.TreeCalculus.treePairing_sub_coeff line 453
  41. lemma OAI.BoundedTreePotentials.TreeCalculus.treePairing_smul_coeff line 457
  42. lemma OAI.BoundedTreePotentials.TreeCalculus.treePairing_congr line 465
  43. lemma OAI.BoundedTreePotentials.TreeCalculus.treePairing_zero_of_disjoint line 472
  44. lemma OAI.BoundedTreePotentials.TreeCalculus.treePairing_le_norm line 479
  45. lemma OAI.BoundedTreePotentials.TreeCalculus.treePairing_head_eq line 484
  46. lemma OAI.BoundedTreePotentials.TreeCalculus.treePairing_tail_eq line 490
  47. lemma OAI.BoundedTreePotentials.TreeCalculus.inward_pairing_identity line 497
  48. theorem OAI.BoundedTreePotentials.TreeCalculus.paired_finite_test_bound line 524

    Source documentation

    The finite-array form of the paired inward inequality. The proof takes suprema instead of presuming an attained infinite-dimensional polar norm.

    theorem paired_finite_test_bound {r : Bool} {k : QuadraticKind} {D : Set Node}
    (hD : Initial D) (hroot : [] ∈ D)
    (x y : TreeCoordinate r →₀ ℝ)
    (hx : ∀ s, x s ≠ 0 → s.val ∈ D) (hy : ∀ s, s.val ∈ D → y s = 0)
    {a θ t : ℝ} (ha : 0 ≤ a) (ha1 : a ≤ 1) (hθ : 0 ≤ θ) (hθ1 : θ ≤ 1/2)
    (hsquare : a^2 + θ^2 ≤ 1)
    (f g : treeTestFamily r k) :
    a * finitePairing f.val x + (t * θ / 2) * finitePairing g.val y ≤
      (testNorm (treeTestFamily r k) (x + t • y) + testNorm (treeTestFamily r k) (x - t • y)) / 2 := by
…

    Mentions: OAI.BoundedTreePotentials.TreeCalculus.QuadraticKind, OAI.BoundedTreePotentials.TreeCalculus.Node, OAI.BoundedTreePotentials.TreeCalculus.Initial, OAI.BoundedTreePotentials.TreeCalculus.TreeCoordinate, OAI.BoundedTreePotentials.TreeCalculus.treeTestFamily, OAI.BoundedTreePotentials.finitePairing, OAI.BoundedTreePotentials.testNorm

  49. lemma OAI.BoundedTreePotentials.testNorm_weighted_sup line 550
  50. theorem OAI.BoundedTreePotentials.TreeCalculus.paired_finite_inequality line 571