OAI/Combinatorics/StripMass/DensityExhaustion.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.ordered_density_covariance_exhaustion line 13
  2. lemma OAI.CriticalStrip.positiveWindow_mono line 56
  3. lemma OAI.CriticalStrip.positiveWindow_cover line 61
  4. theorem OAI.CriticalStrip.ordered_density_covariance_Ioi line 79
  5. lemma OAI.CriticalStrip.boundedWindow_mono line 100
  6. lemma OAI.CriticalStrip.boundedWindow_cover line 108
  7. theorem OAI.CriticalStrip.ordered_density_covariance_Ioo line 130
  8. lemma OAI.CriticalStrip.weighted_covariance_normalize line 153
  9. lemma OAI.CriticalStrip.continuousOn_laguerreWeight line 160
  10. theorem OAI.CriticalStrip.integrable_laguerreLaw_iff line 167
  11. theorem OAI.CriticalStrip.laguerreLaw_covariance line 181
  12. theorem OAI.CriticalStrip.laguerreLaw_reverse_covariance line 202
  13. lemma OAI.CriticalStrip.continuousOn_omega_Ioi line 218
  14. theorem OAI.CriticalStrip.expectation_covariance line 226
  15. lemma OAI.CriticalStrip.expectation_neg line 245
  16. theorem OAI.CriticalStrip.expectation_reverse_covariance line 251
  17. theorem OAI.CriticalStrip.laguerreLaw_increasing_tilt line 267
  18. theorem OAI.CriticalStrip.laguerreLaw_covariance_antitone line 281
  19. def OAI.CriticalStrip.cutoffRamp line 299
  20. lemma OAI.CriticalStrip.cutoffRamp_bounds line 301
  21. lemma OAI.CriticalStrip.continuous_cutoffRamp line 305
  22. lemma OAI.CriticalStrip.antitone_cutoffRamp line 309
  23. lemma OAI.CriticalStrip.cutoffRamp_tendsto line 314
  24. def OAI.CriticalStrip.cutoffEvent line 335
  25. def OAI.CriticalStrip.cutoffProduct line 337
  26. lemma OAI.CriticalStrip.measurableSet_cutoffEvent line 340
  27. lemma OAI.CriticalStrip.cutoffProduct_bounds line 343
  28. lemma OAI.CriticalStrip.cutoffProduct_norm_le line 349
  29. lemma OAI.CriticalStrip.continuous_cutoffProduct line 354
  30. lemma OAI.CriticalStrip.antitone_cutoffProduct line 358
  31. lemma OAI.CriticalStrip.cutoffProduct_tendsto line 363
  32. lemma OAI.CriticalStrip.cutoffProduct_integrable line 378
  33. lemma OAI.CriticalStrip.cutoffProduct_integral_tendsto line 383
  34. lemma OAI.CriticalStrip.cutoffProduct_weighted_tendsto line 392
  35. theorem OAI.CriticalStrip.laguerreLaw_cutoff_covariance line 411