OAI/Analysis/CircleDomains/Modulus/LevelIncidence.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite level unions and analytic compatibility failures

Repeated labels are allowed in a finite tuple of levels. Closed level graphs give a closed union graph; its nondegenerate-component relation is Borel by the compact hyperspace argument. After restriction to a Borel set of free points, projection over the point is analytic.

  1. def OAI.CircleDomainRigidity.finiteLevelUnionGraph line 20
  2. theorem OAI.CircleDomainRigidity.isClosed_finiteLevelUnionGraph line 24
  3. theorem OAI.CircleDomainRigidity.measurableSet_finiteLevel_nontrivial_components line 33
  4. def OAI.CircleDomainRigidity.freeComponentFailure line 41
  5. theorem OAI.CircleDomainRigidity.analyticSet_freeComponentFailure line 51

    Source documentation

    The failure event in (P) is an analytic subset of its finite level parameter space. Its universal measurability is the separate classical descriptive-set-theoretic input when completed measures are used.

    theorem analyticSet_freeComponentFailure
    {X T J Λ : Type*} [MetricSpace X] [CompactSpace X] [PolishSpace X]
    [TopologicalSpace T] [PolishSpace T] [Fintype J]
    [MeasurableSpace X] [MeasurableSpace T] [BorelSpace X] [BorelSpace T]
    {F : Set X} (hF : MeasurableSet F) {Rnew : Set (X × T)} (hnew : IsClosed Rnew)
    {R : Λ → Set (X × T)} (hR : ∀ l, IsClosed (R l)) (labels : J → Λ) :
    AnalyticSet (freeComponentFailure F Rnew R labels) := by
…

    Mentions: OAI.CircleDomainRigidity.freeComponentFailure

  6. theorem OAI.CircleDomainRigidity.product_null_of_nullMeasurable_sections line 69

    Source documentation

    Fubini's null-section implication for a completed-measurable event. This version does not require the event itself to be Borel.

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