OAI/Analysis/LpDimension/Parallelogram.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SubpolynomialLp.powerDefect line 12
  2. lemma OAI.SubpolynomialLp.sq_rpow_half line 15
  3. lemma OAI.SubpolynomialLp.strictly_superadditive_rpow line 20
  4. lemma OAI.SubpolynomialLp.strictly_subadditive_rpow line 38
  5. lemma OAI.SubpolynomialLp.powerDefect_pos line 56
  6. lemma OAI.SubpolynomialLp.powerDefect_neg line 69
  7. lemma OAI.SubpolynomialLp.powerDefect_eq_zero_iff line 82
  8. def OAI.SubpolynomialLp.lpPower line 93
  9. lemma OAI.SubpolynomialLp.lpPower_disjointness line 95
  10. lemma OAI.SubpolynomialLp.abs_midpoint_rpow_strict line 122
  11. lemma OAI.SubpolynomialLp.abs_midpoint_rpow_le line 139
  12. lemma OAI.SubpolynomialLp.lpPower_midpoint_eq_iff line 147
  13. lemma OAI.SubpolynomialLp.lpPower_nonneg line 167
  14. lemma OAI.SubpolynomialLp.lpPower_neg line 170
  15. lemma OAI.SubpolynomialLp.lpPower_smul line 173
  16. lemma OAI.SubpolynomialLp.lpPower_midpoint line 178
  17. lemma OAI.SubpolynomialLp.antipodes_of_lpPower line 183
  18. lemma OAI.SubpolynomialLp.disjoint_rows_columns_card line 193