OAI/GroupTheory/PolycyclicRecognition/Analysis/CompactProbabilityDensity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_compact_probability_density line 18

   Source documentation

   A compact subset of an open chart admits a continuous compactly supported probability density which is one fixed positive constant on that subset. It is bounded above by that same constant everywhere.

   theorem exists_compact_probability_density
       {X : Type*} [TopologicalSpace X] [R1Space X] [LocallyCompactSpace X]
       [MeasurableSpace X] [BorelSpace X]
       (μ : Measure X) [μ.IsOpenPosMeasure] [IsFiniteMeasureOnCompacts μ]
       {K U : Set X} (hK : IsCompact K) (hne : K.Nonempty)
       (hU : IsOpen U) (hKU : K ⊆ U) :
       ∃ (ρ : C(X, ℝ)) (b : ℝ), 0 < b ∧ HasCompactSupport ρ ∧ tsupport ρ ⊆ U ∧
         (∀ x, 0 ≤ ρ x ∧ ρ x ≤ b) ∧ (∀ x ∈ K, ρ x = b) ∧
         Integrable ρ μ ∧ ∫ x, ρ x ∂μ = 1 := by
   …

2. theorem OAI.PolycyclicRecognition.mem_support_densityProbabilityMeasure line 55

   Source documentation

   Every point where the continuous density is positive belongs to the support of its probability measure.

   theorem mem_support_densityProbabilityMeasure
       {X : Type*} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X]
       (μ : Measure X) [μ.IsOpenPosMeasure] (ρ : X → ℝ) (hρ : Continuous ρ)
       (hi : Integrable ρ μ) (hp : ∀ x, 0 ≤ ρ x) (hm : ∫ x, ρ x ∂μ = 1)
       {x : X} (hx : 0 < ρ x) :
       x ∈ (densityProbabilityMeasure μ ρ hi hp hm : Measure X).support := by
   …

   Mentions: OAI.PolycyclicRecognition.densityProbabilityMeasure