OAI/NumberTheory/PrimePackets/RootCharts.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.PrimeDegreePackets.rootGroupMeasurableSpace line 65
  2. instance OAI.PrimeDegreePackets.rootGroupBorelSpace line 66
  3. lemma OAI.PrimeDegreePackets.rootPivot_isOpen line 68
  4. lemma OAI.PrimeDegreePackets.exists_rootPivot line 75
  5. def OAI.PrimeDegreePackets.rootCoordinateMeasure line 83
  6. instance OAI.PrimeDegreePackets.rootCoordinateMeasure_isFinite line 87
  7. def OAI.PrimeDegreePackets.rootConditionalKernel line 95
  8. instance OAI.PrimeDegreePackets.rootConditionalKernel_isMarkov line 99
  9. theorem OAI.PrimeDegreePackets.rootConditionalKernel_disintegrate line 106
  10. def OAI.PrimeDegreePackets.rootQuotientParametrization line 116
  11. lemma OAI.PrimeDegreePackets.rootQuotientParametrization_localHomeomorph line 120
  12. theorem OAI.PrimeDegreePackets.rootQuotientParametrization_localEmbedding line 129
  13. lemma OAI.PrimeDegreePackets.rootQuotientParametrization_add line 135
  14. structure OAI.PrimeDegreePackets.RootBox line 150
  15. abbrev OAI.PrimeDegreePackets.RootBox.domain line 161
  16. abbrev OAI.PrimeDegreePackets.RootBox.param line 162
  17. def OAI.PrimeDegreePackets.RootBox.range line 163
  18. lemma OAI.PrimeDegreePackets.RootBox.range_open line 165
  19. def OAI.PrimeDegreePackets.RootBox.coordinateMeasure line 169
  20. instance OAI.PrimeDegreePackets.RootBox.coordinateMeasure_finite line 173
  21. lemma OAI.PrimeDegreePackets.RootBox.map_coordinateMeasure line 182
  22. def OAI.PrimeDegreePackets.RootBox.conditionalKernel line 190
  23. instance OAI.PrimeDegreePackets.RootBox.conditionalKernel_markov line 193
  24. theorem OAI.PrimeDegreePackets.RootBox.disintegrate line 200
  25. theorem OAI.PrimeDegreePackets.exists_rootBox_at_coordinates line 208
  26. theorem OAI.PrimeDegreePackets.exists_rootBox_at line 218
  27. theorem OAI.PrimeDegreePackets.exists_countable_rootBox_cover line 232
  28. lemma OAI.PrimeDegreePackets.RootBox.coordinateMeasure_ae_domain line 247
  29. lemma OAI.PrimeDegreePackets.RootBox.coordinateMeasure_fst_ae_transverse line 254
  30. lemma OAI.PrimeDegreePackets.RootBox.conditionalKernel_ae_time line 263
  31. lemma OAI.PrimeDegreePackets.RootBox.conditionalKernel_time_mass line 272
  32. lemma OAI.PrimeDegreePackets.RootBox.coordinateMeasure_apply line 281
  33. theorem OAI.PrimeDegreePackets.RootBox.root_window_integral line 297
  34. lemma OAI.PrimeDegreePackets.compProd_map_measurableEquiv line 314
  35. lemma OAI.PrimeDegreePackets.fst_map_measurableEquiv line 332
  36. theorem OAI.PrimeDegreePackets.condKernel_map_measurableEquiv line 343
  37. lemma OAI.PrimeDegreePackets.mul_diagonalOneParameter_entry line 365
  38. def OAI.PrimeDegreePackets.rootSliceDiagonal line 371
  39. lemma OAI.PrimeDegreePackets.rootSliceDiagonal_add line 379
  40. lemma OAI.PrimeDegreePackets.rootSliceDiagonal_zero line 386
  41. def OAI.PrimeDegreePackets.rootSliceDiagonalHomeomorph line 392
  42. def OAI.PrimeDegreePackets.rootTimeScaling line 401
  43. lemma OAI.PrimeDegreePackets.rootQuotientParametrization_diagonal line 406
  44. theorem OAI.PrimeDegreePackets.root_conditional_scaling line 425
  45. abbrev OAI.PrimeDegreePackets.rootDiagonalCoordinates line 441
  46. lemma OAI.PrimeDegreePackets.rootDiagonalCoordinates_param line 446
  47. def OAI.PrimeDegreePackets.RootBox.diagonal line 456
  48. lemma OAI.PrimeDegreePackets.RootBox.diagonal_domain line 479
  49. theorem OAI.PrimeDegreePackets.RootBox.diagonal_coordinateMeasure line 486
  50. theorem OAI.PrimeDegreePackets.RootBox.diagonal_conditionalKernel line 514