OAI/Analysis/DiamondDistortion/PathModels.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DiamondDistortion.PathModel.L1 line 17
  2. abbrev OAI.DiamondDistortion.PathModel.L2 line 18
  3. def OAI.DiamondDistortion.PathModel.branch line 20
  4. lemma OAI.DiamondDistortion.PathModel.branch_apply line 21
  5. lemma OAI.DiamondDistortion.PathModel.ancestors_card line 26
  6. lemma OAI.DiamondDistortion.PathModel.branch_norm line 37
  7. lemma OAI.DiamondDistortion.PathModel.summable_abs line 46
  8. lemma OAI.DiamondDistortion.PathModel.tsum_abs line 48
  9. lemma OAI.DiamondDistortion.PathModel.path_summable_norm line 50
  10. lemma OAI.DiamondDistortion.PathModel.path_summable line 55
  11. def OAI.DiamondDistortion.PathModel.path line 58
  12. lemma OAI.DiamondDistortion.PathModel.path_apply line 74
  13. lemma OAI.DiamondDistortion.PathModel.path_coordinate line 79
  14. def OAI.DiamondDistortion.PathModel.presentation line 101

    Source documentation

    The admissible decompositions use full ℓ² and ℓ¹, and the norm on their pair is exactly the linear (q=1) or quadratic (q=2) representation cost.

    def presentation (q : ℝ≥0∞) [Fact (1 ≤ q)] (h : ℕ) :
    InfimalCost.Presentation (WithLp q (L2 h × L1 h)) (L2 h) where
…

    Mentions: OAI.DiamondDistortion.InfimalCost.Presentation, OAI.DiamondDistortion.PathModel.L2, OAI.DiamondDistortion.PathModel.L1

  15. lemma OAI.DiamondDistortion.PathModel.presentation_output line 116
  16. lemma OAI.DiamondDistortion.PathModel.presentation_section line 118
  17. def OAI.DiamondDistortion.PathModel.cost line 122

    Source documentation

    Literal infimum over all decompositions z=h+Jμ.

    def cost (q : ℝ≥0∞) [Fact (1 ≤ q)] (h : ℕ) : Seminorm ℝ (L2 h) := (presentation q h).seminorm

    Mentions: OAI.DiamondDistortion.PathModel.L2, OAI.DiamondDistortion.PathModel.presentation

  18. lemma OAI.DiamondDistortion.PathModel.linear_cost_formula line 123
  19. lemma OAI.DiamondDistortion.PathModel.quadratic_cost_formula line 133
  20. lemma OAI.DiamondDistortion.PathModel.representation_coordinate line 144
  21. lemma OAI.DiamondDistortion.PathModel.linear_coordinate line 151
  22. lemma OAI.DiamondDistortion.PathModel.quadratic_coordinate line 157
  23. lemma OAI.DiamondDistortion.PathModel.linear_le_norm line 170
  24. lemma OAI.DiamondDistortion.PathModel.quadratic_le_norm line 173
  25. def OAI.DiamondDistortion.PathModel.finiteEmbedding line 178

    Source documentation

    Coordinate finite vectors inherit the same exact full-representation infimum.

    def finiteEmbedding (h : ℕ) : Vec h →ₗ[ℝ] L2 h where
…

    Mentions: OAI.DiamondDistortion.PathModel.L2

  26. def OAI.DiamondDistortion.PathModel.finiteCost line 182
  27. def OAI.DiamondDistortion.RecursiveModel.outerValues line 190

    Source documentation

    The literal outer ℓ² norm of a family of finite component seminorms.

    def outerValues (s : ∀ h,Seminorm ℝ (Vec (h+1))) (v : ForestVec) : ℕ →₀ ℝ :=
…

    Mentions: OAI.DiamondDistortion.RecursiveModel.Vec, OAI.DiamondDistortion.RecursiveModel.ForestVec

  28. lemma OAI.DiamondDistortion.RecursiveModel.outerValues_apply line 192
  29. lemma OAI.DiamondDistortion.RecursiveModel.outerValues_zero line 194
  30. lemma OAI.DiamondDistortion.RecursiveModel.outerValues_nonneg line 195
  31. lemma OAI.DiamondDistortion.RecursiveModel.outerValues_add line 197
  32. lemma OAI.DiamondDistortion.RecursiveModel.outerValues_neg line 201
  33. lemma OAI.DiamondDistortion.RecursiveModel.outerValues_smul line 205
  34. def OAI.DiamondDistortion.RecursiveModel.outerSeminorm line 210
  35. lemma OAI.DiamondDistortion.RecursiveModel.component_le_outer line 217
  36. def OAI.DiamondDistortion.PathModel.linearForestSeminorm line 227
  37. def OAI.DiamondDistortion.PathModel.quadraticForestSeminorm line 228
  38. lemma OAI.DiamondDistortion.PathModel.linear_forest_coordinate line 229
  39. lemma OAI.DiamondDistortion.PathModel.quadratic_forest_coordinate line 232
  40. def OAI.DiamondDistortion.PathModel.root line 238

    Source documentation

    Original component root; this is distinct from a forest component index.

    def root : (h : ℕ) → Coord h
  | 0 => ()
  | _+1 => Sum.inl ()
  41. lemma OAI.DiamondDistortion.PathModel.root_ancestors line 241
  42. lemma OAI.DiamondDistortion.PathModel.branch_root line 242
  43. lemma OAI.DiamondDistortion.PathModel.path_single line 244
  44. lemma OAI.DiamondDistortion.PathModel.linear_root line 251
  45. lemma OAI.DiamondDistortion.PathModel.quadratic_root line 256
  46. def OAI.DiamondDistortion.PathModel.linearData line 282

    Source documentation

    Exact path-cost completions on the original finite-height components.

    def linearData : CoordinateCompletion.Data ForestCoord where
…

    Mentions: OAI.DiamondDistortion.CoordinateCompletion.Data

  47. def OAI.DiamondDistortion.PathModel.quadraticData line 285
  48. abbrev OAI.DiamondDistortion.PathModel.LinearSpace line 288
  49. abbrev OAI.DiamondDistortion.PathModel.QuadraticSpace line 289
  50. def OAI.DiamondDistortion.PathModel.linearHeads line 290
  51. def OAI.DiamondDistortion.PathModel.quadraticHeads line 292
  52. lemma OAI.DiamondDistortion.PathModel.linearHeads_commutes line 294
  53. lemma OAI.DiamondDistortion.PathModel.quadraticHeads_commutes line 295
  54. theorem OAI.DiamondDistortion.PathModel.linear_flow_graph line 298

    Source documentation

    Positive flow and trimming are retained as independent exact intrinsic inputs.

    theorem linear_flow_graph (hinput : FlowInput linearHeads (linearC^2))
    {D s : ℝ} (k : ℕ) (f : Diamond.Vertex k → LinearSpace) (hf : Diamond.HasDistortion k f D s) :
    1+(k:ℝ)/(2*linearC^2) ≤ D^2 ∧ (k:ℝ) ≤ 2*linearC^2*D^2 :=
…

    Mentions: OAI.DiamondDistortion.PathModel.linearHeads, OAI.DiamondDistortion.Diamond.Vertex, OAI.DiamondDistortion.PathModel.LinearSpace, OAI.DiamondDistortion.Diamond.HasDistortion

  55. theorem OAI.DiamondDistortion.PathModel.linear_trimming_graph line 302
  56. theorem OAI.DiamondDistortion.PathModel.linear_clipping_graph line 305
  57. theorem OAI.DiamondDistortion.PathModel.linear_vanishing_graph line 309
  58. theorem OAI.DiamondDistortion.PathModel.linear_vanishing_weak line 311
  59. theorem OAI.DiamondDistortion.PathModel.quadratic_graph line 317
  60. theorem OAI.DiamondDistortion.PathModel.stopped_graph line 320
  61. theorem OAI.DiamondDistortion.PathModel.quadratic_component_graph line 323