OAI/NumberTheory/DukePrimeDegree/Dynamics/ExactInvariantSets.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact representatives of invariant measurable sets

An almost invariant set has an exactly invariant representative when the acting group carries a nonzero finite measure in a translation invariant measure class. Haar measure supplies such a finite measure. This is the measure-class step needed to compare the full invariant sigma algebra with a countable dense subgroup's invariant sigma algebra.

  1. def OAI.DukePrimeDegree.orbitAlmostAllSet line 28
  2. lemma OAI.DukePrimeDegree.measurableSet_orbitAlmostAllSet line 31
  3. lemma OAI.DukePrimeDegree.preimage_orbitAlmostAllSet_eq line 45
  4. theorem OAI.DukePrimeDegree.orbitAlmostAllSet_ae_eq line 61

    Source documentation

    Fubini replaces separate almost invariance by one exactly invariant set, without a countable intersection over the acting group.

    theorem orbitAlmostAllSet_ae_eq
    (μ : Measure Y) [SFinite μ]
    (ρ : Measure H) [SFinite ρ] (hρ : ρ ≠ 0)
    (hsmul : Measurable (fun p : H × Y => p.1 • p.2))
    {B : Set Y} (hB : MeasurableSet B)
    (hfix : ∀ h : H, (fun x : Y => h • x) ⁻¹' B =ᵐ[μ] B) :
    orbitAlmostAllSet ρ B =ᵐ[μ] B := by
…

    Mentions: OAI.DukePrimeDegree.orbitAlmostAllSet

  5. theorem OAI.DukePrimeDegree.exists_finite_right_quasiInvariant_measure line 86

    Source documentation

    A finite measure equivalent to a left Haar measure has a measure class invariant under every right translation.

    theorem exists_finite_right_quasiInvariant_measure
    [MeasurableMul₂ H] [MeasurableInv H] (haar : Measure H) [SFinite haar]
    [haar.IsMulLeftInvariant] (hhaar : haar ≠ 0) :
    ∃ ρ : Measure H, IsFiniteMeasure ρ ∧ ρ ≠ 0 ∧
      ∀ g : H, QuasiMeasurePreserving (fun h : H => h * g) ρ ρ := by
…
  6. theorem OAI.DukePrimeDegree.exists_exact_invariant_set line 102

    Source documentation

    Exact invariant representatives are obtained from the actual translation-invariant measure class, rather than postulated.

    theorem exists_exact_invariant_set
    [MeasurableMul₂ H] [MeasurableInv H] (haar : Measure H) [SFinite haar]
    [haar.IsMulLeftInvariant] (hhaar : haar ≠ 0)
    (μ : Measure Y) [SFinite μ]
    (hsmul : Measurable (fun p : H × Y => p.1 • p.2))
    {B : Set Y} (hB : MeasurableSet B)
    (hfix : ∀ h : H, (fun x : Y => h • x) ⁻¹' B =ᵐ[μ] B) :
    ∃ E : Set Y, MeasurableSet E ∧ E =ᵐ[μ] B ∧
      ∀ h : H, (fun x : Y => h • x) ⁻¹' E = E := by
…