LocalOrbitIsolation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Local orbit isolation gives a positive-mass orbit

The topological conclusion needed from the shearing argument is local isolation of the invariant-group orbits inside one positive-mass good set. Second countability then produces a countable orbit cover, so one actual orbit has positive mass. No finite-orbit existence is assumed.

theorem OAI.DukePrimeDegree.exists_positive_member_of_local_cover line 26

Source documentation

A positive-mass set locally covered by single members of a family has positive mass in one family member. The family members need not be open, measurable, or countable.

theorem exists_positive_member_of_local_cover
    {Y I : Type*} [TopologicalSpace Y] [SecondCountableTopology Y] [MeasurableSpace Y]
    (μ : Measure Y) (E : Set Y) (hE : μ E ≠ 0) (O : I → Set Y)
    (hlocal : ∀ x ∈ E, ∃ (i : I) (U : Set Y),
      IsOpen U ∧ x ∈ U ∧ E ∩ U ⊆ O i) :
    ∃ i : I, μ (O i) ≠ 0 := by
…

theorem OAI.DukePrimeDegree.exists_good_point_in_closure_outside_orbit line 52

Source documentation

If every orbit is null, every positive-mass good set contains a point approached by good points from outside its orbit.

theorem exists_good_point_in_closure_outside_orbit
    {Y : Type*} [TopologicalSpace Y] [SecondCountableTopology Y] [MeasurableSpace Y]
    (μ : Measure Y) (E : Set Y) (hE : μ E ≠ 0) (O : Y → Set Y)
    (hnull : ∀ x, μ (O x) = 0) :
    ∃ x ∈ E, x ∈ closure (E \ O x) := by
…

theorem OAI.DukePrimeDegree.exists_good_sequence_outside_orbit line 70

theorem OAI.DukePrimeDegree.isHaar_of_local_invariant_orbit_isolation line 84

Source documentation

For the actual closed measure stabilizer, local orbit isolation is enough for the previously proved prime-degree Haar obstruction. The isolation premise is an intermediate shearing target, not a replacement for the published rigidity theorem.

theorem isHaar_of_local_invariant_orbit_isolation
    (d : ℕ) (hprime : (d + 1).Prime)
    (μ : Measure (X (d + 1))) [IsProbabilityMeasure μ]
    (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u)) = μ)
    (r : Setoid (Fin (d + 1)))
    (hr : ∀ i j, r i j ↔ rootInvarianceRelation μ i j)
    (hnontrivial : ∃ i j, i ≠ j ∧ r i j)
    (E : Set (X (d + 1))) (hE : μ E ≠ 0)
    (hlocal : ∀ x ∈ E, ∃ (g : G (d + 1)) (U : Set (X (d + 1))),
      IsOpen U ∧ x ∈ U ∧ E ∩ U ⊆ range (latticeOrbitPoint g (invariantRightSubgroup μ))) :
    IsHaarProbability μ := by
…

Mentions: OAI.DukePrimeDegree.diagonalFlow, OAI.DukePrimeDegree.latticeOrbitPoint