OAI/NumberTheory/Jacobsthal/Probability/ArrivalKernelGeometry.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos970.NumberTheoryLean.KernelWeightTransform.PositiveWeight line 18
  2. instance OAI.Erdos970.NumberTheoryLean.KernelWeightTransform.(instance at line 24) line 24
  3. theorem OAI.Erdos970.NumberTheoryLean.KernelWeightTransform.ratio_measurable line 26
  4. theorem OAI.Erdos970.NumberTheoryLean.KernelWeightTransform.ratio_ne_top line 30
  5. theorem OAI.Erdos970.NumberTheoryLean.KernelWeightTransform.ratio_cocycle line 33
  6. def OAI.Erdos970.NumberTheoryLean.KernelWeightTransform.conjugate line 40
  7. instance OAI.Erdos970.NumberTheoryLean.KernelWeightTransform.conjugate_isSFiniteKernel line 43
  8. instance OAI.Erdos970.NumberTheoryLean.KernelWeightTransform.kernelPower_isSFiniteKernel line 46
  9. theorem OAI.Erdos970.NumberTheoryLean.KernelWeightTransform.conjugate_apply line 55
  10. theorem OAI.Erdos970.NumberTheoryLean.KernelWeightTransform.conjugate_lintegral line 59
  11. theorem OAI.Erdos970.NumberTheoryLean.KernelWeightTransform.conjugate_id line 64
  12. theorem OAI.Erdos970.NumberTheoryLean.KernelWeightTransform.conjugate_comp line 72
  13. theorem OAI.Erdos970.NumberTheoryLean.KernelWeightTransform.conjugate_congr line 93
  14. theorem OAI.Erdos970.NumberTheoryLean.KernelWeightTransform.conjugate_pow line 98
  15. theorem OAI.Erdos970.NumberTheoryLean.KernelWeightTransform.conjugate_pow_lintegral line 110
  16. theorem OAI.Erdos970.NumberTheoryLean.KernelWeightTransform.conjugate_prefix_sum line 123
  17. theorem OAI.Erdos970.NumberTheoryLean.KernelExitBarrier.restrict_inner_comp line 148
  18. theorem OAI.Erdos970.NumberTheoryLean.KernelExitBarrier.restricted_pow_eq line 161
  19. theorem OAI.Erdos970.NumberTheoryLean.KernelExitBarrier.restricted_future_sum line 176
  20. theorem OAI.Erdos970.NumberTheoryLean.KernelExitBarrier.conjugate_restrict line 187
  21. theorem OAI.Erdos970.NumberTheoryLean.KernelMappedDomination.mapped_pow_lintegral_le line 208
  22. theorem OAI.Erdos970.NumberTheoryLean.KernelMappedDomination.mapped_pow_le line 233
  23. theorem OAI.Erdos970.NumberTheoryLean.KernelMappedDomination.mapped_prefix_sum_le line 244
  24. theorem OAI.Erdos970.NumberTheoryLean.KernelMappedDomination.mapped_pow_lintegral_eq line 252
  25. theorem OAI.Erdos970.NumberTheoryLean.KernelMappedDomination.mapped_pow_eq line 276
  26. def OAI.Erdos970.NumberTheoryLean.HarmonicWeightKernel.harmonicWeight line 299
  27. def OAI.Erdos970.NumberTheoryLean.HarmonicWeightKernel.harmonicKernel line 307
  28. instance OAI.Erdos970.NumberTheoryLean.HarmonicWeightKernel.harmonicKernel_isSFiniteKernel line 309
  29. theorem OAI.Erdos970.NumberTheoryLean.HarmonicWeightKernel.exp_neg_two_cost line 311
  30. theorem OAI.Erdos970.NumberTheoryLean.HarmonicWeightKernel.transition_weight_ratio line 320
  31. def OAI.Erdos970.NumberTheoryLean.HarmonicWeightKernel.correction line 333
  32. theorem OAI.Erdos970.NumberTheoryLean.HarmonicWeightKernel.weight_measurable line 336
  33. theorem OAI.Erdos970.NumberTheoryLean.HarmonicWeightKernel.correction_measurable line 341
  34. def OAI.Erdos970.NumberTheoryLean.HarmonicWeightKernel.harmonicRatioDensity line 345
  35. theorem OAI.Erdos970.NumberTheoryLean.HarmonicWeightKernel.harmonicRatioDensity_measurable line 348
  36. theorem OAI.Erdos970.NumberTheoryLean.HarmonicWeightKernel.corrected_density_eq line 351
  37. theorem OAI.Erdos970.NumberTheoryLean.HarmonicWeightKernel.initial_weight_inv line 369
  38. theorem OAI.Erdos970.NumberTheoryLean.HarmonicWeightKernel.harmonic_prefix_lintegral line 373
  39. def OAI.Erdos970.NumberTheoryLean.HarmonicWeightKernel.harmonicOccupation line 379
  40. instance OAI.Erdos970.NumberTheoryLean.HarmonicWeightKernel.harmonicOccupation_isSFiniteKernel line 381
  41. theorem OAI.Erdos970.NumberTheoryLean.HarmonicWeightKernel.inclusiveOccupation_eq_prefix_sum line 385
  42. theorem OAI.Erdos970.NumberTheoryLean.HarmonicWeightKernel.harmonicOccupation_transform line 391
  43. theorem OAI.Erdos970.NumberTheoryLean.HarmonicKernelDensities.harmonic_even_typed line 409
  44. theorem OAI.Erdos970.NumberTheoryLean.HarmonicKernelDensities.harmonic_odd_typed line 424
  45. def OAI.Erdos970.NumberTheoryLean.HarmonicKernelDensities.evenUpdateReal line 439
  46. def OAI.Erdos970.NumberTheoryLean.HarmonicKernelDensities.oddUpdateReal line 440
  47. theorem OAI.Erdos970.NumberTheoryLean.HarmonicKernelDensities.evenUpdateReal_measurable line 442
  48. theorem OAI.Erdos970.NumberTheoryLean.HarmonicKernelDensities.oddUpdateReal_measurable line 445
  49. theorem OAI.Erdos970.NumberTheoryLean.HarmonicKernelDensities.harmonic_even_joint_lintegral line 448
  50. theorem OAI.Erdos970.NumberTheoryLean.HarmonicKernelDensities.harmonic_odd_joint_lintegral line 468
  51. theorem OAI.Erdos970.NumberTheoryLean.HarmonicKernelDensities.harmonic_even_measure line 488
  52. theorem OAI.Erdos970.NumberTheoryLean.HarmonicKernelDensities.harmonic_odd_measure line 500
  53. def OAI.Erdos970.NumberTheoryLean.ArrivalKernelGeometry.currentExponent line 526
  54. theorem OAI.Erdos970.NumberTheoryLean.ArrivalKernelGeometry.gapValue_measurable line 528
  55. theorem OAI.Erdos970.NumberTheoryLean.ArrivalKernelGeometry.currentExponent_measurable line 531
  56. theorem OAI.Erdos970.NumberTheoryLean.ArrivalKernelGeometry.currentExponent_pos line 534
  57. def OAI.Erdos970.NumberTheoryLean.ArrivalKernelGeometry.arrivalSet line 537
  58. theorem OAI.Erdos970.NumberTheoryLean.ArrivalKernelGeometry.arrivalSet_measurable line 539
  59. theorem OAI.Erdos970.NumberTheoryLean.ArrivalKernelGeometry.arrivalSet_eq_cutoff line 542
  60. theorem OAI.Erdos970.NumberTheoryLean.ArrivalKernelGeometry.gapValue_update line 548
  61. theorem OAI.Erdos970.NumberTheoryLean.ArrivalKernelGeometry.currentExponent_update line 554
  62. theorem OAI.Erdos970.NumberTheoryLean.ArrivalKernelGeometry.stateKernel_ae_minRatio line 559
  63. theorem OAI.Erdos970.NumberTheoryLean.ArrivalKernelGeometry.costKernel_gap_flow line 575
  64. theorem OAI.Erdos970.NumberTheoryLean.ArrivalKernelGeometry.costKernel_exponent_nonincreasing line 588
  65. theorem OAI.Erdos970.NumberTheoryLean.ArrivalKernelGeometry.harmonicKernel_absolutelyContinuous line 600
  66. theorem OAI.Erdos970.NumberTheoryLean.ArrivalKernelGeometry.harmonicKernel_gap_flow line 603
  67. theorem OAI.Erdos970.NumberTheoryLean.ArrivalKernelGeometry.harmonicKernel_exponent_nonincreasing line 607
  68. theorem OAI.Erdos970.NumberTheoryLean.ArrivalKernelGeometry.costKernel_no_reentry line 611
  69. theorem OAI.Erdos970.NumberTheoryLean.ArrivalKernelGeometry.harmonicKernel_no_reentry line 619