UnaryTelescope.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The unary-segment energy telescope

This is the finite cancellation behind §10, equation src-28. The actual and propagated endpoint amounts agree, leaving only amplitude errors and the small baseline-denominator corrections.

theorem OAI.LipschitzHilbert.log_add_baseline line 20
theorem OAI.LipschitzHilbert.unary_log_telescope line 27

theorem OAI.LipschitzHilbert.unary_log_telescope_errors line 67

Source documentation

The telescope, with each surviving correction controlled by an actual logarithmic-energy error and the relative baseline drop.

theorem unary_log_telescope_errors (N : ℕ) (V W n h beta error : ℕ → ℝ)
    (hn : ∀ i ≤ N, 0 < n i)
    (hV : ∀ i ≤ N, n i ≤ V i) (hW : ∀ i ≤ N, n i ≤ W i)
    (hh : ∀ i < N, 0 ≤ h i) (hbeta : ∀ i < N, 0 < beta i)
    (hprediction : ∀ i < N, beta i ≤ V i / (h i + V (i + 1)))
    (hstar : ∀ i < N, W i ≤ h i + W (i + 1)) (hend : W N = V N)
    (herror : ∀ i ≤ N, |Real.log (V i) - Real.log (W i)| ≤ error i) :
    (∑ i ∈ Finset.range N, Real.log (beta i)) ≤ error 0 +
      ∑ i ∈ Finset.range N, (h i / n (i + 1)) * error (i + 1) := by
…

theorem OAI.LipschitzHilbert.unary_vertex_telescope line 99

Source documentation

Applying the scalar telescope to the actual vertex amounts gives the finite form of src-28 before the segment mass comparison.

theorem unary_vertex_telescope (N : ℕ) (n : ℕ → ℝ) (A Astar : ℕ → E)
    (beta : ℕ → ℝ) {a p D : ℝ} (hp : 1 ≤ p) (hap : a ≤ p)
    (hn : ∀ i ≤ N, 0 < n i) (hmass : ∀ i < N, n (i + 1) ≤ n i)
    (hcontraction : ∀ i < N, ‖Astar i‖ ≤ ‖Astar (i + 1)‖)
    (hend : Astar N = A N) (hbeta : ∀ i < N, 0 < beta i)
    (hprediction : ∀ i < N, beta i ≤ vertexAmount (n i) (A i) a p /
      (n i - n (i + 1) + vertexAmount (n (i + 1)) (A (i + 1)) a p))
    (herror : ∀ i ≤ N, ‖A i - Astar i‖ ≤ D) :
    (∑ i ∈ Finset.range N, Real.log (beta i)) ≤
      p * n 0 ^ ((a - 1) / p - 1) * D +
        ∑ i ∈ Finset.range N, ((n i - n (i + 1)) / n (i + 1)) *
          (p * n (i + 1) ^ ((a - 1) / p - 1) * D) := by
…

Mentions: OAI.LipschitzHilbert.vertexAmount

theorem OAI.LipschitzHilbert.unary_vertex_telescope_uniform line 132

Source documentation

A lower mass bound makes all the energy Lipschitz constants uniform. Only the sum of relative drops remains; no factor counts unary indices.

theorem unary_vertex_telescope_uniform (N : ℕ) (n : ℕ → ℝ) (A Astar : ℕ → E)
    (beta : ℕ → ℝ) {a p D m : ℝ} (hp : 1 ≤ p) (hap : a ≤ p)
    (hm : 0 < m) (hD : 0 ≤ D) (hn : ∀ i ≤ N, m ≤ n i)
    (hmass : ∀ i < N, n (i + 1) ≤ n i)
    (hcontraction : ∀ i < N, ‖Astar i‖ ≤ ‖Astar (i + 1)‖)
    (hend : Astar N = A N) (hbeta : ∀ i < N, 0 < beta i)
    (hprediction : ∀ i < N, beta i ≤ vertexAmount (n i) (A i) a p /
      (n i - n (i + 1) + vertexAmount (n (i + 1)) (A (i + 1)) a p))
    (herror : ∀ i ≤ N, ‖A i - Astar i‖ ≤ D) :
    (∑ i ∈ Finset.range N, Real.log (beta i)) ≤
      (p * m ^ ((a - 1) / p - 1) * D) *
        (1 + ∑ i ∈ Finset.range N, (n i - n (i + 1)) / n (i + 1)) := by
…

Mentions: OAI.LipschitzHilbert.vertexAmount

theorem OAI.LipschitzHilbert.segment_relative_drop_sum_le line 172

Source documentation

The mass drop over a segment telescopes even if the segment contains arbitrarily many very small unary drops.

theorem segment_relative_drop_sum_le (N : ℕ) (n : ℕ → ℝ) {m : ℝ} (hm : 0 < m)
    (hn : ∀ i ≤ N, m ≤ n i) (hmass : ∀ i < N, n (i + 1) ≤ n i) :
    (∑ i ∈ Finset.range N, (n i - n (i + 1)) / n (i + 1)) ≤ (n 0 - n N) / m := by
…

theorem OAI.LipschitzHilbert.half_mass_rpow_le line 187

theorem OAI.LipschitzHilbert.unary_vertex_telescope_short_segment line 202

Source documentation

The final src-28 estimate, with an explicit absolute constant, on a segment whose total mass drop is at most two.

theorem unary_vertex_telescope_short_segment {E : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E]
    (N : ℕ) (n : ℕ → ℝ) (A Astar : ℕ → E) (beta : ℕ → ℝ)
    {a p D : ℝ} (hp : 1 ≤ p) (ha : 1 ≤ a) (hap : a ≤ p) (hD : 0 ≤ D)
    (hstart : 4 ≤ n 0) (hn : ∀ i ≤ N, n 0 - 2 ≤ n i)
    (hmass : ∀ i < N, n (i + 1) ≤ n i)
    (hcontraction : ∀ i < N, ‖Astar i‖ ≤ ‖Astar (i + 1)‖)
    (hend : Astar N = A N) (hbeta : ∀ i < N, 0 < beta i)
    (hprediction : ∀ i < N, beta i ≤ vertexAmount (n i) (A i) a p /
      (n i - n (i + 1) + vertexAmount (n (i + 1)) (A (i + 1)) a p))
    (herror : ∀ i ≤ N, ‖A i - Astar i‖ ≤ D) :
    (∑ i ∈ Finset.range N, Real.log (beta i)) ≤
…

Mentions: OAI.LipschitzHilbert.vertexAmount