OAI/Combinatorics/HoneycombChords/StripGram.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Beta kernel moments and positive strip Gram determinants.

  1. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripDensity line 10
  2. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripDensity_pos line 11
  3. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripDensity_bound line 15
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_pair_integrable line 24
  5. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetGram line 58
  6. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetPointDensity line 61
  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weighted_jet_evaluation line 63
  8. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jet_gram_andreief line 73
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetPointDensity_pos line 98
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetGram_det_pos line 110
  11. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_pair_moment_integrable line 163
  12. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.strip_label_margin line 194
  13. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.strip_jet_pair_moment_integrable line 209
  14. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.strip_jet_pair_integrable line 215
  15. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.strip_jet_gram_det_pos line 220
  16. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.poleAdjustedDensity line 228
  17. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.poleAdjustedDensity_pos line 229
  18. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pole_adjusted_pair_moment_integrable line 231
  19. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pole_adjusted_gram_det_pos line 252
  20. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetPencil line 268
  21. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.characteristicRatio line 270
  22. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetPointDensity_tilt line 271
  23. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pole_jet_pair_pencil_integrable line 275
  24. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetPencil_affine line 285
  25. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pole_jetPencil_det_pos_nonpos line 301
  26. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pole_jetPencil_real_root_positive line 311
  27. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pole_pencil_restore_weight line 319
  28. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pole_pencil_tilt_weight line 326
  29. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.strip_jet_characteristic_product line 333