OAI/Analysis/RecursivePotentials/VariableLp.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RecursivePotentials.LpSupport.separable line 35
  2. lemma OAI.RecursivePotentials.dual_separable_of_equiv line 56
  3. structure OAI.RecursivePotentials.PowerExponent line 69
  4. lemma OAI.RecursivePotentials.PowerExponent.pos line 75
  5. lemma OAI.RecursivePotentials.PowerExponent.ne_zero line 77
  6. instance OAI.RecursivePotentials.PowerExponent.(instance at line 79) line 79
  7. def OAI.RecursivePotentials.PowerExponent.conjugate line 82
  8. lemma OAI.RecursivePotentials.PowerExponent.holder line 85
  9. abbrev OAI.RecursivePotentials.ScalarLp.Space line 94
  10. def OAI.RecursivePotentials.ScalarLp.pairing line 98
  11. lemma OAI.RecursivePotentials.ScalarLp.pairing_apply line 104
  12. lemma OAI.RecursivePotentials.ScalarLp.pairing_single_right line 108
  13. lemma OAI.RecursivePotentials.ScalarLp.pairing_single_left line 114
  14. def OAI.RecursivePotentials.ScalarLp.coefficient line 120
  15. lemma OAI.RecursivePotentials.ScalarLp.apply_single line 123
  16. def OAI.RecursivePotentials.ScalarLp.norming line 130
  17. lemma OAI.RecursivePotentials.ScalarLp.abs_norming line 132
  18. lemma OAI.RecursivePotentials.ScalarLp.norming_mul line 136
  19. lemma OAI.RecursivePotentials.ScalarLp.norming_rpow line 154
  20. lemma OAI.RecursivePotentials.ScalarLp.restriction_bound line 157
  21. lemma OAI.RecursivePotentials.ScalarLp.restriction_mem line 194
  22. def OAI.RecursivePotentials.ScalarLp.restrict line 200
  23. lemma OAI.RecursivePotentials.ScalarLp.restrict_apply line 203
  24. lemma OAI.RecursivePotentials.ScalarLp.pairing_restrict line 206
  25. theorem OAI.RecursivePotentials.ScalarLp.isReflexive line 214
  26. lemma OAI.RecursivePotentials.ScalarLp.separable line 236
  27. lemma OAI.RecursivePotentials.ScalarLp.dual_separable line 240
  28. lemma OAI.RecursivePotentials.AggregationVector.toLpLinear_apply line 259
  29. lemma OAI.RecursivePotentials.AggregationSpace.lpEquiv_coe line 279
  30. lemma OAI.RecursivePotentials.AggregationSpace.lpEquiv_apply line 285
  31. theorem OAI.RecursivePotentials.AggregationSpace.lp_comparisons line 293
  32. theorem OAI.RecursivePotentials.AggregationSpace.finite_height_reflexive line 314
  33. theorem OAI.RecursivePotentials.AggregationSpace.finite_height_dual_separable line 320