OAI/Combinatorics/Progressions/Estimates/FiniteMixedPermutation.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.finiteMixedLpCore line 11
  2. def OAI.Erdos3.finiteMixedLpBound line 15
  3. theorem OAI.Erdos3.finiteMixedLpCore_nonneg line 19
  4. theorem OAI.Erdos3.finiteMixedLpBound_nonneg line 25
  5. theorem OAI.Erdos3.finiteMixedLpCore_eq_product line 33
  6. theorem OAI.Erdos3.scaled_reciprocal_exponent line 40
  7. theorem OAI.Erdos3.finiteMixedLpCore_scale line 44
  8. theorem OAI.Erdos3.finiteMixedLpBound_step line 59
  9. theorem OAI.Erdos3.finiteMixedLpCore_le_constant line 87
  10. theorem OAI.Erdos3.finiteMixedLpBound_le_constant line 114
  11. theorem OAI.Erdos3.finiteMixedLp_le_bound line 152
  12. theorem OAI.Erdos3.finiteMixedLp_interpolation line 205
  13. theorem OAI.Erdos3.finiteSectionCount_snoc line 226
  14. theorem OAI.Erdos3.finiteSectionL2Control_sections line 230
  15. theorem OAI.Erdos3.finiteSectionL2Control_of_sections line 248
  16. theorem OAI.Erdos3.finiteSectionL2Control_iff_sections line 273
  17. theorem OAI.Erdos3.finiteMixedLp_interpolation_of_sections line 292
  18. theorem OAI.Erdos3.finiteMixedLp_le_constant_of_sections line 303
  19. theorem OAI.Erdos3.finiteMixedLp_permuted_le_constant line 324