GoodSetFiberCorrection.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Correcting a pair inside a large generic set

The two initial points may be corrected by a changing element of the measure stabilizer. Averaging the bad set along a fixed group patch gives a larger good set. For two points in that larger set, a common group translation restores membership in the original generic set. No commutation with the averaging flow is needed for this selection.

def OAI.DukePrimeDegree.badOrbitFiberMass line 28
lemma OAI.DukePrimeDegree.badOrbitFiberMass_eq_measure line 32
lemma OAI.DukePrimeDegree.measurable_badOrbitFiberMass line 45

lemma OAI.DukePrimeDegree.lintegral_badOrbitFiberMass line 52

Source documentation

Invariance gives the exact average bad-fiber mass.

lemma lintegral_badOrbitFiberMass
    (μ : Measure Y) [SFinite μ] (ρ : Measure H) [SFinite ρ]
    (R : Y → H → Y) (hR : Measurable (Function.uncurry R))
    (hinv : ∀ h, MeasurePreserving (fun x => R x h) μ μ)
    (K : Set H) (G : Set Y) (hG : MeasurableSet G) :
    (∫⁻ x, badOrbitFiberMass ρ R K G x ∂μ) = ρ K * μ Gᶜ := by
…

Mentions: OAI.DukePrimeDegree.badOrbitFiberMass

theorem OAI.DukePrimeDegree.exists_goodOrbitFiber_set line 75

Source documentation

The enlarged good set has an explicit complement bound and a pointwise fiber estimate, rather than only an almost-everywhere one.

theorem exists_goodOrbitFiber_set
    (μ : Measure Y) [SFinite μ] (ρ : Measure H) [SFinite ρ]
    (R : Y → H → Y) (hR : Measurable (Function.uncurry R))
    (hinv : ∀ h, MeasurePreserving (fun x => R x h) μ μ)
    (K : Set H) (G : Set Y) (hG : MeasurableSet G)
    (a : ℝ≥0∞) (ha : a ≠ 0) (hatop : a ≠ ⊤) :
    ∃ E : Set Y, MeasurableSet E ∧
      μ Eᶜ ≤ (ρ K * μ Gᶜ) / a ∧
      ∀ x ∈ E, badOrbitFiberMass ρ R K G x < a := by
…

Mentions: OAI.DukePrimeDegree.badOrbitFiberMass

theorem OAI.DukePrimeDegree.exists_positive_goodOrbitFiber_set line 96

Source documentation

A small original exceptional set leaves a genuinely positive-mass set of points with uniformly small bad fibers.

theorem exists_positive_goodOrbitFiber_set
    (μ : Measure Y) [IsProbabilityMeasure μ] (ρ : Measure H) [SFinite ρ]
    (R : Y → H → Y) (hR : Measurable (Function.uncurry R))
    (hinv : ∀ h, MeasurePreserving (fun x => R x h) μ μ)
    (K : Set H) (G : Set Y) (hG : MeasurableSet G)
    (a : ℝ≥0∞) (ha : a ≠ 0) (hatop : a ≠ ⊤)
    (hbudget : (ρ K * μ Gᶜ) / a < 1) :
    ∃ E : Set Y, MeasurableSet E ∧ μ E ≠ 0 ∧
      ∀ x ∈ E, badOrbitFiberMass ρ R K G x < a := by
…

Mentions: OAI.DukePrimeDegree.badOrbitFiberMass

theorem OAI.DukePrimeDegree.exists_common_goodOrbit_correction line 124

Source documentation

A common bounded translation corrects both points. The first correction is allowed to vary and need not commute with any flow.

theorem exists_common_goodOrbit_correction
    (ρ : Measure H) [ρ.IsMulLeftInvariant]
    (R : Y → H → Y) (hR : ∀ x, Measurable (R x))
    (K₀ K₁ : Set H) (hK : K₀ ⊆ K₁)
    (G : Set Y) (hG : MeasurableSet G) (x y : Y) (b : H)
    (hb : ∀ h ∈ K₀, b * h ∈ K₁)
    (hsmall : badOrbitFiberMass ρ R K₁ G x +
      badOrbitFiberMass ρ R K₁ G y < ρ K₀) :
    ∃ h ∈ K₀, R x h ∈ G ∧ R y (b * h) ∈ G := by
…

Mentions: OAI.DukePrimeDegree.badOrbitFiberMass

theorem OAI.DukePrimeDegree.exists_common_goodOrbit_correction_of_fiber_bounds line 159

Source documentation

The common correction applies uniformly to every pair in the fiber-good set and every sufficiently small correction.

theorem exists_common_goodOrbit_correction_of_fiber_bounds
    (ρ : Measure H) [ρ.IsMulLeftInvariant]
    (R : Y → H → Y) (hR : ∀ x, Measurable (R x))
    (K₀ K₁ : Set H) (hK : K₀ ⊆ K₁)
    (G E : Set Y) (hG : MeasurableSet G)
    (a : ℝ≥0∞) (hsize : a + a < ρ K₀)
    (hE : ∀ x ∈ E, badOrbitFiberMass ρ R K₁ G x ≤ a)
    (x y : Y) (hx : x ∈ E) (hy : y ∈ E) (b : H)
    (hb : ∀ h ∈ K₀, b * h ∈ K₁) :
    ∃ h ∈ K₀, R x h ∈ G ∧ R y (b * h) ∈ G := by
…

Mentions: OAI.DukePrimeDegree.badOrbitFiberMass