CompactCorrectionPatches.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed compact patches for varying stabilizer corrections

The pair correction tends to identity. Two fixed compact patches then suffice: small corrections send the smaller patch into the larger one. Positive Haar mass and finite larger-patch mass give the two constants used in the fiber-good-set estimate.

theorem OAI.DukePrimeDegree.exists_compact_correction_patches line 24

theorem OAI.DukePrimeDegree.eventually_maps_compact_correction_patch line 45

Source documentation

A fixed patch works eventually for an arbitrary sequence of identity-converging corrections. No rate is compared with the orbit window length.

theorem eventually_maps_compact_correction_patch
    {H I : Type*} [Group H] [TopologicalSpace H]
    {l : Filter I} (b : I → H) (hb : Tendsto b l (𝓝 1))
    (W K₀ K₁ : Set H) (hW : IsOpen W) (h1 : 1 ∈ W)
    (hpatch : ∀ a ∈ W, ∀ h ∈ K₀, a * h ∈ K₁) :
    ∀ᶠ i in l, ∀ h ∈ K₀, b i * h ∈ K₁ := by
…