OAI/NumberTheory/DirichletL/Detector/PrincipalTransport.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SevenEighths.ProbePrincipalTransport.gaussianMoment_tendsto line 16
  2. lemma OAI.SevenEighths.ProbePrincipalTransport.gaussianMoment_even line 27
  3. lemma OAI.SevenEighths.ProbePrincipalTransport.gaussianMoment_tendsto_bot line 30
  4. lemma OAI.SevenEighths.ProbePrincipalTransport.shifted_gaussian_integrable line 34
  5. lemma OAI.SevenEighths.ProbePrincipalTransport.shifted_gaussian_top line 38
  6. lemma OAI.SevenEighths.ProbePrincipalTransport.shifted_gaussian_bottom line 42
  7. theorem OAI.SevenEighths.ProbePrincipalTransport.verticalIntegral_eq_of_shifted_gaussian line 51
  8. theorem OAI.SevenEighths.ProbePrincipalTransport.principal_box_majorant line 78
  9. theorem OAI.SevenEighths.ProbePrincipalTransport.continued_x_shift line 129
  10. lemma OAI.SevenEighths.ProbePrincipalTransport.continued_source_differentiable_z line 154
  11. lemma OAI.SevenEighths.ProbePrincipalTransport.continued_principal_differentiable_z line 176
  12. theorem OAI.SevenEighths.ProbePrincipalTransport.continued_z_shift line 194
  13. lemma OAI.SevenEighths.ProbePrincipalTransport.verticalIntegral_swap line 225
  14. lemma OAI.SevenEighths.ProbePrincipalTransport.verticalIntegral_triple_reverse line 233
  15. lemma OAI.SevenEighths.ProbePrincipalTransport.verticalIntegral_congr_line line 250
  16. theorem OAI.SevenEighths.ProbePrincipalTransport.continued_triple_x_shift line 256
  17. theorem OAI.SevenEighths.ProbePrincipalTransport.continued_triple_z_shift line 283
  18. lemma OAI.SevenEighths.ProbePrincipalTransport.continued_triple_eq_raw line 312
  19. theorem OAI.SevenEighths.ProbePrincipalTransport.source_initial_placement line 330
  20. theorem OAI.SevenEighths.ProbePrincipalTransport.source_initial_ordered_at_a line 353
  21. lemma OAI.SevenEighths.ProbePrincipalTransport.continued_principal_measurable line 375
  22. lemma OAI.SevenEighths.ProbePrincipalTransport.strip_integrable_of_uniform_slices line 407
  23. theorem OAI.SevenEighths.ProbePrincipalTransport.uniform_high_x_joins line 435
  24. theorem OAI.SevenEighths.ProbePrincipalTransport.uniform_high_z_joins line 487
  25. lemma OAI.SevenEighths.ProbePrincipalTransport.high_x_join_ae_raw line 539
  26. lemma OAI.SevenEighths.ProbePrincipalTransport.high_z_join_ae_raw line 559
  27. theorem OAI.SevenEighths.ProbePrincipalTransport.raw_uniform_high_x_joins line 580
  28. theorem OAI.SevenEighths.ProbePrincipalTransport.raw_uniform_high_z_joins line 608
  29. theorem OAI.SevenEighths.ProbePrincipalTransport.source_initial_joint_ordered_at_a line 635