OAI/Combinatorics/StripMass/PfaffianConfluentLimit.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.StripPfaffian.pfaffian_confluent_limit line 13
  2. theorem OAI.CriticalStrip.rho_pos line 53
  3. theorem OAI.CriticalStrip.c_pos line 57
  4. theorem OAI.CriticalStrip.archWeight_nonneg line 61
  5. theorem OAI.CriticalStrip.bridgeWeight_nonneg line 69
  6. theorem OAI.CriticalStrip.K_nonneg line 77
  7. theorem OAI.CriticalStrip.bridgeKernel_nonneg line 80
  8. theorem OAI.CriticalStrip.archMass_nonneg line 83
  9. theorem OAI.CriticalStrip.bridgeMass_nonneg line 86
  10. theorem OAI.CriticalStrip.moment_nonneg line 89
  11. theorem OAI.CriticalStrip.K_zero line 92
  12. theorem OAI.CriticalStrip.IsPath.mono line 96
  13. theorem OAI.CriticalStrip.archWeight_mono line 102
  14. theorem OAI.CriticalStrip.K_le_of_summable line 113
  15. theorem OAI.CriticalStrip.archMass_le_of_finite line 119
  16. theorem OAI.CriticalStrip.moment_le_of_finite line 126
  17. theorem OAI.CriticalStrip.bridgeMass_le_of_finite_and_flux line 138
  18. theorem OAI.CriticalStrip.sum_increment_bounds line 147
  19. theorem OAI.CriticalStrip.comparable_of_antitone_increments line 177
  20. theorem OAI.CriticalStrip.criticalStripMass_iff_four_estimates line 258
  21. theorem OAI.CriticalStrip.reflection_deficit_bounds line 279
  22. theorem OAI.CriticalStrip.reflection_deficit_lower line 304
  23. theorem OAI.CriticalStrip.rpow_le_eight_omega line 326
  24. def OAI.CriticalStrip.pointwiseArchIntegrand line 361
  25. def OAI.CriticalStrip.pointwiseArchIntegral line 364
  26. theorem OAI.CriticalStrip.measurable_pointwiseArchIntegrand line 367
  27. theorem OAI.CriticalStrip.pointwiseArchIntegrand_bounds line 372
  28. theorem OAI.CriticalStrip.integrableOn_pointwiseArchIntegrand line 398