AutocorrelationRecurrence.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The positive autocorrelation behind backward recurrence

def OAI.PolycyclicRecognition.rightInverseAverage line 19
Source documentation
Average a function over the inverse of a sampled right increment.
```
def rightInverseAverage (σ : Measure G) (f : G → ℝ≥0∞) (x : G) : ℝ≥0∞ :=
…
```
theorem OAI.PolycyclicRecognition.measurable_rightInverseAverage line 22
theorem OAI.PolycyclicRecognition.rightInverseAverage_le_one line 29
theorem OAI.PolycyclicRecognition.rightInverseAverage_indicator_eq_zero line 40
Source documentation
The averaged indicator vanishes outside the product of its original set and a set carrying the increment law. This is the support bound used in Cauchy--Schwarz.
```
theorem rightInverseAverage_indicator_eq_zero
    (σ : Measure G) (A K R : Set G) (hK : ∀ᵐ s ∂σ, s ∈ K)
    (hAR : ∀ a ∈ A, ∀ s ∈ K, a * s ∈ R) {x : G} (hx : x ∉ R) :
    rightInverseAverage σ (A.indicator (fun _ => (1 : ℝ≥0∞))) x = 0 := by
…
```
Mentions: OAI.PolycyclicRecognition.rightInverseAverage
theorem OAI.PolycyclicRecognition.right_autocorrelation_eq_square line 54
Source documentation
The transition law obtained from two independent copies of the same increment has nonnegative quadratic form. The square identity is exact and uses right Haar invariance and Tonelli, with no symmetry assumption on σ.
```
theorem right_autocorrelation_eq_square
    (μ σ : Measure G) [SFinite μ] [SFinite σ] [μ.IsMulRightInvariant]
    (f : G → ℝ≥0∞) (hf : Measurable f) :
    (∫⁻ x, f x * (∫⁻ s, rightInverseAverage σ f (x * s) ∂σ) ∂μ) =
      ∫⁻ z, rightInverseAverage σ f z ^ 2 ∂μ := by
…
```
Mentions: OAI.PolycyclicRecognition.rightInverseAverage
theorem OAI.PolycyclicRecognition.lintegral_rightInverseAverage line 89
Source documentation
The first averaged function has the same total mass as the original one. This is the second input to the recurrence lower bound.
```
theorem lintegral_rightInverseAverage
    (μ σ : Measure G) [SFinite μ] [IsProbabilityMeasure σ] [μ.IsMulRightInvariant]
    (f : G → ℝ≥0∞) (hf : Measurable f) :
    (∫⁻ z, rightInverseAverage σ f z ∂μ) = ∫⁻ z, f z ∂μ := by
…
```
Mentions: OAI.PolycyclicRecognition.rightInverseAverage