OAI/NumberTheory/Jacobsthal/Probability/HarmonicPrefixKernel.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosPrimeInputs.WeightedKernelMass.mass line 19
  2. theorem OAI.Erdos970.ErdosPrimeInputs.WeightedKernelMass.mass_zero line 21
  3. lemma OAI.Erdos970.ErdosPrimeInputs.WeightedKernelMass.mass_succ line 25
  4. lemma OAI.Erdos970.ErdosPrimeInputs.WeightedKernelMass.mass_measurable line 31
  5. theorem OAI.Erdos970.ErdosPrimeInputs.WeightedKernelMass.weighted_sum_succ line 34
  6. theorem OAI.Erdos970.ErdosPrimeInputs.WeightedKernelMass.weighted_finite_bound line 48
  7. theorem OAI.Erdos970.ErdosPrimeInputs.WeightedKernelMass.weighted_total_bound line 59
  8. def OAI.Erdos970.ErdosPrimeInputs.HarmonicPrefixKernel.density line 76
  9. lemma OAI.Erdos970.ErdosPrimeInputs.HarmonicPrefixKernel.density_measurable line 79
  10. def OAI.Erdos970.ErdosPrimeInputs.HarmonicPrefixKernel.kernel line 84
  11. instance OAI.Erdos970.ErdosPrimeInputs.HarmonicPrefixKernel.kernel_isSFinite line 87
  12. theorem OAI.Erdos970.ErdosPrimeInputs.HarmonicPrefixKernel.kernel_lintegral line 94
  13. theorem OAI.Erdos970.ErdosPrimeInputs.HarmonicPrefixKernel.kernel_eq_restrict line 102
  14. lemma OAI.Erdos970.ErdosPrimeInputs.HarmonicPrefixKernel.kernel_eq_zero line 110
  15. def OAI.Erdos970.ErdosPrimeInputs.HarmonicPrefixKernel.bound line 114
  16. def OAI.Erdos970.ErdosPrimeInputs.HarmonicPrefixKernel.boundE line 115
  17. lemma OAI.Erdos970.ErdosPrimeInputs.HarmonicPrefixKernel.bound_measurable line 117
  18. lemma OAI.Erdos970.ErdosPrimeInputs.HarmonicPrefixKernel.boundE_measurable line 120
  19. lemma OAI.Erdos970.ErdosPrimeInputs.HarmonicPrefixKernel.bound_on line 123
  20. lemma OAI.Erdos970.ErdosPrimeInputs.HarmonicPrefixKernel.bound_below line 126
  21. lemma OAI.Erdos970.ErdosPrimeInputs.HarmonicPrefixKernel.harmonic_bound_integral line 129
  22. theorem OAI.Erdos970.ErdosPrimeInputs.HarmonicPrefixKernel.schur_one line 148
  23. theorem OAI.Erdos970.ErdosPrimeInputs.HarmonicPrefixKernel.total_prefix_mass line 163