OAI/Analysis/RecursivePotentials/VariableCompletion.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RecursivePotentials.VariableTree.P_eq_zero_off_head line 32
  2. lemma OAI.RecursivePotentials.VariableTree.Q_eq_zero_off_head line 37
  3. lemma OAI.RecursivePotentials.VariableTree.potentials_le_normSum line 42
  4. lemma OAI.RecursivePotentials.VariableTree.potentials_lipschitz line 51
  5. def OAI.RecursivePotentials.VariableTree.projectHead line 64
  6. lemma OAI.RecursivePotentials.VariableTree.projectHead_apply line 66
  7. lemma OAI.RecursivePotentials.VariableTree.projectHead_bound line 69
  8. lemma OAI.RecursivePotentials.AggregationVector.norm_def line 95
  9. lemma OAI.RecursivePotentials.AggregationVector.coordinate_apply line 97
  10. lemma OAI.RecursivePotentials.AggregationVector.lipschitz_P line 99
  11. lemma OAI.RecursivePotentials.AggregationVector.lipschitz_Q line 106
  12. def OAI.RecursivePotentials.AggregationVector.projectionLinear line 113
  13. def OAI.RecursivePotentials.AggregationVector.projection line 128
  14. lemma OAI.RecursivePotentials.AggregationVector.projection_apply line 135
  15. lemma OAI.RecursivePotentials.AggregationVector.projection_contracts line 138
  16. lemma OAI.RecursivePotentials.AggregationVector.projection_idem line 141
  17. lemma OAI.RecursivePotentials.AggregationSpace.coordinate_coe line 160
  18. lemma OAI.RecursivePotentials.AggregationSpace.P_coe line 164
  19. lemma OAI.RecursivePotentials.AggregationSpace.Q_coe line 168
  20. lemma OAI.RecursivePotentials.AggregationSpace.continuous_P line 172
  21. lemma OAI.RecursivePotentials.AggregationSpace.continuous_Q line 175
  22. lemma OAI.RecursivePotentials.AggregationSpace.P_nonneg line 178
  23. lemma OAI.RecursivePotentials.AggregationSpace.Q_nonneg line 183
  24. lemma OAI.RecursivePotentials.AggregationSpace.P_sub_Q line 188
  25. theorem OAI.RecursivePotentials.AggregationSpace.norm_eq line 195
  26. lemma OAI.RecursivePotentials.AggregationSpace.abs_coordinate_le line 200
  27. lemma OAI.RecursivePotentials.AggregationSpace.fields_lipschitz line 206
  28. def OAI.RecursivePotentials.AggregationSpace.projection line 222
  29. lemma OAI.RecursivePotentials.AggregationSpace.projection_coe line 226
  30. lemma OAI.RecursivePotentials.AggregationSpace.projection_contracts line 230
  31. lemma OAI.RecursivePotentials.AggregationSpace.projection_idem line 237
  32. lemma OAI.RecursivePotentials.AggregationSpace.coordinate_projection line 243
  33. def OAI.RecursivePotentials.AggregationSpace.tail line 256
  34. lemma OAI.RecursivePotentials.AggregationSpace.tail_closed line 259
  35. theorem OAI.RecursivePotentials.AggregationSpace.finite_tail_dense line 263
  36. def OAI.RecursivePotentials.AggregationVector.ofHeadLinear line 291
  37. def OAI.RecursivePotentials.AggregationVector.ofHead line 306
  38. lemma OAI.RecursivePotentials.AggregationVector.ofHead_apply line 309
  39. lemma OAI.RecursivePotentials.AggregationVector.ofHead_support line 314
  40. lemma OAI.RecursivePotentials.AggregationVector.basisVector_apply line 321
  41. lemma OAI.RecursivePotentials.AggregationVector.not_finite_dimensional line 324
  42. def OAI.RecursivePotentials.AggregationSpace.headCoordinates line 339
  43. lemma OAI.RecursivePotentials.AggregationSpace.headCoordinates_apply line 342
  44. theorem OAI.RecursivePotentials.AggregationSpace.projection_reconstructs line 345
  45. lemma OAI.RecursivePotentials.AggregationSpace.tail_eq_coordinate_kernel line 366
  46. theorem OAI.RecursivePotentials.AggregationSpace.tail_finite_codimension line 383
  47. theorem OAI.RecursivePotentials.AggregationSpace.supported_is_finite line 388
  48. theorem OAI.RecursivePotentials.AggregationSpace.not_finite_dimensional line 394
  49. lemma OAI.RecursivePotentials.VariableExponent.cubicConstant_pos line 406
  50. lemma OAI.RecursivePotentials.VariableExponent.cubicConstant_le_one line 408
  51. lemma OAI.RecursivePotentials.VariableExponent.sixthConstant_pos line 414
  52. lemma OAI.RecursivePotentials.VariableExponent.sixthConstant_le_twice_cubic line 416
  53. lemma OAI.RecursivePotentials.VariableExponent.sixth_of_cubic line 437
  54. theorem OAI.RecursivePotentials.VariableTree.normSum_cubic line 487
  55. theorem OAI.RecursivePotentials.AggregationSpace.cubic_projected_tail line 530
  56. theorem OAI.RecursivePotentials.AggregationSpace.cubic_tail line 550
  57. theorem OAI.RecursivePotentials.AggregationSpace.cubic_supported line 563
  58. lemma OAI.RecursivePotentials.AggregationSpace.norm_lens_average line 573
  59. theorem OAI.RecursivePotentials.AggregationSpace.cubic_component line 584
  60. theorem OAI.RecursivePotentials.AggregationSpace.sixth_supported line 598
  61. lemma OAI.RecursivePotentials.AggregationSpace.cubic_zero line 609
  62. lemma OAI.RecursivePotentials.AggregationSpace.sixth_zero line 617
  63. theorem OAI.RecursivePotentials.AggregationSpace.sixth_component line 625