OAI/GroupTheory/PolycyclicRecognition/Analysis/RecurrenceIntegralBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.sq_integral_le_mass_mul_integral_sq line 16

   Source documentation

   Cauchy--Schwarz against the constant function, proved directly by the nonnegativity of variance. The measure need only have positive finite mass.

   theorem sq_integral_le_mass_mul_integral_sq
       {X : Type*} [MeasurableSpace X] (μ : Measure X) [IsFiniteMeasure μ]
       (hM : 0 < μ.real univ) (f : X → ℝ) (hf : Integrable f μ)
       (hf2 : Integrable (fun x => f x ^ 2) μ) :
       (∫ x, f x ∂μ) ^ 2 ≤ μ.real univ * ∫ x, f x ^ 2 ∂μ := by
   …

2. theorem OAI.PolycyclicRecognition.integral_le_superlevel_mass_add line 52

   Source documentation

   A bounded transition function can carry a large integral only if its superlevel set has large measure.

   theorem integral_le_superlevel_mass_add
       {X : Type*} [MeasurableSpace X] (μ : Measure X) [IsFiniteMeasure μ]
       (f : X → ℝ) (hf : Measurable f) (hbound : ∀ x, 0 ≤ f x ∧ f x ≤ 1)
       {t : ℝ} (ht : 0 ≤ t) :
       (∫ x, f x ∂μ) ≤ μ.real {x | t ≤ f x} + t * μ.real univ := by
   …