OAI/Combinatorics/Progressions/Estimates/SmoothWindowChange.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.FiniteProbabilityWeights.exists_bounded_change_of_measure line 12
  2. theorem OAI.Erdos3.finite_window_change_of_measure line 45
  3. def OAI.Erdos3.smoothSourceFiniteWeights line 92
  4. theorem OAI.Erdos3.smoothSourceFiniteWeights_mean line 106
  5. theorem OAI.Erdos3.smoothSourceFiniteWeights_energy line 119
  6. theorem OAI.Erdos3.smooth_inner_mem_indices line 139
  7. theorem OAI.Erdos3.smooth_window_change_of_measure line 150
  8. theorem OAI.Erdos3.shiftedSmoothProductMass_pos_of_large_scales line 169