OAI/NumberTheory/DukePrimeDegree/Dynamics/ShearingTimeCovariance.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Choosing recurrence times with leaf covariance

Finitely many affine pullbacks of a Lebesgue null exceptional set are null. Thus the two-point, two-scale recurrence selection can enforce the actual leaf covariance identities at every selected time.

  1. lemma OAI.DukePrimeDegree.ae_affine_precompose line 21
  2. theorem OAI.DukePrimeDegree.exists_common_two_scale_time_ae line 28
  3. theorem OAI.DukePrimeDegree.exists_common_two_scale_time_with_covariance line 54