OAI/Analysis/TreePotential/TailEstimates.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BoundedTreePotentials.lp_hasSum_sq line 14
  2. lemma OAI.BoundedTreePotentials.lp_midpoint_sq line 19
  3. structure OAI.BoundedTreePotentials.FiniteOuterHead line 44

    Source documentation

    A finite ancestral subset of the disjoint union of the finite-height trees.

    structure FiniteOuterHead where
…
  4. def OAI.BoundedTreePotentials.CostHeads.linearHead line 54
  5. lemma OAI.BoundedTreePotentials.CostHeads.linearHead_equiv line 61
  6. lemma OAI.BoundedTreePotentials.CostHeads.linearHead_norm line 64
  7. def OAI.BoundedTreePotentials.CostHeads.linearOuterHead line 70
  8. lemma OAI.BoundedTreePotentials.CostHeads.linearOuterHead_apply line 74
  9. lemma OAI.BoundedTreePotentials.CostHeads.linearOuterHead_contract line 78
  10. lemma OAI.BoundedTreePotentials.CostHeads.linearOuterHead_idem line 84
  11. lemma OAI.BoundedTreePotentials.CostHeads.linearOuterTail_bound line 91
  12. theorem OAI.BoundedTreePotentials.CostHeads.linearOuter_midpoint_sq line 96

    Source documentation

    Paired estimates permit arbitrary old-head motion in the displacement.

    theorem linearOuter_midpoint_sq (D : ℕ → Set Node) (hD : ∀ n, Initial (D n))
    (x y : LinearOuter) (hx : linearOuterHead D hD x = x) :
    ‖x‖^2+‖y-linearOuterHead D hD y‖^2/16 ≤ ((‖x+y‖+‖x-y‖)/2)^2 := by
…

    Mentions: OAI.BoundedTreePotentials.LinearOuter, OAI.BoundedTreePotentials.CostHeads.linearOuterHead

  13. theorem OAI.BoundedTreePotentials.CostHeads.linearOuter_midpoint line 112
  14. theorem OAI.BoundedTreePotentials.CostHeads.linearOuter_tail_four line 118
  15. def OAI.BoundedTreePotentials.CostHeads.quadraticHead line 130
  16. lemma OAI.BoundedTreePotentials.CostHeads.quadraticHead_equiv line 137
  17. lemma OAI.BoundedTreePotentials.CostHeads.quadraticHead_norm line 140
  18. def OAI.BoundedTreePotentials.CostHeads.quadraticOuterHead line 146
  19. lemma OAI.BoundedTreePotentials.CostHeads.quadraticOuterHead_apply line 150
  20. lemma OAI.BoundedTreePotentials.CostHeads.quadraticOuterHead_contract line 154
  21. lemma OAI.BoundedTreePotentials.CostHeads.quadraticOuterHead_idem line 160
  22. lemma OAI.BoundedTreePotentials.CostHeads.quadraticOuterTail_bound line 167
  23. theorem OAI.BoundedTreePotentials.CostHeads.quadraticOuter_midpoint_sq line 172

    Source documentation

    Paired estimates permit arbitrary old-head motion in the displacement.

    theorem quadraticOuter_midpoint_sq (D : ℕ → Set Node) (hD : ∀ n, Initial (D n))
    (x y : QuadraticOuter) (hx : quadraticOuterHead D hD x = x) :
    ‖x‖^2+‖y-quadraticOuterHead D hD y‖^2/16 ≤ ((‖x+y‖+‖x-y‖)/2)^2 := by
…

    Mentions: OAI.BoundedTreePotentials.QuadraticOuter, OAI.BoundedTreePotentials.CostHeads.quadraticOuterHead

  24. theorem OAI.BoundedTreePotentials.CostHeads.quadraticOuter_midpoint line 188
  25. theorem OAI.BoundedTreePotentials.CostHeads.quadraticOuter_tail_four line 194
  26. theorem OAI.BoundedTreePotentials.CostHeads.quadratic_tail_seven line 208

    Source documentation

    The coefficient-seven tail bound without a head-zero hypothesis on displacement. The inward inequality gives the stronger coefficient four.

    theorem quadratic_tail_seven (A : FiniteOuterHead) (x y : QuadraticOuter)
    (hx : quadraticOuterHead A.nodes A.initial x = x) {R : ℝ} (hR : 0 ≤ R)
    (hp : ‖x+y‖ ≤ R) (hm : ‖x-y‖ ≤ R) :
    ‖y-quadraticOuterHead A.nodes A.initial y‖ ≤ 7*Real.sqrt (R^2-‖x‖^2) := by
…

    Mentions: OAI.BoundedTreePotentials.FiniteOuterHead, OAI.BoundedTreePotentials.QuadraticOuter, OAI.BoundedTreePotentials.CostHeads.quadraticOuterHead

  27. theorem OAI.BoundedTreePotentials.CostHeads.quadratic_tail_eight line 215
  28. lemma OAI.BoundedTreePotentials.norm_displacement_le_avg line 227
  29. lemma OAI.BoundedTreePotentials.norm_center_le_avg line 234
  30. lemma OAI.BoundedTreePotentials.scalar_avg_sq_le line 241
  31. lemma OAI.BoundedTreePotentials.scalar_midpoint_energy line 248
  32. lemma OAI.BoundedTreePotentials.scalar_clipping_family line 253
  33. lemma OAI.BoundedTreePotentials.scalar_positive_scaled line 266
  34. theorem OAI.BoundedTreePotentials.CostHeads.linear_head_tail_clipping line 286
  35. theorem OAI.BoundedTreePotentials.CostHeads.linear_fresh_energy_sixteen line 298
  36. theorem OAI.BoundedTreePotentials.CostHeads.linear_fresh_layer_400 line 304
  37. theorem OAI.BoundedTreePotentials.CostHeads.linear_trimming_242 line 314
  38. theorem OAI.BoundedTreePotentials.CostHeads.linear_positive_outer line 322
  39. theorem OAI.BoundedTreePotentials.CostHeads.quadratic_symmetric_twelve line 332
  40. theorem OAI.BoundedTreePotentials.CostHeads.quadratic_tail_nine line 340
  41. lemma OAI.BoundedTreePotentials.BlockCalculus.linear_block_midpoint_sq line 352
  42. theorem OAI.BoundedTreePotentials.BlockCalculus.linear_positive_scaled line 361
  43. theorem OAI.BoundedTreePotentials.BlockCalculus.linear_positive_unit line 376
  44. theorem OAI.BoundedTreePotentials.BlockCalculus.linear_bottom_up_tail line 398