AutocorrelationLowerBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The quantitative lower bound for a two-sample return

theorem OAI.PolycyclicRecognition.sq_mass_le_region_mul_square_mass line 17

Source documentation

A function with values in [0,1], supported in a finite-volume region, has square integral at least its squared mass divided by that volume.

theorem sq_mass_le_region_mul_square_mass
    {X : Type*} [MeasurableSpace X] (μ : Measure X)
    (f : X → ℝ≥0∞) (hf : Measurable f) (hb : ∀ x, f x ≤ 1)
    (R : Set X) (hRfin : μ R ≠ ∞) (hRpos : 0 < (μ R).toReal)
    (hsupp : ∀ x, x ∉ R → f x = 0) :
    (∫⁻ x, f x ∂μ).toReal ^ 2 ≤ (μ R).toReal * (∫⁻ x, f x ^ 2 ∂μ).toReal := by
…

theorem OAI.PolycyclicRecognition.return_correlation_lower_bound line 64

Source documentation

The mean probability of returning to A after a difference of two independent increments has the required quadratic lower bound. The region R can be the compact product Q * support σ in the application.

theorem return_correlation_lower_bound
    {G : Type*} [Group G] [MeasurableSpace G] [MeasurableMul₂ G] [MeasurableInv G]
    (μ σ : Measure G) [SFinite μ] [IsProbabilityMeasure σ] [μ.IsMulRightInvariant]
    (A K R : Set G) (hA : MeasurableSet A) (hK : ∀ᵐ s ∂σ, s ∈ K)
    (hRfin : μ R ≠ ∞) (hRpos : 0 < (μ R).toReal)
    (hAR : ∀ a ∈ A, ∀ s ∈ K, a * s ∈ R) :
    (μ A).toReal ^ 2 ≤ (μ R).toReal *
      (∫⁻ x in A, ∫⁻ s₁, ∫⁻ s₂,
        A.indicator (fun _ => (1 : ℝ≥0∞)) (x * s₁ * s₂⁻¹) ∂σ ∂σ ∂μ).toReal := by
…