CompactProbeLift.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Retained compact probes in the ambient product Haar coordinates

def OAI.PolycyclicRecognition.cellSubtypeProbability line 14

Source documentation

The original normalized cell law, viewed on its carrying subtype.

def cellSubtypeProbability {X : Type*} [MeasurableSpace X]
    (μ : Measure X) (C : Set X) (hC : MeasurableSet C)
    (hzero : μ C ≠ 0) (hfinite : μ C ≠ ⊤) : ProbabilityMeasure C :=
…

theorem OAI.PolycyclicRecognition.compact_supported_probe_image line 22

Source documentation

Returning a retained compact probe set from a carrying subtype to the ambient space preserves its exact original probability mass.

theorem compact_supported_probe_image
    {X : Type*} [TopologicalSpace X] [T2Space X]
    [MeasurableSpace X] [BorelSpace X]
    (μ : ProbabilityMeasure X) (carrying : Set X) (hc : MeasurableSet carrying)
    (hfull : ∀ᵐ x ∂(μ : Measure X), x ∈ carrying)
    (K : Set carrying) (hK : IsCompact K) :
    IsCompact (Subtype.val '' K) ∧ MeasurableSet (Subtype.val '' K) ∧
      Subtype.val '' K ⊆ carrying ∧
      (μ : Measure X) (Subtype.val '' K) =
        (supportedProbabilityRestriction μ carrying hc hfull : Measure carrying) K := by
…

Mentions: OAI.PolycyclicRecognition.supportedProbabilityRestriction

theorem OAI.PolycyclicRecognition.cellSubtypeProbability_compact_image line 40