OAI/Combinatorics/StripMass/NorthMass.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.sum_subtype_indicator line 14
  2. def OAI.CriticalStrip.NorthHistory.Valid line 22
  3. def OAI.CriticalStrip.NorthHistory.pairEquiv line 28
  4. lemma OAI.CriticalStrip.NorthHistory.weighted_valid line 35
  5. lemma OAI.CriticalStrip.NorthHistory.sum_weight_pairings line 80
  6. lemma OAI.CriticalStrip.NorthHistory.sum_weight_source line 103
  7. instance OAI.CriticalStrip.NorthHistory.boundedFintype line 117
  8. lemma OAI.CriticalStrip.NorthHistory.sum_weight_cross line 120
  9. lemma OAI.CriticalStrip.Diagram.column_pow_empty_empty line 137
  10. lemma OAI.CriticalStrip.Diagram.column_pow_empty_nonempty line 148
  11. theorem OAI.CriticalStrip.Diagram.column_pow_empty_tendsto line 170
  12. lemma OAI.CriticalStrip.Diagram.physical_augmented_stationary line 179
  13. lemma OAI.CriticalStrip.Diagram.reversed_augmented_stationary line 188
  14. lemma OAI.CriticalStrip.Diagram.physical_empty_tendsto_source line 197
  15. lemma OAI.CriticalStrip.Diagram.reversed_empty_tendsto_source line 206
  16. lemma OAI.CriticalStrip.NorthHistory.mass_tendsto line 229
  17. lemma OAI.CriticalStrip.CrossTopArch.weight_nonneg line 246
  18. lemma OAI.CriticalStrip.CrossTopArch.Fits.mono line 253
  19. def OAI.CriticalStrip.CrossTopArch.window line 256
  20. lemma OAI.CriticalStrip.CrossTopArch.mem_window line 259
  21. lemma OAI.CriticalStrip.CrossTopArch.window_tendsto line 264
  22. lemma OAI.CriticalStrip.CrossTopArch.window_mass line 276
  23. theorem OAI.CriticalStrip.CrossTopArch.summable_weight line 283
  24. theorem OAI.CriticalStrip.CrossTopArch.tsum_weight line 295
  25. lemma OAI.CriticalStrip.TopArchConfiguration.weight_nonneg line 317
  26. lemma OAI.CriticalStrip.TopArchConfiguration.weight_sum line 323
  27. lemma OAI.CriticalStrip.TopArchConfiguration.summable_weight_iff line 331
  28. def OAI.CriticalStrip.CrossTopArch.sigmaEquiv line 346
  29. lemma OAI.CriticalStrip.CrossTopArch.summable_sigma line 353
  30. lemma OAI.CriticalStrip.CrossTopArch.sigma_sums line 358
  31. theorem OAI.CriticalStrip.archWeight_summable_positive line 374
  32. theorem OAI.CriticalStrip.archWeight_summable line 382
  33. theorem OAI.CriticalStrip.moment_summable line 397
  34. theorem OAI.CriticalStrip.moment_eq_realNorthSeparator line 404
  35. theorem OAI.CriticalStrip.physical_arch_formula line 424
  36. theorem OAI.CriticalStrip.physical_moment_growth line 430