OAI/Analysis/TreePotential/StartPolar.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Start-cost polar identification.

  1. lemma OAI.BoundedTreePotentials.Segments.enn_sqrt_sq line 13
  2. lemma OAI.BoundedTreePotentials.Segments.enn_sq_sqrt line 17
  3. lemma OAI.BoundedTreePotentials.Segments.startCost_finset_sum line 21
  4. lemma OAI.BoundedTreePotentials.Segments.treeSum_fintype_sum line 29
  5. def OAI.BoundedTreePotentials.Segments.layerMass line 33
  6. def OAI.BoundedTreePotentials.Segments.layerNorm line 36
  7. lemma OAI.BoundedTreePotentials.Segments.layerMass_antichain line 39
  8. lemma OAI.BoundedTreePotentials.Segments.layerCost_eq_norm line 45
  9. lemma OAI.BoundedTreePotentials.Segments.sum_layers line 48
  10. lemma OAI.BoundedTreePotentials.Segments.sum_layerNorm_sq line 58
  11. lemma OAI.BoundedTreePotentials.Segments.startCost_le_sum_layers line 73

    Source documentation

    Exact level estimate on countably branching trees, allowing either side to be infinite.

    lemma startCost_le_sum_layers (n : ℕ) (m : List ℕ → ℝ≥0∞) :
    startCost n m≤∑ d : Fin (n+1),layerNorm n d m := by
…

    Mentions: OAI.BoundedTreePotentials.Segments.startCost, OAI.BoundedTreePotentials.Segments.layerNorm

  12. lemma OAI.BoundedTreePotentials.Segments.sum_layers_le_hilbert line 83
  13. lemma OAI.BoundedTreePotentials.Segments.startCost_hilbert_comparisons line 90
  14. def OAI.BoundedTreePotentials.Segments.ConeFamily line 111

    Source documentation

    Finite incomparable tests wholly contained in a specified descendant cone. The component index, prefix, root and endpoint conventions are unchanged.

    def ConeFamily (n : ℕ) (s : List ℕ) :=
…
  15. instance OAI.BoundedTreePotentials.Segments.coneFamilyNonempty line 114
  16. def OAI.BoundedTreePotentials.Segments.coneEnergy line 119

    Source documentation

    Squared local polar budget. Supremums in ENNReal avoid any assumption of an optimizing antichain or endpoint.

    def coneEnergy (g : Node → ℝ) (n : ℕ) (s : List ℕ) : ℝ≥0∞ :=
…

    Mentions: OAI.BoundedTreePotentials.Segments.Node

  17. def OAI.BoundedTreePotentials.Segments.coneBudget line 122
  18. lemma OAI.BoundedTreePotentials.Segments.coneBudget_sq line 125
  19. lemma OAI.BoundedTreePotentials.Segments.branch_index_eq line 130
  20. lemma OAI.BoundedTreePotentials.Segments.cone_children_union line 137
  21. lemma OAI.BoundedTreePotentials.Segments.coneEnergy_children line 161
  22. lemma OAI.BoundedTreePotentials.Segments.coneBudget_children line 173
  23. lemma OAI.BoundedTreePotentials.Segments.coneBudget_potential line 179
  24. lemma OAI.BoundedTreePotentials.Segments.coneEnergy_roots line 189
  25. lemma OAI.BoundedTreePotentials.Segments.coneBudget_roots line 210
  26. lemma OAI.BoundedTreePotentials.Segments.segment_le_coneBudget line 217
  27. lemma OAI.BoundedTreePotentials.Segments.forest_pair_budget_le line 234

    Source documentation

    The polar estimate for an arbitrary nonnegative start array, allowing infinite costs. Its local budgets were obtained from actual incomparable tests.

    lemma forest_pair_budget_le (m : (n : ℕ) → List ℕ → ℝ≥0∞)
    (g : Node → ℝ) (hg : IsUnitTest g) :
    (∑' n : ℕ,treeSum (n+1) (fun s => m n s*coneBudget g n s)) ≤ forestCost m := by
…

    Mentions: OAI.BoundedTreePotentials.Segments.Node, OAI.BoundedTreePotentials.Segments.IsUnitTest, OAI.BoundedTreePotentials.Segments.treeSum, OAI.BoundedTreePotentials.Segments.coneBudget, OAI.BoundedTreePotentials.Segments.forestCost