OAI/Combinatorics/SumProduct/Alignment/MicrocellScale01.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SourcePointLaw.beta_integrand_continuous line 28
  2. def OAI.SourcePointLaw.empiricalLaw line 42
  3. lemma OAI.SourcePointLaw.integral_empiricalLaw line 48
  4. theorem OAI.SourcePointLaw.empirical_tendsto_betaMixture line 73
  5. lemma OAI.MicrocellProbability.weight_pos line 124
  6. def OAI.MicrocellProbability.weightedLaw line 128
  7. def OAI.MicrocellProbability.uniformLaw line 136
  8. lemma OAI.MicrocellProbability.weightedLaw_apply line 139
  9. lemma OAI.MicrocellProbability.uniformLaw_apply line 153
  10. theorem OAI.MicrocellProbability.harmonic_event_error line 169
  11. theorem OAI.MicrocellProbability.harmonic_success line 180
  12. lemma OAI.MicrocellProbability.empiricalLaw_eq line 188
  13. def OAI.MicrocellScale.radius line 207
  14. def OAI.MicrocellScale.length line 208
  15. lemma OAI.MicrocellScale.modulus_dvd line 210
  16. lemma OAI.MicrocellScale.length_eq line 211
  17. lemma OAI.MicrocellScale.radius_le line 214
  18. lemma OAI.MicrocellScale.radius_gt line 220
  19. lemma OAI.MicrocellScale.radius_half_sqrt line 229
  20. lemma OAI.MicrocellScale.sqrt_ratio line 235
  21. def OAI.MicrocellScale.Dominates line 243
  22. lemma OAI.MicrocellScale.sqrt_dominates line 246
  23. theorem OAI.MicrocellScale.radius_dominates line 257
  24. theorem OAI.MicrocellScale.boundary_rate line 281
  25. theorem OAI.MicrocellScale.endpoint_rate line 309