BackwardRecurrenceFamily.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Backward recurrence for a varying family of Haar boxes

theorem OAI.PolycyclicRecognition.normalized_backward_mass_bound line 17
Source documentation
The elementary change from Haar mass to relative Haar mass in the quadratic recurrence.
```
theorem normalized_backward_mass_bound {a b q D : ℝ} (hq : 0 < q) (hD : 0 < D)
    (h : b ^ 2 / (2 * D * q) ≤ a) :
    (b / q) ^ 2 / (2 * D) ≤ a / q := by
…
```

theorem OAI.PolycyclicRecognition.exists_subexponential_backward_recurrence line 28

Source documentation

The retained initial sheets and the probability of every successful switch both have subexponential lower bounds. The groups and sampling laws are actual measure spaces, and the good set may vary with scale.

theorem exists_subexponential_backward_recurrence
    {G : Type*} [Group G] [MeasurableSpace G] [MeasurableMul₂ G] [MeasurableInv G]
    (μ : Measure G) [SFinite μ] [μ.IsMulRightInvariant]
    (σ : ℝ → ℕ → Measure G) [∀ r j, IsProbabilityMeasure (σ r j)]
    (Q A : ℝ → Set G) (K R : ℝ → ℕ → Set G) (D : ℝ → ℕ → ℝ)
    (hQfin : ∀ r, μ (Q r) ≠ ∞) (hQpos : ∀ r, 0 < (μ (Q r)).toReal)
    (hK : ∀ r j, ∀ᵐ s ∂σ r j, s ∈ K r j)
    (hRfin : ∀ r j, μ (R r j) ≠ ∞) (hRpos : ∀ r j, 0 < (μ (R r j)).toReal)
    (hQR : ∀ r j, ∀ a ∈ Q r, ∀ s ∈ K r j, a * s ∈ R r j)
    (hD : ∀ r j, 0 < D r j)
    (hvol : ∀ r j, (μ (R r j)).toReal ≤ D r j * (μ (Q r)).toReal)
    (h : ℕ) (hA : ∀ r, MeasurableSet (A r)) (hAQ : ∀ r, A r ⊆ Q r)
…