OAI/Combinatorics/Progressions/Linear/KernelMixtureControl.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.kernelAverage line 12
  2. theorem OAI.Erdos3.kernelAverage_lipschitz line 15
  3. theorem OAI.Erdos3.kernelAverage_nonneg line 40
  4. theorem OAI.Erdos3.kernelAverage_cap line 45
  5. theorem OAI.Erdos3.fixedKernelMixture_lipschitz line 68
  6. theorem OAI.Erdos3.fixedKernelMixture_difference_le line 96
  7. theorem OAI.Erdos3.fixedKernelMixture_abs_le line 111
  8. theorem OAI.Erdos3.fixedKernelMixture_lipschitzOn line 123