OAI/GroupTheory/PolycyclicRecognition/Analysis/CellProfileRestriction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.ae_mem_cellProbabilityMeasure line 15

   Source documentation

   The normalized cell measure is carried by the cell itself.

   theorem ae_mem_cellProbabilityMeasure {A : Type*} [MeasurableSpace A]
       (μ : Measure A) (C : Set A) (hC : MeasurableSet C) (hC0 : μ C ≠ 0) (hCfin : μ C ≠ ⊤) :
       ∀ᵐ a ∂(cellProbabilityMeasure μ C hC0 hCfin : Measure A), a ∈ C :=
   …

   Mentions: OAI.PolycyclicRecognition.cellProbabilityMeasure

2. theorem OAI.PolycyclicRecognition.map_supportedProbabilityRestriction line 22

   Source documentation

   Restricting a sample to a measurable set of full probability does not change any pushed-forward profile law.

   theorem map_supportedProbabilityRestriction
       {A X : Type*} [MeasurableSpace A] [MeasurableSpace X]
       (μ : ProbabilityMeasure A) (C : Set A) (hC : MeasurableSet C)
       (hfull : ∀ᵐ a ∂(μ : Measure A), a ∈ C) (f : A → X) (hf : Measurable f) :
       ProbabilityMeasure.map (supportedProbabilityRestriction μ C hC hfull)
         (fun a : C => f a.val) = ProbabilityMeasure.map μ f := by
   …

   Mentions: OAI.PolycyclicRecognition.supportedProbabilityRestriction