OAI/NumberTheory/DukePrimeDegree/Dynamics/KernelStabilizerMeasurable.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Measurable invariance events for the actual component measures

Equality of finite kernel values is detected by countably many half-line tests after a measurable embedding in the real line. Consequently both invariance under one lattice translation and invariance under an entire root flow are measurable events in the component parameter. The latter uses rational times and the closedness of the actual measure stabilizer.

  1. lemma OAI.DukePrimeDegree.measurableSet_finite_kernel_eq line 24
  2. lemma OAI.DukePrimeDegree.measurableSet_kernel_translation_invariant line 67
  3. lemma OAI.DukePrimeDegree.all_root_mem_iff_rational_root_mem line 76
  4. lemma OAI.DukePrimeDegree.measurableSet_kernel_root_invariant line 89

    Source documentation

    Full real-root invariance is a measurable event, without replacing the real root by a discrete-time action.

    lemma measurableSet_kernel_root_invariant
    {Z : Type*} [MeasurableSpace Z] {n : ℕ} {i j : Fin n}
    (hij : i ≠ j) (κ : Kernel Z (X n)) [IsFiniteKernel κ] :
    MeasurableSet {z | ∀ t : ℝ,
      Matrix.SpecialLinearGroup.transvection hij t ∈ invariantRightSubgroup (κ z)} := by
…