Tubes.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

From ball covers to entropy-producing tube estimates

A cover by balls with a dimension gap between their mass exponent and covering number gives exponential tube decay. The entropy implication uses the constant-sequence specialization of Einsiedler--Lindenstrauss--Michel--Venkatesh (2009), Corollary 3.3, with its two-sided flow tubes.

theorem OAI.DukePrimeDegree.tube_mass_le_of_ball_cover line 27

Source documentation

A tube covered by O(r^{-(n-1)}) balls, each of mass O(r^n), has mass O(r). The cardinality assumption is multiplied through by r^(n-1) to avoid division and retain the exact dimension gap.

theorem tube_mass_le_of_ball_cover
    (μ : Measure X) (tube : Set X) {J : Type*} [Fintype J]
    (balls : J → Set X) (hcover : tube ⊆ ⋃ j, balls j)
    (n : ℕ) (hn : 1 ≤ n) (r Cball Ccover : ℝ)
    (hr : 0 ≤ r) (hCball : 0 ≤ Cball)
    (hball : ∀ j, μ (balls j) ≤ ENNReal.ofReal (Cball * r ^ n))
    (hcard : (Fintype.card J : ℝ) * r ^ (n - 1) ≤ Ccover) :
    μ tube ≤ ENNReal.ofReal (Cball * Ccover * r) := by
…

def OAI.DukePrimeDegree.HasTubeDecay line 57
Source documentation
Uniform exponential tube bounds on each compact set. The constants are finite but may depend on the compact set.
```
def HasTubeDecay (μ : Measure X) (tube : ℝ → X → Set X) (rate : ℝ) : Prop :=
…
```
lemma OAI.DukePrimeDegree.HasTubeDecay.mono_rate line 62

lemma OAI.DukePrimeDegree.HasTubeDecay.of_le_smul line 74

Source documentation

Domination by a finite multiple preserves tube decay.

lemma HasTubeDecay.of_le_smul {μ ν : Measure X} {tube : ℝ → X → Set X}
    {rate : ℝ} (h : HasTubeDecay μ tube rate)
    (c : ℝ≥0∞) (hc : c ≠ ∞) (hν : ν ≤ c • μ) :
    HasTubeDecay ν tube rate := by
…

Mentions: OAI.DukePrimeDegree.HasTubeDecay

theorem OAI.DukePrimeDegree.tube_decay_of_ball_covers line 92

Source documentation

Exact specialization of the preceding finite-cover estimate with radius exp(-rate*t). The cover cardinalities and ball estimates are geometric hypotheses, separate from the published entropy criterion.

theorem tube_decay_of_ball_covers
    (μ : Measure X) (tube : ℝ → X → Set X)
    (n : ℕ) (hn : 1 ≤ n) (rate : ℝ)
    (hcovers : ∀ K : Set X, IsCompact K →
      ∃ Cball Ccover : ℝ, 0 ≤ Cball ∧ 0 ≤ Ccover ∧
        ∀ t : ℝ, 0 ≤ t → ∀ x ∈ K,
          ∃ (J : Type) (_ : Fintype J) (balls : J → Set X),
            tube t x ⊆ ⋃ j, balls j ∧
            (∀ j, μ (balls j) ≤ ENNReal.ofReal (Cball * Real.exp (-rate * t) ^ n)) ∧
            (Fintype.card J : ℝ) * Real.exp (-rate * t) ^ (n - 1) ≤ Ccover) :
    HasTubeDecay μ tube rate := by
…

Mentions: OAI.DukePrimeDegree.HasTubeDecay

theorem OAI.DukePrimeDegree.entropy_lower_bound_of_tube_decay line 115

Source documentation

The constant-sequence specialization of ELMV's tube criterion, using the flow and two-sided neighborhoods of Corollary 3.3.

theorem entropy_lower_bound_of_tube_decay
    (μ : Measure X) (flow : ℝ → X → X) (tube : ℝ → X → Set X)
    (entropy : Measure X → ℝ≥0∞) (rate : ℝ) (hrate : 0 < rate)
    (hprob : IsProbabilityMeasure μ)
    (hinv : ∀ t, Measure.map (flow t) μ = μ)
    (hdecay : HasTubeDecay μ tube rate)
    (elmv : ∀ (ν : Measure X) (η : ℝ), IsProbabilityMeasure ν →
      (∀ t, Measure.map (flow t) ν = ν) → 0 < η →
      HasTubeDecay ν tube (2 * η) → ENNReal.ofReal η ≤ entropy ν) :
    ENNReal.ofReal (rate / 3) ≤ entropy μ := by
…

Mentions: OAI.DukePrimeDegree.HasTubeDecay