DiagonalProjectiveRecurrence.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Finite invariant projective laws of a positive diagonal map

This is a coordinate form of diagonal recurrence. A measurable nonzero representative may change by an arbitrary nonzero scalar under the dynamics. Ratios cancel that scalar. Unequal positive diagonal weights cannot both occur in the support of a representative almost everywhere. The conclusion is an actual eigenline statement, not an orbit hypothesis.

lemma OAI.DukePrimeDegree.ratio_of_common_nonzero_scalar line 21
theorem OAI.DukePrimeDegree.ae_coordinate_zero_or_zero_of_diagonal_weights line 28

theorem OAI.DukePrimeDegree.ae_diagonal_projective_single_weight line 52

Source documentation

Unequal weights do not coexist in a nonzero projective coordinate representative. Only countably many coordinates are needed.

theorem ae_diagonal_projective_single_weight
    {Y I : Type*} [MeasurableSpace Y] [Countable I]
    (μ : Measure Y) [IsFiniteMeasure μ]
    (T : Y → Y) (hT : MeasurePreserving T μ μ)
    (w : Y → I → ℝ) (hw : ∀ i, Measurable (fun x => w x i))
    (a : I → ℝ) (ha : ∀ i, 0 < a i)
    (r : Y → ℝ) (hr : ∀ᵐ x ∂μ, r x ≠ 0)
    (hcov : ∀ i, (fun x => w (T x) i) =ᵐ[μ] fun x => r x * a i * w x i) :
    ∀ᵐ x ∂μ, ∀ i j, a i ≠ a j → w x i = 0 ∨ w x j = 0 := by
…

theorem OAI.DukePrimeDegree.ae_diagonal_projective_eigenline line 75

Source documentation

The projective representative lies in one genuine eigenspace of the positive diagonal operator almost everywhere.

theorem ae_diagonal_projective_eigenline
    {Y I : Type*} [MeasurableSpace Y] [Countable I]
    (μ : Measure Y) [IsFiniteMeasure μ]
    (T : Y → Y) (hT : MeasurePreserving T μ μ)
    (w : Y → I → ℝ) (hw : ∀ i, Measurable (fun x => w x i))
    (hne : ∀ᵐ x ∂μ, ∃ i, w x i ≠ 0)
    (a : I → ℝ) (ha : ∀ i, 0 < a i)
    (r : Y → ℝ) (hr : ∀ᵐ x ∂μ, r x ≠ 0)
    (hcov : ∀ i, (fun x => w (T x) i) =ᵐ[μ] fun x => r x * a i * w x i) :
    ∀ᵐ x ∂μ, ∃ c : ℝ, 0 < c ∧ ∀ i, a i * w x i = c * w x i := by
…