CorrectedGenericPairs.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous generic representatives of a transverse pair

A correction in a block-preserving subgroup may depend on the pair. The Haar-fiber selection puts both corrected points back in the same generic set, and simultaneous block conjugation preserves the scalar within-block normalization. The subgroup is contained in the actual measure stabilizer in the application; that inclusion is explicit here.

lemma OAI.DukePrimeDegree.measurable_rightAction_subgroup_uncurry line 23

theorem OAI.DukePrimeDegree.exists_actual_stabilizer_fiber_good_set line 30

Source documentation

The finite-patch enlargement uses invariance of the ambient measure under its actual stabilizer, without selecting an ergodic time-one map.

theorem exists_actual_stabilizer_fiber_good_set {n : ℕ}
    (μ : Measure (X n)) [IsProbabilityMeasure μ]
    (H : Subgroup (G n)) (hH : H ≤ invariantRightSubgroup μ)
    (ρ : Measure H) [SFinite ρ] (K : Set H)
    (G₀ : Set (X n)) (hG₀ : MeasurableSet G₀)
    (a : ℝ≥0∞) (ha : a ≠ 0) (hatop : a ≠ ⊤) :
    ∃ E : Set (X n), MeasurableSet E ∧
      μ Eᶜ ≤ (ρ K * μ G₀ᶜ) / a ∧
      ∀ x ∈ E,
        badOrbitFiberMass ρ (fun y h => rightAction y (h : G n)) K G₀ x < a := by
…

Mentions: OAI.DukePrimeDegree.badOrbitFiberMass

theorem OAI.DukePrimeDegree.exists_corrected_generic_pair line 48

Source documentation

Algebraic and generic-set properties hold for the very same common translation. The selected translation lies in the prescribed bounded patch; it is not an extra independent limit or invariance hypothesis.

theorem exists_corrected_generic_pair {n : ℕ}
    (L H : Subgroup (G n)) (hHL : H ≤ L)
    (r : Setoid (Fin n)) (hblock : H ≤ blockMatrixGroup r)
    (ρ : Measure H) [ρ.IsMulLeftInvariant]
    (K₀ K₁ : Set H) (hK : K₀ ⊆ K₁)
    (G₀ : Set (X n)) (hG₀ : MeasurableSet G₀)
    (x : X n) (a : G n) (ha : a ∉ L) (b : H)
    (hb : ∀ h ∈ K₀, b * h ∈ K₁)
    (c : ℝ)
    (hpart : withinBlockPart r (a * (b : G n)).val = Matrix.diagonal (fun _ => c))
    (hsmall :
      badOrbitFiberMass ρ (fun y h => rightAction y (h : G n)) K₁ G₀ x +
…

Mentions: OAI.DukePrimeDegree.blockMatrixGroup, OAI.DukePrimeDegree.withinBlockPart, OAI.DukePrimeDegree.badOrbitFiberMass