OAI/NumberTheory/DukePrimeDegree/Dynamics/DiagonalRecurrence.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Vanishing of expanding scalar coordinates in a finite invariant law

This is the scalar step in diagonal recurrence on projective or Grassmannian coordinates. Bounded monotone truncation avoids assuming that the original coordinate is integrable. It will be applied to ratios of unequal diagonal weights; no stabilizer or orbit conclusion is assumed.

  1. def OAI.DukePrimeDegree.boundedAbsCoordinate line 21
  2. lemma OAI.DukePrimeDegree.boundedAbsCoordinate_nonneg line 23
  3. lemma OAI.DukePrimeDegree.boundedAbsCoordinate_le_one line 26
  4. lemma OAI.DukePrimeDegree.boundedAbsCoordinate_mono line 30
  5. lemma OAI.DukePrimeDegree.boundedAbsCoordinate_strictMono line 36
  6. theorem OAI.DukePrimeDegree.ae_eq_zero_of_expanding_covariance line 44

    Source documentation

    An a.e. expanding scalar coordinate must vanish under a finite invariant measure. The scalar coordinate itself need not be integrable.

    theorem ae_eq_zero_of_expanding_covariance
    {Y : Type*} [MeasurableSpace Y]
    (μ : Measure Y) [IsFiniteMeasure μ]
    (T : Y → Y) (hT : MeasurePreserving T μ μ)
    (f : Y → ℝ) (hf : Measurable f) (c : ℝ) (hc : 1 < c)
    (hcov : (fun x => f (T x)) =ᵐ[μ] fun x => c * f x) :
    f =ᵐ[μ] 0 := by
…