OAI/GroupTheory/PolycyclicRecognition/Algebra/ParameterDensityMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.measure_le_of_density_bound line 14

   Source documentation

   The density bound is imposed before restriction to the successful set.

   theorem measure_le_of_density_bound {A : Type*} [MeasurableSpace A]
       (μ : Measure A) (ν : Measure A) (f : A → ℝ≥0∞) (hν : ν = μ.withDensity f)
       {D : ℝ≥0∞} (hf : ∀ᵐ x ∂μ, f x ≤ D) : ν ≤ D • μ := by
   …

2. theorem OAI.PolycyclicRecognition.subexponential_volume_of_probability line 22

   Source documentation

   A subexponential density upper bound turns positive successful probability into the volume lower bound used by the polynomial image argument.

   theorem subexponential_volume_of_probability
       {A : Type*} [MeasurableSpace A]
       (μ ν : ℝ → Measure A) (E : ℝ → Set A) (D : ℝ → ℝ≥0)
       (hfinite : ∀ r, μ r (E r) ≠ ∞)
       (hdom : ∀ r, ν r ≤ (D r : ℝ≥0∞) • μ r)
       (hprob : HasSubexponentialLowerBound (fun r => (ν r (E r)).toReal))
       (hD : HasSubexponentialUpperBound (fun r => (D r : ℝ)))
       (hpos : ∀ᶠ r in atTop, 0 < D r) :
       HasSubexponentialLowerBound (fun r => (μ r (E r)).toReal) := by
   …

   Mentions: OAI.PolycyclicRecognition.HasSubexponentialLowerBound, OAI.PolycyclicRecognition.HasSubexponentialUpperBound