PathVolumeComparison.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Stationary path-volume comparison

A common pair on a positive-volume endpoint set gives the lower exponential count. Coarse path packing bounds its image count. Polynomial and logarithmic losses disappear before the template thickening tends to zero.

theorem OAI.PolycyclicRecognition.exponent_le_of_stationary_path_counts line 25

Source documentation

Exact comparison with every positive enlargement of the image template.

theorem exponent_le_of_stationary_path_counts
    (π : G →* Multiplicative W) (E : Set W) (P : Set W → ℝ)
    {p K C D : ℝ} {a Q : ℝ≥0∞} (hΛ : 0 < (Λ : ℝ))
    (hK : 0 ≤ K) (hC : 0 ≤ C) (ha : 0 < a) (hafin : a < ⊤)
    (hQ : Q < ⊤) (hD : 0 < D) (k : ℕ)
    (hlower : ∀ δ : ℝ, 0 < δ → ∀ η : ℝ, 0 < η → ∃ r₀ : ℝ, 1 ≤ r₀ ∧
      ∀ r : ℝ, r₀ ≤ r → ∃ (f : NormalizedPair G Λ) (s : Finset G),
        (∀ x ∈ s, ∀ y ∈ s, x ≠ y → (Λ : ℝ) * ((Λ : ℝ) + 1) < dist x y) ∧
        a * ENNReal.ofReal (Real.exp (r * p)) ≤ (s.card : ℝ≥0∞) * Q ∧
        ∀ g ∈ s, ∃ γ : Path (1 : G) g,
          PathMetricBound γ (C * r) (C * (1 + Real.log (2 + r))) ∧
          ∀ t, ∃ z ∈ E, ‖pairHeight π (γ t) f - r • z‖ ≤
…

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