OAI/NumberTheory/DukePrimeDegree/Dynamics/LeafFlowCovariance.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Joint almost-everywhere leaf covariance for the shearing flow

The fixed-time covariance theorem alone does not justify using a time selected from a recurrence argument. Measurable kernels and a countable determining family of leaf tests allow Fubini to put the time quantifier inside: almost every initial point has covariance at almost every real time. This is sufficient for selection after finitely many affine time changes, without asserting an unproved pointwise equivariant version.

  1. def OAI.DukePrimeDegree.rescaledRealKernel line 24
  2. def OAI.DukePrimeDegree.normalizedRescaledRealKernel line 37
  3. lemma OAI.DukePrimeDegree.normalized_scaling_locallyFinite line 48
  4. def OAI.DukePrimeDegree.rootPairCovarianceKernel line 65
  5. lemma OAI.DukePrimeDegree.rootPairCovarianceKernel_apply line 74
  6. theorem OAI.DukePrimeDegree.ae_rootPairKernel_covariance_fixed line 84
  7. theorem OAI.DukePrimeDegree.ae_rootPairKernel_covariance_time line 113