OAI/NumberTheory/PrimePackets/KernelScaling.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PrimeDegreePackets.scaleBaseKernel line 69
  2. lemma OAI.PrimeDegreePackets.scaleBaseKernel_apply line 76
  3. lemma OAI.PrimeDegreePackets.scaleBaseKernel_finite line 79
  4. lemma OAI.PrimeDegreePackets.compProd_scaleBaseKernel line 88
  5. lemma OAI.PrimeDegreePackets.compProd_restrict_rectangle line 97
  6. lemma OAI.PrimeDegreePackets.fst_compProd_withDensity line 116
  7. lemma OAI.PrimeDegreePackets.restricted_conditional_marginal line 126
  8. theorem OAI.PrimeDegreePackets.restricted_conditional_kernel line 140
  9. def OAI.PrimeDegreePackets.RootBox.shrink line 170
  10. theorem OAI.PrimeDegreePackets.RootBox.shrink_coordinateMeasure line 178
  11. theorem OAI.PrimeDegreePackets.RootBox.shrink_conditionalKernel line 192
  12. theorem OAI.PrimeDegreePackets.RootBox.shrink_marginal line 205
  13. lemma OAI.PrimeDegreePackets.transitive_eigenfunction_ne_zero line 220
  14. theorem OAI.PrimeDegreePackets.transitive_eigencharacter_pow_card line 234
  15. theorem OAI.PrimeDegreePackets.odd_transitive_quadratic_eigencharacter_trivial line 248
  16. lemma OAI.PrimeDegreePackets.localHomeomorph_collision_free_isOpen line 267
  17. theorem OAI.PrimeDegreePackets.compact_injective_localHomeomorph_neighborhood line 287
  18. lemma OAI.PrimeDegreePackets.root_time_injective_of_free line 309
  19. theorem OAI.PrimeDegreePackets.rootBox_contains_compact_time line 328
  20. theorem OAI.PrimeDegreePackets.rootBox_arbitrary_length_of_free line 352
  21. theorem OAI.PrimeDegreePackets.ae_rootBox_arbitrary_length line 372
  22. lemma OAI.PrimeDegreePackets.measure_eq_of_ae_local_restrict_eq line 392
  23. theorem OAI.PrimeDegreePackets.homeomorph_measurePreserving_of_ae_local line 410
  24. def OAI.PrimeDegreePackets.RootBox.HasHaarConditionals line 440
  25. lemma OAI.PrimeDegreePackets.RootBox.coordinateMeasure_of_haarConditionals line 444
  26. def OAI.PrimeDegreePackets.RootBox.timeTranslation line 458
  27. lemma OAI.PrimeDegreePackets.RootBox.timeTranslation_apply line 461
  28. lemma OAI.PrimeDegreePackets.RootBox.prod_volume_timeTranslation_invariant line 464
  29. theorem OAI.PrimeDegreePackets.RootBox.coordinateMeasure_translate_of_haar line 476