OAI/Analysis/RecursivePotentials/VariableStability.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RecursivePotentials.VariableExponent.holder_mixed line 31
  2. lemma OAI.RecursivePotentials.VariableExponent.cuberoot_cube line 45
  3. lemma OAI.RecursivePotentials.VariableExponent.cube_cuberoot line 49
  4. lemma OAI.RecursivePotentials.VariableExponent.cube_two_thirds line 53
  5. lemma OAI.RecursivePotentials.VariableExponent.square_cuberoot line 57
  6. lemma OAI.RecursivePotentials.VariableExponent.cubic_transport line 61
  7. lemma OAI.RecursivePotentials.VariableExponent.cubic_transport_tsum line 81
  8. lemma OAI.RecursivePotentials.VariableExponent.energy_of_cubic line 92
  9. abbrev OAI.RecursivePotentials.VariableExponent.Outer line 113
  10. lemma OAI.RecursivePotentials.VariableExponent.outer_hasSum_square line 115
  11. lemma OAI.RecursivePotentials.VariableExponent.norm_midpoint_average line 120
  12. lemma OAI.RecursivePotentials.VariableExponent.midpoint_energy_nonneg line 131
  13. theorem OAI.RecursivePotentials.VariableExponent.outer_sixth_of_components line 136
  14. theorem OAI.RecursivePotentials.VariableExponent.outer_cubic_squared line 154
  15. theorem OAI.RecursivePotentials.VariableExponent.outer_cubic_of_components line 189
  16. def OAI.RecursivePotentials.AggregationVector.childLp line 234
  17. lemma OAI.RecursivePotentials.AggregationVector.childLp_apply line 237
  18. lemma OAI.RecursivePotentials.AggregationVector.childLp_norm_le line 242
  19. lemma OAI.RecursivePotentials.AggregationVector.childLp_norm_eq line 252
  20. def OAI.RecursivePotentials.AggregationVector.childP line 275
  21. def OAI.RecursivePotentials.AggregationVector.childQ line 278
  22. lemma OAI.RecursivePotentials.AggregationVector.child_bounds line 281
  23. lemma OAI.RecursivePotentials.AggregationVector.field_differences line 286
  24. lemma OAI.RecursivePotentials.AggregationVector.children_dist_le line 299
  25. lemma OAI.RecursivePotentials.AggregationVector.childP_lipschitz line 326
  26. lemma OAI.RecursivePotentials.AggregationVector.childQ_lipschitz line 331
  27. lemma OAI.RecursivePotentials.AggregationVector.finite_recursion line 336
  28. def OAI.RecursivePotentials.AggregationSpace.childP line 397
  29. def OAI.RecursivePotentials.AggregationSpace.childQ line 400
  30. lemma OAI.RecursivePotentials.AggregationSpace.childP_coe line 403
  31. lemma OAI.RecursivePotentials.AggregationSpace.childQ_coe line 407
  32. lemma OAI.RecursivePotentials.AggregationSpace.continuous_childP line 411
  33. lemma OAI.RecursivePotentials.AggregationSpace.continuous_childQ line 414
  34. lemma OAI.RecursivePotentials.AggregationSpace.childP_apply line 417
  35. lemma OAI.RecursivePotentials.AggregationSpace.childQ_apply line 426
  36. theorem OAI.RecursivePotentials.AggregationSpace.recursion line 435
  37. lemma OAI.RecursivePotentials.AggregationSpace.childP_norm_formula line 446
  38. lemma OAI.RecursivePotentials.AggregationSpace.childQ_norm_formula line 455
  39. lemma OAI.RecursivePotentials.Variable.component_comparisons line 474
  40. lemma OAI.RecursivePotentials.Variable.component_reflexive line 480
  41. instance OAI.RecursivePotentials.Variable.component_dual_separable line 484
  42. theorem OAI.RecursivePotentials.Variable.reflexive line 488
  43. instance OAI.RecursivePotentials.Variable.dual_separable line 490
  44. lemma OAI.RecursivePotentials.Variable.componentEquiv_apply line 497
  45. lemma OAI.RecursivePotentials.Variable.component_ext line 502
  46. lemma OAI.RecursivePotentials.Variable.coordinate_apply line 509
  47. lemma OAI.RecursivePotentials.Variable.coordinates_ext line 512
  48. lemma OAI.RecursivePotentials.Variable.coordinate_basis line 517
  49. lemma OAI.RecursivePotentials.Variable.projection_apply line 530
  50. lemma OAI.RecursivePotentials.Variable.coordinate_projection line 534
  51. lemma OAI.RecursivePotentials.Variable.projection_finite line 540
  52. lemma OAI.RecursivePotentials.Variable.projection_fixed line 543
  53. lemma OAI.RecursivePotentials.Variable.projection_idem line 552
  54. lemma OAI.RecursivePotentials.Variable.component_projection_fixed line 559
  55. lemma OAI.RecursivePotentials.Variable.component_mem_tail line 570
  56. lemma OAI.RecursivePotentials.Variable.component_cubic line 581
  57. lemma OAI.RecursivePotentials.Variable.component_sixth line 592
  58. theorem OAI.RecursivePotentials.Variable.cubic_stability line 599
  59. theorem OAI.RecursivePotentials.Variable.sixth_stability line 604
  60. lemma OAI.RecursivePotentials.ScalarLp.coordinate_cofinite line 626
  61. lemma OAI.RecursivePotentials.ScalarLp.basis_functionals_tendsto_zero line 635
  62. def OAI.RecursivePotentials.Variable.finiteSubmodule line 652
  63. lemma OAI.RecursivePotentials.Variable.finite_single line 664
  64. lemma OAI.RecursivePotentials.Variable.finite_support_dense line 676
  65. lemma OAI.RecursivePotentials.Variable.projection_finite_rank line 686
  66. lemma OAI.RecursivePotentials.Variable.projection_weaklyNull line 694
  67. def OAI.RecursivePotentials.Variable.fiber line 699
  68. def OAI.RecursivePotentials.Variable.ancestralHeads line 702
  69. def OAI.RecursivePotentials.Variable.ancestralUnion line 705
  70. lemma OAI.RecursivePotentials.Variable.fiber_mem line 707
  71. lemma OAI.RecursivePotentials.Variable.ancestralUnion_contains line 710
  72. lemma OAI.RecursivePotentials.Variable.heads_admissible line 715
  73. lemma OAI.RecursivePotentials.Variable.weakTailConstant_pos line 733
  74. lemma OAI.RecursivePotentials.Variable.cubic_stability_mul line 737
  75. lemma OAI.RecursivePotentials.Variable.finite_center_weak_bound line 751
  76. theorem OAI.RecursivePotentials.Variable.weak_null_cubic line 797
  77. theorem OAI.RecursivePotentials.Variable.weak_tail line 808