OAI/Analysis/TreePotential/QuadraticCost.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BoundedTreePotentials.dot_two_le_sqrt line 14
  2. def OAI.BoundedTreePotentials.pairCost line 22
  3. lemma OAI.BoundedTreePotentials.pairCost_eq_norm line 24
  4. lemma OAI.BoundedTreePotentials.pairCost_add_le line 30
  5. lemma OAI.BoundedTreePotentials.pairCost_smul line 35
  6. lemma OAI.BoundedTreePotentials.pairCost_zero_right line 40
  7. lemma OAI.BoundedTreePotentials.pairCost_zero_left line 44
  8. def OAI.BoundedTreePotentials.quadraticCost line 49

    Source documentation

    The exact quadratic path cost.

    def quadraticCost (B : M →L[ℝ] H) (x : H) : ℝ :=
…
  9. lemma OAI.BoundedTreePotentials.quadraticCost_bddBelow line 52
  10. lemma OAI.BoundedTreePotentials.quadraticCost_nonneg line 56
  11. lemma OAI.BoundedTreePotentials.quadraticCost_le line 59
  12. lemma OAI.BoundedTreePotentials.quadraticCost_le_norm line 62
  13. lemma OAI.BoundedTreePotentials.quadraticCost_zero line 65
  14. lemma OAI.BoundedTreePotentials.quadraticCost_synthesis_le line 68
  15. lemma OAI.BoundedTreePotentials.quadraticCost_representation_le line 71
  16. lemma OAI.BoundedTreePotentials.quadraticCost_add_le line 75
  17. lemma OAI.BoundedTreePotentials.quadraticCost_smul_le line 89
  18. def OAI.BoundedTreePotentials.quadraticCostSeminorm line 99
  19. lemma OAI.BoundedTreePotentials.quadraticCost_exists_norming line 103
  20. lemma OAI.BoundedTreePotentials.norm_le_mul_quadraticCost line 112
  21. def OAI.BoundedTreePotentials.quadraticBlockCost line 132

    Source documentation

    Z_n uses the same rooted tree and synthesis, but a genuinely different norm.

    def quadraticBlockCost (n : ℕ) (x : TreeHilbert n) := quadraticCost (pathSynthesis n) x

    Mentions: OAI.BoundedTreePotentials.TreeHilbert, OAI.BoundedTreePotentials.quadraticCost, OAI.BoundedTreePotentials.pathSynthesis

  22. theorem OAI.BoundedTreePotentials.quadraticBlockCost_comparison line 134
  23. def OAI.BoundedTreePotentials.QuadraticBlock line 146
  24. instance OAI.BoundedTreePotentials.(instance at line 147) line 147
  25. instance OAI.BoundedTreePotentials.(instance at line 148) line 148
  26. def OAI.BoundedTreePotentials.quadraticBlockEquiv line 149
  27. instance OAI.BoundedTreePotentials.(instance at line 152) line 152
  28. theorem OAI.BoundedTreePotentials.quadraticBlockCore line 154
  29. instance OAI.BoundedTreePotentials.(instance at line 173) line 173
  30. instance OAI.BoundedTreePotentials.(instance at line 174) line 174
  31. lemma OAI.BoundedTreePotentials.norm_QuadraticBlock line 176
  32. def OAI.BoundedTreePotentials.quadraticBlockHilbertEquiv line 178
  33. def OAI.BoundedTreePotentials.quadraticBlockUniformEquiv line 187
  34. instance OAI.BoundedTreePotentials.(instance at line 191) line 191
  35. lemma OAI.BoundedTreePotentials.quadraticBlock_reflexive line 194
  36. abbrev OAI.BoundedTreePotentials.QuadraticOuter line 197
  37. theorem OAI.BoundedTreePotentials.quadraticOuter_reflexive line 198
  38. abbrev OAI.BoundedTreePotentials.pathBound line 204
  39. lemma OAI.BoundedTreePotentials.path_le_pathBound line 206
  40. lemma OAI.BoundedTreePotentials.pathBound_nonneg line 209
  41. def OAI.BoundedTreePotentials.quadraticPolar line 212
  42. lemma OAI.BoundedTreePotentials.quadraticPolar_nonneg line 215
  43. lemma OAI.BoundedTreePotentials.quadraticPolar_sq line 218
  44. lemma OAI.BoundedTreePotentials.quadraticPolar_le_iff line 221
  45. lemma OAI.BoundedTreePotentials.atom_pairing_scaled line 244
  46. lemma OAI.BoundedTreePotentials.path_pairing_bound line 263
  47. lemma OAI.BoundedTreePotentials.quadraticBlockCost_abs_eval_scaled line 268
  48. lemma OAI.BoundedTreePotentials.pathSynthesis_single line 283
  49. def OAI.BoundedTreePotentials.quadraticFunctional line 287
  50. lemma OAI.BoundedTreePotentials.quadraticFunctional_apply line 290
  51. theorem OAI.BoundedTreePotentials.quadraticFunctional_norm line 294

    Source documentation

    Exact quadratic dual norm, with a sum rather than a maximum.

    theorem quadraticFunctional_norm (n : ℕ) (f : TreeHilbert n) :
    ‖quadraticFunctional n f‖ = quadraticPolar n f := by
…

    Mentions: OAI.BoundedTreePotentials.TreeHilbert, OAI.BoundedTreePotentials.quadraticFunctional, OAI.BoundedTreePotentials.quadraticPolar

  52. theorem OAI.BoundedTreePotentials.quadraticFunctional_surjective line 326
  53. lemma OAI.BoundedTreePotentials.quadraticBlockCost_norming line 339
  54. theorem OAI.BoundedTreePotentials.quadraticBlockCost_duality line 346
  55. lemma OAI.BoundedTreePotentials.pathBound_single line 359
  56. lemma OAI.BoundedTreePotentials.quadraticPolar_single line 368
  57. lemma OAI.BoundedTreePotentials.coordinate_le_quadraticBlockCost line 372
  58. lemma OAI.BoundedTreePotentials.quadraticBlockCost_single_bounds line 378
  59. lemma OAI.BoundedTreePotentials.quadraticBlockCost_path_bounds line 388