OAI/Combinatorics/Progressions/Probability/WeightedPlateauMixture.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.rationalGridPhase_sub line 18
  2. def OAI.Erdos3.plateauModeMixture line 26
  3. theorem OAI.Erdos3.plateauModeMixture_integrand_norm line 32
  4. theorem OAI.Erdos3.plateauModeMixture_norm line 40
  5. theorem OAI.Erdos3.plateauModeMixture_lipschitz line 47
  6. theorem OAI.Erdos3.plateauModeMixture_grid_factor line 66
  7. def OAI.Erdos3.weightedModeratePlateauApproximation line 101
  8. theorem OAI.Erdos3.weightedModerateGridDensity_eq_pmf_buffered line 107
  9. theorem OAI.Erdos3.weightedModeratePointMass_error_plateau line 128
  10. theorem OAI.Erdos3.weightedModeratePlateauApproximation_norm_le_cap line 178
  11. theorem OAI.Erdos3.weightedModeratePlateauApproximation_split line 191
  12. theorem OAI.Erdos3.weightedModeratePlateauApproximation_split_periods line 225
  13. theorem OAI.Erdos3.weightedModeratePlateauMixture_expansion line 242