OAI/GroupTheory/PolycyclicRecognition/Algebra/OccupationDomination.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.map_densityProbabilityMeasure_le line 17

   Source documentation

   The density comparison is made before projecting the coordinates. A measure-preserving coordinate move therefore retains the same bound after pushforward, without any injectivity requirement on the chart.

   theorem map_densityProbabilityMeasure_le
       {D : Type*} [MeasurableSpace D] (m : Measure D)
       (η ρ : D → ℝ) (hiη : Integrable η m) (hiρ : Integrable ρ m)
       (hpη : ∀ z, 0 ≤ η z) (hpρ : ∀ z, 0 ≤ ρ z)
       (hmη : ∫ z, η z ∂m = 1) (hmρ : ∫ z, ρ z ∂m = 1)
       (hρ : Measurable ρ) (T : D → D) (hT : MeasurePreserving T m m)
       (c : ℝ≥0) (hbound : ∀ z, η z ≤ (c : ℝ) * ρ (T z)) :
       Measure.map T (densityProbabilityMeasure m η hiη hpη hmη : Measure D) ≤
         c • (densityProbabilityMeasure m ρ hiρ hpρ hmρ : Measure D) := by
   …

   Mentions: OAI.PolycyclicRecognition.densityProbabilityMeasure

2. theorem OAI.PolycyclicRecognition.density_bound_on_swept_support line 44

   Source documentation

   A uniform upper bound on the initial density and a positive lower bound on the swept support give the coordinate density comparison.

   theorem density_bound_on_swept_support
       {D : Type*} (η ρ : D → ℝ) (T : D → D) (K : Set D)
       {A b : ℝ} (hA : 0 ≤ A) (hb : 0 < b)
       (hη : ∀ z, η z ≤ A) (hρ : ∀ z, 0 ≤ ρ z)
       (hsupp : ∀ z, η z ≠ 0 → T z ∈ K) (hlower : ∀ z ∈ K, b ≤ ρ z) :
       ∀ z, η z ≤ (A / b) * ρ (T z) := by
   …

3. theorem OAI.PolycyclicRecognition.map_productOccupationLaw_le line 61

   Source documentation

   Domination in the second sampling coordinate passes through the actual chart and its exact action identity.

   theorem map_productOccupationLaw_le
       {A D X : Type*} [MeasurableSpace A] [MeasurableSpace D] [MeasurableSpace X]
       (μ : ProbabilityMeasure A) (σ ν : ProbabilityMeasure D)
       (p : A × D → X) (hp : Measurable p)
       (T : D → D) (hT : Measurable T) (act : X → X) (hact : Measurable act)
       (hmove : ∀ a z, act (p (a, z)) = p (a, T z))
       (c : ℝ≥0) (hdom : Measure.map T (σ : Measure D) ≤ c • (ν : Measure D)) :
       Measure.map act (productOccupationLaw μ σ p : Measure X) ≤
         c • (productOccupationLaw μ ν p : Measure X) := by
   …

   Mentions: OAI.PolycyclicRecognition.productOccupationLaw