OAI/NumberTheory/DukePrimeDegree/Dynamics/VelocityMembershipMeasurable.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Measurable tests for actual component velocities

For a fixed matrix, membership in the velocity space of a component stabilizer is a measurable event. The exponential characterization makes it a countable collection of ordinary stabilizer tests. Rational times suffice because the subgroup and its matrix image are closed.

  1. lemma OAI.DukePrimeDegree.all_exp_mem_iff_rational_exp_mem line 22
  2. lemma OAI.DukePrimeDegree.mem_matrixVelocitySpace_iff_rational_exp line 42
  3. lemma OAI.DukePrimeDegree.measurableSet_kernel_exp_invariant line 50
  4. theorem OAI.DukePrimeDegree.measurableSet_kernel_velocity_mem line 80

    Source documentation

    This tests the genuine differentiable-curve velocity space. No measurable choice of subgroup curves is assumed or made.

    theorem measurableSet_kernel_velocity_mem
    {Z : Type*} [MeasurableSpace Z] {n : ℕ} [Nonempty (Fin n)]
    (κ : Kernel Z (X n)) [IsFiniteKernel κ]
    (V : Matrix (Fin n) (Fin n) ℝ) :
    MeasurableSet {z | V ∈ matrixVelocitySpace (invariantRightSubgroup (κ z))} := by
…

    Mentions: OAI.DukePrimeDegree.matrixVelocitySpace