LusinInput.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Completed-measure compatibility for finite level tuples

Lusin's universal-measurability theorem applies to the finite-dimensional tori used for level choices: A. S. Kechris, Classical Descriptive Set Theory, GTM 156 (1995), Theorem 21.10, p. 155. Every analytic subset of a standard Borel space is measurable for the completion of each sigma-finite Borel measure. Publisher: https://doi.org/10.1007/978-1-4612-4190-4

The compatibility statement uses analyticity of compact incidence sets and nullity of the free trace image on each nondegenerate component.

def OAI.CircleDomainRigidity.FiniteTorusAnalyticMeasurability line 27
Source documentation
The specialization of Kechris, Theorem 21.10, actually needed for finite tuples of circle-valued levels.
```
def FiniteTorusAnalyticMeasurability : Prop :=
…
```
theorem OAI.CircleDomainRigidity.nontrivialComponentInLocus_eq_image line 34
Source documentation
The ambient version of the nondegenerate-component locus agrees with the image of the corresponding locus in the level subtype.
```
theorem nontrivialComponentInLocus_eq_image
    {X : Type*} [TopologicalSpace X] (A : Set X) :
    {x | (connectedComponentIn A x).Nontrivial} =
      Subtype.val '' nontrivialComponentLocus A := by
…
```
Mentions: OAI.CircleDomainRigidity.nontrivialComponentLocus

theorem OAI.CircleDomainRigidity.volume_trace_nontrivialComponentInLocus_eq_zero line 54

Source documentation

Null component traces give a null trace image on the ambient nondegenerate-component locus of a compact level union.

theorem volume_trace_nontrivialComponentInLocus_eq_zero
    {X : Type*} [MetricSpace X] (A : Set X) [CompactSpace A]
    (hbound : HasFiniteLargeContinuumBound A) (F : Set X)
    (w : X → UnitAddCircle)
    (hnull : ∀ C : Set A, (∃ x, C = connectedComponent x) → C.Nontrivial →
      volume ((fun x : A => w x) '' ((Subtype.val ⁻¹' F) ∩ C)) = 0) :
    volume (w '' (F ∩ {x | (connectedComponentIn A x).Nontrivial})) = 0 := by
…

Mentions: OAI.CircleDomainRigidity.HasFiniteLargeContinuumBound

theorem OAI.CircleDomainRigidity.product_null_of_nullMeasurable_swapped_sections line 76

Source documentation

Fubini's null-section implication with the other order of factors. The event need only be measurable in the completed product measure.

theorem product_null_of_nullMeasurable_swapped_sections
    {A B : Type*} [MeasurableSpace A] [MeasurableSpace B]
    {μ : Measure A} {ν : Measure B} [SFinite μ] [SFinite ν]
    {E : Set (A × B)} (hE : NullMeasurableSet E (μ.prod ν))
    (hsections : ∀ᵐ y ∂ν, μ ((fun x => (x, y)) ⁻¹' E) = 0) :
    (μ.prod ν) E = 0 := by
…

theorem OAI.CircleDomainRigidity.nullMeasurableSet_freeComponentFailure line 92

Source documentation

An analytic compatibility failure is measurable for the completed product law, using analytic measurability on finite tori.

theorem nullMeasurableSet_freeComponentFailure
    {X Λ : Type*} [MetricSpace X] [CompactSpace X] [PolishSpace X]
    [MeasurableSpace X] [BorelSpace X]
    (hLusin : FiniteTorusAnalyticMeasurability) (d : ℕ)
    {F : Set X} (hF : MeasurableSet F)
    {Rnew : Set (X × UnitAddCircle)} (hnew : IsClosed Rnew)
    {R : Λ → Set (X × UnitAddCircle)} (hR : ∀ l, IsClosed (R l))
    (labels : Fin d → Λ) :
    NullMeasurableSet (freeComponentFailure F Rnew R labels)
      (volume.prod (Measure.pi (fun _ : Fin d => volume))) :=
…

Mentions: OAI.CircleDomainRigidity.FiniteTorusAnalyticMeasurability, OAI.CircleDomainRigidity.freeComponentFailure

theorem OAI.CircleDomainRigidity.measure_new_level_failure_eq_zero line 106

Source documentation

For one fixed prior tuple, null component traces exclude all new levels except a Haar-null set. No measurability of the trace is needed.

theorem measure_new_level_failure_eq_zero
    {X Λ : Type*} [MetricSpace X] [CompactSpace X]
    (F : Set X) (Rnew : Set (X × UnitAddCircle))
    (R : Λ → Set (X × UnitAddCircle)) (d : ℕ) (labels : Fin d → Λ)
    (θ : Fin d → UnitAddCircle) (w : X → UnitAddCircle)
    (hlevel : ∀ x ∈ F, ∀ t, (x, t) ∈ Rnew ↔ w x = t)
    (hA : IsClosed {x | (x, θ) ∈ finiteLevelUnionGraph R labels})
    (hbound : HasFiniteLargeContinuumBound
      {x | (x, θ) ∈ finiteLevelUnionGraph R labels})
    (hnull : ∀ C : Set {x | (x, θ) ∈ finiteLevelUnionGraph R labels},
      (∃ x, C = connectedComponent x) → C.Nontrivial →
      volume ((fun x : {x | (x, θ) ∈ finiteLevelUnionGraph R labels} => w x) ''
…

Mentions: OAI.CircleDomainRigidity.finiteLevelUnionGraph, OAI.CircleDomainRigidity.HasFiniteLargeContinuumBound

theorem OAI.CircleDomainRigidity.measure_freeComponentFailure_eq_zero line 132

Source documentation

The finite-tuple compatibility conclusion, conditional on the analytic measurability on finite tori and the null-trace hypotheses. Repeated prior labels are allowed.

theorem measure_freeComponentFailure_eq_zero
    {X Λ : Type*} [MetricSpace X] [CompactSpace X] [PolishSpace X]
    [MeasurableSpace X] [BorelSpace X]
    (hLusin : FiniteTorusAnalyticMeasurability) (d : ℕ)
    {F : Set X} (hF : MeasurableSet F)
    {Rnew : Set (X × UnitAddCircle)} (hnew : IsClosed Rnew)
    {R : Λ → Set (X × UnitAddCircle)} (hR : ∀ l, IsClosed (R l))
    (labels : Fin d → Λ) (w : X → UnitAddCircle)
    (hlevel : ∀ x ∈ F, ∀ t, (x, t) ∈ Rnew ↔ w x = t)
    (hgood : ∀ᵐ θ ∂Measure.pi (fun _ : Fin d => (volume : Measure UnitAddCircle)),
      HasFiniteLargeContinuumBound {x | (x, θ) ∈ finiteLevelUnionGraph R labels} ∧
      ∀ C : Set {x | (x, θ) ∈ finiteLevelUnionGraph R labels},
…

Mentions: OAI.CircleDomainRigidity.FiniteTorusAnalyticMeasurability, OAI.CircleDomainRigidity.HasFiniteLargeContinuumBound, OAI.CircleDomainRigidity.finiteLevelUnionGraph