ComponentTrace.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Null traces on the nondegenerate components of a level union

Generic level unions have only countably many nondegenerate components. Consequently a trace that is null on each such component is null on their union. At free points the new coordinate has one trace value, so the levels meeting this union form a Haar-null set. This is the fixed-prior- tuple step in the manuscript's compatibility argument.

def OAI.CircleDomainRigidity.nontrivialComponentLocus line 21
theorem OAI.CircleDomainRigidity.volume_trace_nontrivialComponentLocus_eq_zero line 24

theorem OAI.CircleDomainRigidity.ae_new_level_avoids_nontrivial_components line 44

Source documentation

At free points, membership in the new level is membership of the unique trace value. Null component traces therefore exclude almost every new level from every nondegenerate old component.

theorem ae_new_level_avoids_nontrivial_components
    {X : Type*} [MetricSpace X] [CompactSpace X]
    (hbound : HasFiniteLargeContinuumBound X) (F : Set X)
    (w : X → AddCircle (1 : ℝ)) (H : AddCircle (1 : ℝ) → Set X)
    (hlevel : ∀ x ∈ F, ∀ t, x ∈ H t ↔ w x = t)
    (hnull : ∀ C : Set X, (∃ x, C = connectedComponent x) → C.Nontrivial →
      volume (w '' (F ∩ C)) = 0) :
    ∀ᵐ t ∂volume, ∀ x ∈ F ∩ H t, x ∉ nontrivialComponentLocus X := by
…

Mentions: OAI.CircleDomainRigidity.HasFiniteLargeContinuumBound, OAI.CircleDomainRigidity.nontrivialComponentLocus

theorem OAI.CircleDomainRigidity.ae_product_compatibility_of_ae_sections line 62

Source documentation

Passing from almost every prior tuple and almost every new level to the product assertion requires measurability of the incidence relation. The manuscript obtains this from compact hyperspace projection.

theorem ae_product_compatibility_of_ae_sections
    {T : Type*} [MeasurableSpace T] (ν : Measure T) [SFinite ν]
    (P : AddCircle (1 : ℝ) → T → Prop)
    (hP : MeasurableSet {z : AddCircle (1 : ℝ) × T | P z.1 z.2})
    (hsections : ∀ᵐ s ∂ν, ∀ᵐ t ∂volume, P t s) :
    ∀ᵐ z ∂(volume.prod ν), P z.1 z.2 := by
…