OAI/Analysis/TreePotential/Inward.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BoundedTreePotentials.inwardOne line 14

    Source documentation

    The two different inward pieces; their difference is the original relative potential. The value at the inherited head c determines their direction.

    def inwardOne (c v : ℝ) : ℝ := if 0 ≤ c then min v 0 else max v 0
  2. def OAI.BoundedTreePotentials.inwardTwo line 15
  3. lemma OAI.BoundedTreePotentials.inwardOne_zero line 17
  4. lemma OAI.BoundedTreePotentials.inwardTwo_zero line 18
  5. lemma OAI.BoundedTreePotentials.inward_difference line 20
  6. lemma OAI.BoundedTreePotentials.inwardOne_abs_le line 26
  7. lemma OAI.BoundedTreePotentials.inwardTwo_abs_le line 36
  8. lemma OAI.BoundedTreePotentials.inwardOne_sub_le line 46
  9. lemma OAI.BoundedTreePotentials.inwardTwo_sub_le line 54
  10. lemma OAI.BoundedTreePotentials.inwardOne_same_sign line 62
  11. lemma OAI.BoundedTreePotentials.inwardTwo_same_sign line 64
  12. lemma OAI.BoundedTreePotentials.opposite_sum_bound line 67
  13. lemma OAI.BoundedTreePotentials.inwardOne_combination_bound line 95
  14. lemma OAI.BoundedTreePotentials.inwardTwo_combination_bound line 103
  15. lemma OAI.BoundedTreePotentials.combined_quadratic_budget line 111
  16. abbrev OAI.BoundedTreePotentials.TreeCalculus.Node line 128

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

  17. def OAI.BoundedTreePotentials.TreeCalculus.potential line 131

    Source documentation

    The root-inclusive scalar prefix sum. Rootless rows will set f([])=0.

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

    def potential (f : Node → ℝ) (s : Node) : ℝ := (s.inits.map f).sum

    Mentions: OAI.BoundedTreePotentials.TreeCalculus.Node

  18. lemma OAI.BoundedTreePotentials.TreeCalculus.potential_root line 133
  19. lemma OAI.BoundedTreePotentials.TreeCalculus.potential_child line 135
  20. lemma OAI.BoundedTreePotentials.TreeCalculus.potential_add line 139
  21. lemma OAI.BoundedTreePotentials.TreeCalculus.potential_smul line 143
  22. lemma OAI.BoundedTreePotentials.TreeCalculus.potential_sub line 149
  23. def OAI.BoundedTreePotentials.TreeCalculus.increments line 156

    Source documentation

    Discrete derivative with dummy parent value zero above the root.

    def increments (P : Node → ℝ) (s : Node) : ℝ :=
…

    Mentions: OAI.BoundedTreePotentials.TreeCalculus.Node

  24. lemma OAI.BoundedTreePotentials.TreeCalculus.increments_root line 159
  25. lemma OAI.BoundedTreePotentials.TreeCalculus.increments_child line 160
  26. theorem OAI.BoundedTreePotentials.TreeCalculus.potential_increments line 163
  27. theorem OAI.BoundedTreePotentials.TreeCalculus.increments_potential line 169
  28. def OAI.BoundedTreePotentials.TreeCalculus.Initial line 176

    Source documentation

    Head sets are predecessor-closed. The empty set is allowed for block heads.

    def Initial (D : Set Node) : Prop := ∀ ⦃s r⦄, s ∈ D → r <+: s → r ∈ D

    Mentions: OAI.BoundedTreePotentials.TreeCalculus.Node

  29. def OAI.BoundedTreePotentials.TreeCalculus.headPart line 178
  30. def OAI.BoundedTreePotentials.TreeCalculus.tailPart line 180
  31. lemma OAI.BoundedTreePotentials.TreeCalculus.potential_tail_on_head line 182
  32. lemma OAI.BoundedTreePotentials.TreeCalculus.potential_head_child line 190
  33. lemma OAI.BoundedTreePotentials.TreeCalculus.potential_head_on_head line 196
  34. lemma OAI.BoundedTreePotentials.TreeCalculus.head_potential_bound line 205
  35. lemma OAI.BoundedTreePotentials.TreeCalculus.tail_eq_sub_head line 219
  36. lemma OAI.BoundedTreePotentials.TreeCalculus.tail_potential_bound line 224
  37. def OAI.BoundedTreePotentials.TreeCalculus.inwardPotentialOne line 230
  38. def OAI.BoundedTreePotentials.TreeCalculus.inwardPotentialTwo line 232
  39. def OAI.BoundedTreePotentials.TreeCalculus.inwardCoeffsOne line 234
  40. def OAI.BoundedTreePotentials.TreeCalculus.inwardCoeffsTwo line 235
  41. lemma OAI.BoundedTreePotentials.TreeCalculus.inwardCoeffsOne_on_head line 237
  42. lemma OAI.BoundedTreePotentials.TreeCalculus.inwardCoeffsTwo_on_head line 246
  43. lemma OAI.BoundedTreePotentials.TreeCalculus.inwardCoeffs_difference line 255
  44. lemma OAI.BoundedTreePotentials.TreeCalculus.inwardCoeffsOne_abs_le line 268
  45. lemma OAI.BoundedTreePotentials.TreeCalculus.inwardCoeffsTwo_abs_le line 286