OAI/NumberTheory/Jacobsthal/Probability/ThirdInnerKernel.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.ErdosOmissionBindings.lossTwo_measurable line 14
  2. theorem OAI.Erdos970.ErdosOmissionBindings.lossTwo_bound line 18
  3. theorem OAI.Erdos970.ErdosOmissionBindings.actual_second_loss_eq_L2 line 42
  4. theorem OAI.Erdos970.ErdosOmissionBindings.lossThree_bound line 58
  5. def OAI.Erdos970.ErdosOmissionBindings.clampedThird line 80
  6. theorem OAI.Erdos970.ErdosOmissionBindings.clampedThird_eq line 83
  7. theorem OAI.Erdos970.ErdosOmissionBindings.clampedThird_bound line 88
  8. theorem OAI.Erdos970.ErdosOmissionBindings.clampedThird_continuous line 91
  9. theorem OAI.Erdos970.ErdosOmissionBindings.baseCutoff_continuous line 105
  10. theorem OAI.Erdos970.ErdosOmissionBindings.odd_gate_indicator line 118
  11. theorem OAI.Erdos970.ErdosOmissionBindings.gate_force_bounds line 144
  12. def OAI.Erdos970.ErdosOmissionBindings.thirdKernel line 161
  13. theorem OAI.Erdos970.ErdosOmissionBindings.thirdKernel_measurable line 164
  14. theorem OAI.Erdos970.ErdosOmissionBindings.thirdKernel_bound line 171
  15. theorem OAI.Erdos970.ErdosOmissionBindings.third_density_kernel line 186
  16. def OAI.Erdos970.ErdosOmissionBindings.thirdInnerKernel line 206
  17. theorem OAI.Erdos970.ErdosOmissionBindings.thirdInnerKernel_continuous line 209
  18. theorem OAI.Erdos970.ErdosOmissionBindings.thirdInnerKernel_bound line 218
  19. theorem OAI.Erdos970.ErdosOmissionBindings.third_even_gate line 231