BackwardRecurrenceStep.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

One quantitative step of backward recurrence

def OAI.PolycyclicRecognition.twoSampleReturn line 19
Source documentation
Probability of returning to A after a difference of two independent increments with law σ.
```
def twoSampleReturn (σ : Measure G) (A : Set G) (x : G) : ℝ≥0∞ :=
…
```
theorem OAI.PolycyclicRecognition.measurable_twoSampleReturn line 22
theorem OAI.PolycyclicRecognition.twoSampleReturn_le_one line 32

theorem OAI.PolycyclicRecognition.exists_backward_recurrence_step line 46

Source documentation

Discarding points with small return probability retains a definite quadratic fraction of the original set. This is the backward construction used to keep every intermediate sheet in the prescribed good set.

theorem exists_backward_recurrence_step
    (μ σ : Measure G) [SFinite μ] [IsProbabilityMeasure σ] [μ.IsMulRightInvariant]
    (A Q K R : Set G) (hA : MeasurableSet A) (hQfin : μ Q ≠ ∞)
    (hAQ : A ⊆ Q) (hApos : 0 < (μ A).toReal) (hQpos : 0 < (μ Q).toReal)
    (hK : ∀ᵐ s ∂σ, s ∈ K) (hRfin : μ R ≠ ∞) (hRpos : 0 < (μ R).toReal)
    (hAR : ∀ a ∈ A, ∀ s ∈ K, a * s ∈ R)
    {D : ℝ} (hD : 0 < D) (hvol : (μ R).toReal ≤ D * (μ Q).toReal) :
    ∃ B : Set G, MeasurableSet B ∧ B ⊆ A ∧ 0 < (μ B).toReal ∧
      (μ A).toReal ^ 2 / (2 * D * (μ Q).toReal) ≤ (μ B).toReal ∧
      ∀ x ∈ B, (μ A).toReal / (2 * D * (μ Q).toReal) ≤
        (twoSampleReturn σ A x).toReal := by
…

Mentions: OAI.PolycyclicRecognition.twoSampleReturn