OAI/Analysis/TreePotential/CostCompletion.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BoundedTreePotentials.CostHeads.linear_coefficient_head line 14
  2. lemma OAI.BoundedTreePotentials.CostHeads.linear_head_eq_self_iff line 18
  3. lemma OAI.BoundedTreePotentials.CostHeads.linear_head_eq_zero_iff line 34
  4. lemma OAI.BoundedTreePotentials.CostHeads.linear_finite_head_approx line 50
  5. def OAI.BoundedTreePotentials.CostHeads.linearCoordinateTail line 55
  6. lemma OAI.BoundedTreePotentials.CostHeads.mem_linearCoordinateTail line 58
  7. lemma OAI.BoundedTreePotentials.CostHeads.linear_head_ker line 63
  8. instance OAI.BoundedTreePotentials.CostHeads.linear_head_finiteRank line 68
  9. lemma OAI.BoundedTreePotentials.CostHeads.linear_head_weaklyNull line 76
  10. lemma OAI.BoundedTreePotentials.CostHeads.quadratic_coefficient_head line 90
  11. lemma OAI.BoundedTreePotentials.CostHeads.quadratic_head_eq_self_iff line 94
  12. lemma OAI.BoundedTreePotentials.CostHeads.quadratic_head_eq_zero_iff line 110
  13. lemma OAI.BoundedTreePotentials.CostHeads.quadratic_finite_head_approx line 126
  14. def OAI.BoundedTreePotentials.CostHeads.quadraticCoordinateTail line 131
  15. lemma OAI.BoundedTreePotentials.CostHeads.mem_quadraticCoordinateTail line 134
  16. lemma OAI.BoundedTreePotentials.CostHeads.quadratic_head_ker line 139
  17. instance OAI.BoundedTreePotentials.CostHeads.quadratic_head_finiteRank line 144
  18. lemma OAI.BoundedTreePotentials.CostHeads.quadratic_head_weaklyNull line 152
  19. lemma OAI.BoundedTreePotentials.sqrt_shift line 168
  20. lemma OAI.BoundedTreePotentials.finiteRank_close_pair line 184
  21. theorem OAI.BoundedTreePotentials.CostHeads.linear_completed_tail_bound line 213

    Source documentation

    Transfer from finite centers to arbitrary completed centers, uniformly on an entire closed finite-codimensional tail.

    theorem linear_completed_tail_bound (x : LinearOuter) (hx : ‖x‖ = 1)
    {t ε : ℝ} (ht : 0 < t) (hε : 0 < ε) :
    ∃ F : ClosedFiniteCodim LinearOuter, ∀ y, y ∈ F.space → 1 ≤ ‖y‖ →
      Real.sqrt (1+t^2/16)-1-ε ≤ (‖x+t • y‖+‖x-t • y‖)/2-1 := by
…

    Mentions: OAI.BoundedTreePotentials.LinearOuter, OAI.BoundedTreePotentials.ClosedFiniteCodim

  22. theorem OAI.BoundedTreePotentials.CostHeads.linear_averaged_modulus line 238
  23. theorem OAI.BoundedTreePotentials.CostHeads.quadratic_completed_tail_bound line 246

    Source documentation

    Transfer from finite centers to arbitrary completed centers, uniformly on an entire closed finite-codimensional tail.

    theorem quadratic_completed_tail_bound (x : QuadraticOuter) (hx : ‖x‖ = 1)
    {t ε : ℝ} (ht : 0 < t) (hε : 0 < ε) :
    ∃ F : ClosedFiniteCodim QuadraticOuter, ∀ y, y ∈ F.space → 1 ≤ ‖y‖ →
      Real.sqrt (1+t^2/16)-1-ε ≤ (‖x+t • y‖+‖x-t • y‖)/2-1 := by
…

    Mentions: OAI.BoundedTreePotentials.QuadraticOuter, OAI.BoundedTreePotentials.ClosedFiniteCodim

  24. theorem OAI.BoundedTreePotentials.CostHeads.quadratic_averaged_modulus line 271