PairStationaryIncrement.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A fixed stationary slope gives increments close to the finite label set

theorem OAI.PolycyclicRecognition.lintegral_normalized_pair_label_distance_le line 23

Source documentation

Normalized increments inherit an L2 distance bound from any one label.

theorem lintegral_normalized_pair_label_distance_le
    (μ : Measure (NormalizedPair G Λ)) [IsProbabilityMeasure μ]
    (π : G →* Multiplicative W) (hπ : Continuous fun g => (π g).toAdd)
    (g : G) {r : ℝ} (hr : 0 < r) {S : Set W} {w : W} (hw : w ∈ S) :
    ∫⁻ p, ENNReal.ofReal (infDist (r⁻¹ • pairHeight π g p) S) ∂μ ≤
      ENNReal.ofReal (r⁻¹ * ‖pairHeightL2 μ π hπ g - Lp.const 2 μ (r • w)‖) := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairHeight, OAI.PolycyclicRecognition.pairHeightL2

theorem OAI.PolycyclicRecognition.normalized_pair_increments_tendsto_labels line 51

Source documentation

The fixed-measure sublinear estimate implies convergence to the whole label set along every linearly bounded family with the prescribed slope.

theorem normalized_pair_increments_tendsto_labels
    (μ : Measure (NormalizedPair G Λ)) [IsProbabilityMeasure μ]
    (π l : G →* Multiplicative W) (hπ : Continuous fun g => (π g).toAdd)
    (hsub : ∀ ε : ℝ, 0 < ε → ∃ B : ℝ, 0 ≤ B ∧ ∀ g,
      ‖pairHeightL2 μ π hπ g - Lp.const 2 μ (l g).toAdd‖ ≤ ε * dist 1 g + B)
    (g : ℝ → G) {R : ℝ} (hR : 0 ≤ R)
    (hsize : ∀ r, 1 ≤ r → dist 1 (g r) ≤ R * r)
    {S : Set W} {w : W} (hw : w ∈ S)
    (hslope : ∀ r, 1 ≤ r → (l (g r)).toAdd = r • w) :
    Tendsto (fun r : ℝ => ∫⁻ p,
      ENNReal.ofReal (infDist (r⁻¹ • pairHeight π (g r) p) S) ∂μ) atTop (𝓝 0) := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairHeightL2, OAI.PolycyclicRecognition.pairHeight