OAI/GroupTheory/PolycyclicRecognition/Analysis/SupportedProbabilityRestriction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.supportedProbabilityRestriction line 15

   Source documentation

   A probability carried by a measurable set, viewed on that subtype.

   def supportedProbabilityRestriction
       {X : Type*} [MeasurableSpace X] (μ : ProbabilityMeasure X)
       (K : Set X) (hK : MeasurableSet K) (hfull : ∀ᵐ x ∂(μ : Measure X), x ∈ K) :
       ProbabilityMeasure K :=
   …

2. theorem OAI.PolycyclicRecognition.supportedProbabilityRestriction_map line 26
3. theorem OAI.PolycyclicRecognition.mem_support_supportedProbabilityRestriction line 34

   Source documentation

   Supported points stay supported after restriction to a carrying set.

   theorem mem_support_supportedProbabilityRestriction
       {X : Type*} [TopologicalSpace X] [MeasurableSpace X]
       (μ : ProbabilityMeasure X) (K : Set X) (hK : MeasurableSet K)
       (hfull : ∀ᵐ x ∂(μ : Measure X), x ∈ K)
       {x : K} (hx : x.val ∈ (μ : Measure X).support) :
       x ∈ (supportedProbabilityRestriction μ K hK hfull : Measure K).support := by
   …

   Mentions: OAI.PolycyclicRecognition.supportedProbabilityRestriction

4. theorem OAI.PolycyclicRecognition.integral_supportedProbabilityRestriction line 59

   Source documentation

   Restriction does not change integrals of ambient observables.

   theorem integral_supportedProbabilityRestriction
       {X E : Type*} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E]
       (μ : ProbabilityMeasure X) (K : Set X) (hK : MeasurableSet K)
       (hfull : ∀ᵐ x ∂(μ : Measure X), x ∈ K) (f : X → E) :
       (∫ x : K, f x.val ∂(supportedProbabilityRestriction μ K hK hfull : Measure K)) =
         ∫ x, f x ∂(μ : Measure X) := by
   …

   Mentions: OAI.PolycyclicRecognition.supportedProbabilityRestriction