OAI/Analysis/TreePotential/Clipping.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BoundedTreePotentials.BlockCalculus.extendCoeff line 15

    Source documentation

    Zero extension, including the root; longer path sums freeze at height n.

    def extendCoeff {n : ℕ} (f : TreeHilbert n) (s : Node) : ℝ :=
…

    Mentions: OAI.BoundedTreePotentials.TreeHilbert

  2. lemma OAI.BoundedTreePotentials.BlockCalculus.extendCoeff_apply line 18
  3. lemma OAI.BoundedTreePotentials.BlockCalculus.pathPotential_root line 21
  4. lemma OAI.BoundedTreePotentials.BlockCalculus.pathPotential_child line 29
  5. lemma OAI.BoundedTreePotentials.BlockCalculus.potential_extendCoeff line 35
  6. lemma OAI.BoundedTreePotentials.BlockCalculus.extendCoeff_potential_bound line 47
  7. def OAI.BoundedTreePotentials.BlockCalculus.dominatedHilbert line 60
  8. lemma OAI.BoundedTreePotentials.BlockCalculus.dominatedHilbert_norm_le line 64
  9. def OAI.BoundedTreePotentials.BlockCalculus.head line 71
  10. lemma OAI.BoundedTreePotentials.BlockCalculus.head_apply line 75
  11. lemma OAI.BoundedTreePotentials.BlockCalculus.head_norm_le line 78
  12. lemma OAI.BoundedTreePotentials.BlockCalculus.head_extendCoeff line 81
  13. lemma OAI.BoundedTreePotentials.BlockCalculus.head_pathBound_le line 86
  14. lemma OAI.BoundedTreePotentials.BlockCalculus.head_linearPolar_le line 93
  15. lemma OAI.BoundedTreePotentials.BlockCalculus.head_quadraticPolar_le line 97
  16. def OAI.BoundedTreePotentials.BlockCalculus.headLM line 104
  17. def OAI.BoundedTreePotentials.BlockCalculus.headCLM line 109
  18. lemma OAI.BoundedTreePotentials.BlockCalculus.head_inner line 112
  19. lemma OAI.BoundedTreePotentials.BlockCalculus.head_idem line 120
  20. lemma OAI.BoundedTreePotentials.BlockCalculus.head_eq_iff line 125
  21. lemma OAI.BoundedTreePotentials.BlockCalculus.extendCoeff_head_support line 134
  22. lemma OAI.BoundedTreePotentials.BlockCalculus.linearBlockCost_norming line 141
  23. lemma OAI.BoundedTreePotentials.BlockCalculus.head_linearCost_le line 148
  24. lemma OAI.BoundedTreePotentials.BlockCalculus.head_quadraticCost_le line 154
  25. def OAI.BoundedTreePotentials.BlockCalculus.inwardOne line 166

    Source documentation

    Coefficientwise clipping is done with the actual inward potentials, not an abstract substitute for a test or a changed cost.

    def inwardOne {n : ℕ} {D : Set Node} (hD : Initial D) (h g : TreeHilbert n)
    (hh : head D h = h) : TreeHilbert n :=
…

    Mentions: OAI.BoundedTreePotentials.TreeHilbert, OAI.BoundedTreePotentials.BlockCalculus.head

  26. def OAI.BoundedTreePotentials.BlockCalculus.inwardTwo line 172
  27. lemma OAI.BoundedTreePotentials.BlockCalculus.inward_difference line 178
  28. lemma OAI.BoundedTreePotentials.BlockCalculus.inwardOne_head line 186
  29. lemma OAI.BoundedTreePotentials.BlockCalculus.inwardTwo_head line 194
  30. lemma OAI.BoundedTreePotentials.BlockCalculus.inwardOne_norm line 202
  31. lemma OAI.BoundedTreePotentials.BlockCalculus.inwardTwo_norm line 204
  32. lemma OAI.BoundedTreePotentials.BlockCalculus.potential_congr_on_prefix line 207
  33. lemma OAI.BoundedTreePotentials.BlockCalculus.inwardOne_potential line 215
  34. lemma OAI.BoundedTreePotentials.BlockCalculus.inwardTwo_potential line 228
  35. lemma OAI.BoundedTreePotentials.BlockCalculus.head_orthogonal line 242
  36. lemma OAI.BoundedTreePotentials.BlockCalculus.disjoint_combination_norm_sq line 249
  37. structure OAI.BoundedTreePotentials.BlockCalculus.InwardPiece line 257

    Source documentation

    The information delivered by inward clipping, with unnormalized block budgets.

    structure InwardPiece {n : ℕ} (D : Set Node) (h g r : TreeHilbert n) : Prop where
…

    Mentions: OAI.BoundedTreePotentials.TreeHilbert

  38. lemma OAI.BoundedTreePotentials.BlockCalculus.inwardOne_piece line 263
  39. lemma OAI.BoundedTreePotentials.BlockCalculus.inwardTwo_piece line 274
  40. lemma OAI.BoundedTreePotentials.BlockCalculus.InwardPiece.hilbert_sq line 285
  41. lemma OAI.BoundedTreePotentials.BlockCalculus.InwardPiece.pathBound_le line 292
  42. lemma OAI.BoundedTreePotentials.BlockCalculus.InwardPiece.pathBound_sq line 297
  43. lemma OAI.BoundedTreePotentials.BlockCalculus.InwardPiece.linear_sq line 312
  44. lemma OAI.BoundedTreePotentials.BlockCalculus.InwardPiece.quadratic_sq line 335
  45. lemma OAI.BoundedTreePotentials.BlockCalculus.InwardPiece.linear_unit line 344
  46. lemma OAI.BoundedTreePotentials.BlockCalculus.InwardPiece.linear_budget line 367
  47. lemma OAI.BoundedTreePotentials.BlockCalculus.InwardPiece.quadratic_budget line 379
  48. lemma OAI.BoundedTreePotentials.BlockCalculus.quadratic_eval_le line 391
  49. lemma OAI.BoundedTreePotentials.BlockCalculus.inward_pair_identity line 397
  50. theorem OAI.BoundedTreePotentials.BlockCalculus.linear_paired line 420
  51. theorem OAI.BoundedTreePotentials.BlockCalculus.quadratic_paired line 438
  52. theorem OAI.BoundedTreePotentials.BlockCalculus.linear_paired_unit line 457

    Source documentation

    The stronger unit-budget version used for the bottom-up linear estimate.

    theorem linear_paired_unit {n : ℕ} {D : Set Node} (hD : Initial D) (x y : TreeHilbert n)
    (hx : head D x = x) {a b : ℝ} (ha : 0 ≤ a) (ha1 : a ≤ 1) (hb : 0 ≤ b)
    (hb1 : b ≤ 1/2) (hab : a^2+b^2 ≤ 1) :
    a*linearBlockCost n x+(b/2)*linearBlockCost n (y-head D y) ≤
      (linearBlockCost n (x+y)+linearBlockCost n (x-y))/2 := by
…

    Mentions: OAI.BoundedTreePotentials.TreeHilbert, OAI.BoundedTreePotentials.BlockCalculus.head, OAI.BoundedTreePotentials.linearBlockCost

  53. lemma OAI.BoundedTreePotentials.BlockCalculus.disk_sup_bound line 476
  54. lemma OAI.BoundedTreePotentials.BlockCalculus.ellipse_sup_bound line 493
  55. theorem OAI.BoundedTreePotentials.BlockCalculus.linear_midpoint_tail line 502
  56. theorem OAI.BoundedTreePotentials.BlockCalculus.quadratic_midpoint_tail line 514