OAI/Analysis/DiamondDistortion/RecursiveBounds.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DiamondDistortion.RecursiveModel.fullUpper_neg line 19
  2. lemma OAI.DiamondDistortion.RecursiveModel.fullUpper_add line 34
  3. lemma OAI.DiamondDistortion.RecursiveModel.fullUpper_smul_nonneg line 69
  4. def OAI.DiamondDistortion.RecursiveModel.fullNu line 87
  5. lemma OAI.DiamondDistortion.RecursiveModel.fullNu_nonneg line 88
  6. lemma OAI.DiamondDistortion.RecursiveModel.fullNu_zero line 90
  7. lemma OAI.DiamondDistortion.RecursiveModel.fullNu_add line 91
  8. lemma OAI.DiamondDistortion.RecursiveModel.fullNu_neg line 96
  9. lemma OAI.DiamondDistortion.RecursiveModel.fullNu_smul line 98
  10. def OAI.DiamondDistortion.RecursiveModel.fullNuSeminorm line 109
  11. lemma OAI.DiamondDistortion.RecursiveModel.fullNu_upper line 116
  12. lemma OAI.DiamondDistortion.RecursiveModel.full_leaf_norm line 121
  13. lemma OAI.DiamondDistortion.RecursiveModel.rootZero_norm line 125
  14. lemma OAI.DiamondDistortion.RecursiveModel.root_children_norm line 134
  15. lemma OAI.DiamondDistortion.RecursiveModel.fullNu_lower line 147
  16. lemma OAI.DiamondDistortion.RecursiveModel.join_difference line 177
  17. lemma OAI.DiamondDistortion.RecursiveModel.join_least line 184
  18. def OAI.DiamondDistortion.RecursiveModel.fullRoot line 188
  19. lemma OAI.DiamondDistortion.RecursiveModel.fullUpper_difference line 192
  20. def OAI.DiamondDistortion.RecursiveModel.fullArray line 201

    Source documentation

    The complete least upper arrays, including every non-root coordinate.

    def fullArray : (h : ℕ) → Full p h → Coord h → ℝ × ℝ
  | 0,v,_ => fullUpper p hp 0 v
  | h+1,v,.inl _ => fullUpper p hp (h+1) v
  | h+1,v,.inr (i,s) => fullArray h (child p hp h v i) s

    Mentions: OAI.DiamondDistortion.RecursiveModel.Full, OAI.DiamondDistortion.RecursiveModel.Coord, OAI.DiamondDistortion.RecursiveModel.fullUpper, OAI.DiamondDistortion.RecursiveModel.child

  21. lemma OAI.DiamondDistortion.RecursiveModel.fullArray_root line 205
  22. lemma OAI.DiamondDistortion.RecursiveModel.fullArray_nonneg_diff line 207
  23. def OAI.DiamondDistortion.RecursiveModel.FullAdmissible line 220

    Source documentation

    Exact upper-array constraints: nonnegative values, coordinate difference v, and each of the two arrays dominating the countable ℓp norm of its children. At leaves the child norm is zero.

    def FullAdmissible : (h : ℕ) → Full p h → (Coord h → ℝ × ℝ) → Prop
  | 0,v,A => 0 ≤ (A ()).1 ∧ 0 ≤ (A ()).2 ∧ (A ()).1-(A ()).2=v ()
  | h+1,v,A =>
    (0 ≤ (A (.inl ())).1 ∧ 0 ≤ (A (.inl ())).2 ∧ (A (.inl ())).1-(A (.inl ())).2=v (.inl ())) ∧
    (∃ a b : lp (fun _ : ℕ => ℝ) p,
      (∀ i,a i=(A (.inr (i,fullRoot h))).1) ∧ (∀ i,b i=(A (.inr (i,fullRoot h))).2) ∧
      ‖a‖ ≤ (A (.inl ())).1 ∧ ‖b‖ ≤ (A (.inl ())).2) ∧
    ∀ i,FullAdmissible h (child p hp h v i) (fun s => A (.inr (i,s)))

    Mentions: OAI.DiamondDistortion.RecursiveModel.Full, OAI.DiamondDistortion.RecursiveModel.Coord, OAI.DiamondDistortion.RecursiveModel.fullRoot, OAI.DiamondDistortion.RecursiveModel.child

  24. lemma OAI.DiamondDistortion.RecursiveModel.fullAdmissible_root line 228
  25. lemma OAI.DiamondDistortion.RecursiveModel.fullArray_admissible line 235
  26. lemma OAI.DiamondDistortion.RecursiveModel.fullUpper_least line 248
  27. lemma OAI.DiamondDistortion.RecursiveModel.fullArray_least line 272
  28. def OAI.DiamondDistortion.Midpoint.Heads.transport line 287
  29. lemma OAI.DiamondDistortion.Midpoint.Heads.transport_projection line 311
  30. lemma OAI.DiamondDistortion.RecursiveModel.exponent_ne_top line 318
  31. lemma OAI.DiamondDistortion.RecursiveModel.exponent_real_pos line 321
  32. def OAI.DiamondDistortion.RecursiveModel.fullData line 323
  33. abbrev OAI.DiamondDistortion.RecursiveModel.VectorComponent line 329
  34. abbrev OAI.DiamondDistortion.RecursiveModel.FullVectorSpace line 331
  35. def OAI.DiamondDistortion.RecursiveModel.fullVectorEmbedding line 333
  36. lemma OAI.DiamondDistortion.RecursiveModel.fullVectorEmbedding_norm line 335
  37. lemma OAI.DiamondDistortion.RecursiveModel.fullVectorEmbedding_dense line 344
  38. def OAI.DiamondDistortion.RecursiveModel.fullVectorEquiv line 347

    Source documentation

    Exact full-model identification, preserving every finite coordinate.

    def fullVectorEquiv : VectorSpace ≃ₗᵢ[ℝ] FullVectorSpace :=
…

    Mentions: OAI.DiamondDistortion.RecursiveModel.VectorSpace, OAI.DiamondDistortion.RecursiveModel.FullVectorSpace

  39. lemma OAI.DiamondDistortion.RecursiveModel.fullVectorEquiv_embedding line 349
  40. def OAI.DiamondDistortion.RecursiveModel.fullVectorHeads line 351
  41. theorem OAI.DiamondDistortion.RecursiveModel.full_sixth_graph line 353
  42. theorem OAI.DiamondDistortion.RecursiveModel.full_cubic_graph line 356