OAI/NumberTheory/PrimePackets/LeafSupport.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.real_mem_measureSupport_iff_rat line 115
  2. lemma OAI.PrimeDegreePackets.measurableSet_kernel_support line 130
  3. theorem OAI.PrimeDegreePackets.RootBox.ae_mem_leafMeasure_support line 145
  4. theorem OAI.PrimeDegreePackets.RootBox.ae_leafMeasure_ball_pos line 170
  5. lemma OAI.PrimeDegreePackets.isSFiniteKernel_of_pointwise_finite line 189
  6. lemma OAI.PrimeDegreePackets.isSFiniteKernel_of_finite_exhaustion line 223
  7. def OAI.PrimeDegreePackets.finiteRealWindows line 243
  8. lemma OAI.PrimeDegreePackets.measurableSet_finiteRealWindows line 246
  9. lemma OAI.PrimeDegreePackets.locallyFinite_of_finite_real_windows line 253
  10. def OAI.PrimeDegreePackets.locallyFiniteRealVersion line 265
  11. lemma OAI.PrimeDegreePackets.locallyFiniteRealVersion_eq line 268
  12. instance OAI.PrimeDegreePackets.locallyFiniteRealVersion_locallyFinite line 274
  13. instance OAI.PrimeDegreePackets.locallyFiniteRealVersion_sFinite line 281
  14. def OAI.PrimeDegreePackets.RootBox.regularLeafKernel line 292
  15. instance OAI.PrimeDegreePackets.RootBox.regularLeafKernel_locallyFinite line 299
  16. instance OAI.PrimeDegreePackets.RootBox.regularLeafKernel_sFinite line 307
  17. lemma OAI.PrimeDegreePackets.RootBox.ae_regularLeafKernel_eq line 314
  18. def OAI.PrimeDegreePackets.centerRealMeasure line 332
  19. lemma OAI.PrimeDegreePackets.centerRealMeasure_ball line 335
  20. instance OAI.PrimeDegreePackets.centerRealMeasure_locallyFinite line 343
  21. def OAI.PrimeDegreePackets.basedRealMeasure line 352
  22. lemma OAI.PrimeDegreePackets.basedRealMeasure_ball_one line 355
  23. lemma OAI.PrimeDegreePackets.basedRealMeasure_locallyFinite line 361
  24. def OAI.PrimeDegreePackets.centerRealKernel line 372
  25. def OAI.PrimeDegreePackets.basedRealKernel line 386
  26. def OAI.PrimeDegreePackets.RootBox.basedLeaf line 400
  27. lemma OAI.PrimeDegreePackets.RootBox.aemeasurable_basedLeaf line 403
  28. theorem OAI.PrimeDegreePackets.RootBox.ae_basedLeaf_spec line 417
  29. lemma OAI.PrimeDegreePackets.anchorNormalize_smul line 439
  30. lemma OAI.PrimeDegreePackets.anchorNormalize_restrict_comm line 447
  31. lemma OAI.PrimeDegreePackets.anchorNormalize_anchor_of_pos_finite line 453
  32. lemma OAI.PrimeDegreePackets.anchorNormalize_twice line 457
  33. lemma OAI.PrimeDegreePackets.centerRealMeasure_smul line 462
  34. lemma OAI.PrimeDegreePackets.basedRealMeasure_smul line 466
  35. lemma OAI.PrimeDegreePackets.centerRealMeasure_center line 472
  36. lemma OAI.PrimeDegreePackets.basedRealMeasure_center line 481
  37. lemma OAI.PrimeDegreePackets.basedRealMeasure_rebase line 488
  38. lemma OAI.PrimeDegreePackets.centerRealMeasure_scaling line 499
  39. lemma OAI.PrimeDegreePackets.basedRealMeasure_scaling line 512