KernelVelocityRecurrence.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Diagonal recurrence for actual component velocity spaces

The kernel covariance is the equality supplied by the normalizer ergodic decomposition. The velocity space and its measurable frame are constructed from the kernel, rather than supplied as extra geometric data. Recurrence is applied separately on its measurable rank events, and gives invariance of the actual velocity space.

lemma OAI.DukePrimeDegree.span_columns_mul_le line 24
lemma OAI.DukePrimeDegree.diagonal_mem_span_of_frame_invariance line 33
lemma OAI.DukePrimeDegree.coordinate_velocitySpace_transport line 48

theorem OAI.DukePrimeDegree.ae_kernel_velocity_diagonal_stable line 72

Source documentation

Covariance under one actual diagonal translation forces the actual kernel velocity space to be stable under its adjoint map almost surely. This uses no ergodicity of that individual translation.

theorem ae_kernel_velocity_diagonal_stable
    {Z : Type*} [MeasurableSpace Z] {n : ℕ} [Nonempty (Fin n)]
    (τ : Measure Z) [IsFiniteMeasure τ]
    (κ : Kernel Z (X n)) [IsMarkovKernel κ]
    (T : Z → Z) (hT : MeasurePreserving T τ τ)
    (ell : Fin n → ℝ) (hell : ∑ i, ell i = 0)
    (hcov : ∀ᵐ z ∂τ,
      (κ z).map (fun x => rightAction x (diagonalOneParameter ell hell (-1))) = κ (T z)) :
    ∀ᵐ z ∂τ, ∀ V ∈ matrixVelocitySpace (invariantRightSubgroup (κ z)),
      (diagonalOneParameter ell hell 1).val * V *
        (diagonalOneParameter ell hell (-1)).val ∈
          matrixVelocitySpace (invariantRightSubgroup (κ z)) := by
…

Mentions: OAI.DukePrimeDegree.matrixVelocitySpace

theorem OAI.DukePrimeDegree.ae_conditional_velocity_diagonal_stable line 132

Source documentation

The preceding recurrence applies to the actual invariant-sigma conditional measures. Normalizer covariance and preservation of their base law are the proved decomposition statements, not new hypotheses.

theorem ae_conditional_velocity_diagonal_stable
    {n : ℕ} [Nonempty (Fin n)]
    (H : Subgroup (G n)) (μ : Measure (X n)) [IsProbabilityMeasure μ]
    (ell : Fin n → ℝ) (hell : ∑ i, ell i = 0)
    (ha : diagonalOneParameter ell hell (-1) ∈ Subgroup.normalizer (H : Set (G n)))
    (hμ : μ.map (fun x => rightAction x (diagonalOneParameter ell hell (-1))) = μ) :
    ∀ᵐ z ∂μ.trim (actionInvariantSigma_le H (X n)),
      ∀ V ∈ matrixVelocitySpace (invariantRightSubgroup
        (condExpKernel μ (actionInvariantSigma H (X n)) z)),
      (diagonalOneParameter ell hell 1).val * V *
        (diagonalOneParameter ell hell (-1)).val ∈
          matrixVelocitySpace (invariantRightSubgroup
…

Mentions: OAI.DukePrimeDegree.matrixVelocitySpace