TopLogAbsorption.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The logarithmic endpoint factor is absorbed by the spare decay of an actual top weight, without any positive lower cutoff on that weight.

theorem OAI.LipschitzHilbert.bounded_weight_rpow_le_linear line 13

theorem OAI.LipschitzHilbert.top_log_absorption line 29

Source documentation

Small weights have no logarithmic singularity after the available polynomial decay is used. The total mass enters only through its logarithm.

theorem top_log_absorption {h S C Q q : ℝ} {d : ℕ}
    (hh : 0 < h) (hS : 0 < S) (hC : 1 ≤ C) (hhC : h ≤ C)
    (hQ : 0 ≤ Q) (hq : 2 ≤ q) (hqd : q ≤ (d : ℝ)+1) :
    h^q * (1+Q*Real.log (S/h)) ≤
      C^d * (1+Q*(Real.log (max 1 S)+1))*h := by
…

theorem OAI.LipschitzHilbert.normalized_top_amplitude_bound line 61

Source documentation

The concentration envelope and endpoint normalization combine to a bound linear in the top weight, even when that weight tends to zero.

theorem normalized_top_amplitude_bound {E : Type*} [NormedAddCommGroup E]
    (v : E) {h n0 nM S C B Q a : ℝ}
    (hh : 0 < h) (hhn : h ≤ nM) (hn : nM ≤ n0) (hnS : n0 ≤ S)
    (hC : 1 ≤ C) (hhC : h ≤ C) (hB : 0 ≤ B) (hQ : 0 ≤ Q)
    (ha0 : 0 ≤ a) (ha1 : a ≤ 1)
    (hv : ‖v‖ ≤ (h^(-a)*(1+Q*Real.log (n0/nM)))*(B*h^8)) :
    ‖v‖ ≤ (C^8*B*(1+Q*(Real.log (max 1 S)+1)))*h := by
…

theorem OAI.LipschitzHilbert.top_log_absorption_four line 94

Source documentation

The four powers retained in the manuscript's individual-top bound.

theorem top_log_absorption_four {h S C Q a : ℝ}
    (hh : 0 < h) (hS : 0 < S) (hC : 1 ≤ C) (hhC : h ≤ C)
    (hQ : 0 ≤ Q) (ha0 : 0 ≤ a) (ha1 : a ≤ 1) :
    h^(8-a) * (1+Q*Real.log (S/h)) ≤
      C^8 * (1+Q*(Real.log (max 1 S)+1))*h^4 := by
…

theorem OAI.LipschitzHilbert.normalized_top_amplitude_bound_four line 114

Source documentation

The normalized source amplitude retains four powers of the top weight, uniformly down to arbitrarily small positive weights.

theorem normalized_top_amplitude_bound_four {E : Type*} [NormedAddCommGroup E]
    (v : E) {h n0 nM S C B Q a : ℝ}
    (hh : 0 < h) (hhn : h ≤ nM) (hn : nM ≤ n0) (hnS : n0 ≤ S)
    (hC : 1 ≤ C) (hhC : h ≤ C) (hB : 0 ≤ B) (hQ : 0 ≤ Q)
    (ha0 : 0 ≤ a) (ha1 : a ≤ 1)
    (hv : ‖v‖ ≤ (h^(-a)*(1+Q*Real.log (n0/nM)))*(B*h^8)) :
    ‖v‖ ≤ (C^8*B*(1+Q*(Real.log (max 1 S)+1)))*h^4 := by
…