OAI/Combinatorics/Progressions/Linear/ProductANOVASectionNormalizedBound.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.productANOVA_smul line 15
  2. theorem OAI.Erdos3.productANOVAEnergy_smul line 22
  3. theorem OAI.Erdos3.sqrt_productANOVAEnergy_smul line 27
  4. def OAI.Erdos3.productANOVASectionEnergy line 45
  5. theorem OAI.Erdos3.productANOVASectionEnergy_nonneg line 50
  6. theorem OAI.Erdos3.sqrt_productANOVASectionEnergy_le line 55
  7. theorem OAI.Erdos3.sqrt_productANOVASectionEnergy_le_normalized line 77
  8. theorem OAI.Erdos3.sqrt_productANOVASectionEnergy_le_of_normalized line 91
  9. theorem OAI.Erdos3.productANOVASection_bound_of_lower_degree line 119
  10. theorem OAI.Erdos3.anovaSection_power_bound line 144
  11. theorem OAI.Erdos3.anovaSection_power_bound_positive line 157
  12. def OAI.Erdos3.disjointCoordinateLevel line 175
  13. theorem OAI.Erdos3.mem_disjointCoordinateLevel line 179
  14. def OAI.Erdos3.productANOVASectionTensor line 184
  15. theorem OAI.Erdos3.productANOVASectionTensor_energy line 189
  16. theorem OAI.Erdos3.productANOVASectionTensor_bound_of_lower_degree line 208
  17. theorem OAI.Erdos3.productANOVASectionTensor_bound_of_normalized line 235