OAI/Analysis/DiamondDistortion/UpperFunction.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DiamondDistortion.RecursiveModel.Full line 17
  2. lemma OAI.DiamondDistortion.RecursiveModel.p_ne_zero line 18
  3. def OAI.DiamondDistortion.RecursiveModel.child line 21
  4. lemma OAI.DiamondDistortion.RecursiveModel.child_apply line 25
  5. lemma OAI.DiamondDistortion.RecursiveModel.child_sum line 27
  6. lemma OAI.DiamondDistortion.RecursiveModel.child_summable line 30
  7. def OAI.DiamondDistortion.RecursiveModel.children line 34
  8. lemma OAI.DiamondDistortion.RecursiveModel.children_apply line 38
  9. lemma OAI.DiamondDistortion.RecursiveModel.children_norm line 39
  10. lemma OAI.DiamondDistortion.RecursiveModel.child_add line 48
  11. lemma OAI.DiamondDistortion.RecursiveModel.child_neg line 50
  12. lemma OAI.DiamondDistortion.RecursiveModel.child_smul line 52
  13. lemma OAI.DiamondDistortion.RecursiveModel.child_zero line 54
  14. structure OAI.DiamondDistortion.UpperFunction.Data line 59
  15. def OAI.DiamondDistortion.UpperFunction.Data.positiveArray line 65
  16. def OAI.DiamondDistortion.UpperFunction.Data.negativeArray line 68
  17. lemma OAI.DiamondDistortion.UpperFunction.Data.positiveArray_apply line 71
  18. lemma OAI.DiamondDistortion.UpperFunction.Data.negativeArray_apply line 73
  19. lemma OAI.DiamondDistortion.UpperFunction.Data.positiveArray_norm line 75
  20. lemma OAI.DiamondDistortion.UpperFunction.Data.negativeArray_norm line 77
  21. lemma OAI.DiamondDistortion.RecursiveModel.join_upper_bound line 83
  22. def OAI.DiamondDistortion.RecursiveModel.fullUpperData line 94

    Source documentation

    Least upper values on the original full ℓp component, not on a finite-support substitute. All child sequences are genuine countable ℓp vectors.

    def fullUpperData : (h : ℕ) → UpperFunction.Data (Full p h) (3^h)
  | 0 => {
      value v := (max (v ()) 0,max (-v ()) 0)
…

    Mentions: OAI.DiamondDistortion.UpperFunction.Data, OAI.DiamondDistortion.RecursiveModel.Full

  23. def OAI.DiamondDistortion.RecursiveModel.fullUpper line 120
  24. def OAI.DiamondDistortion.RecursiveModel.fullPChildren line 121
  25. def OAI.DiamondDistortion.RecursiveModel.fullQChildren line 123
  26. lemma OAI.DiamondDistortion.RecursiveModel.fullUpper_zero_height line 125
  27. lemma OAI.DiamondDistortion.RecursiveModel.fullUpper_succ line 126
  28. lemma OAI.DiamondDistortion.RecursiveModel.fullPChildren_apply line 128
  29. lemma OAI.DiamondDistortion.RecursiveModel.fullQChildren_apply line 130
  30. lemma OAI.DiamondDistortion.RecursiveModel.fullUpper_nonneg line 132
  31. lemma OAI.DiamondDistortion.RecursiveModel.fullUpper_bound line 134
  32. lemma OAI.DiamondDistortion.RecursiveModel.fullUpper_zero line 138
  33. lemma OAI.DiamondDistortion.RecursiveModel.child_finiteLp line 144
  34. lemma OAI.DiamondDistortion.RecursiveModel.fullUpper_finiteLp line 147