TopWeight.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

The actual decaying top weights and their motion along a reference line.

structure OAI.LipschitzHilbert.SlopeBox line 17
Source documentation
A top box in the manuscript's slope coordinates.
```
structure SlopeBox where
…
```
def OAI.LipschitzHilbert.SlopeBox.horizontal line 28
def OAI.LipschitzHilbert.SlopeBox.transverse line 30
def OAI.LipschitzHilbert.SlopeBox.radius line 33
def OAI.LipschitzHilbert.SlopeBox.weight line 35
def OAI.LipschitzHilbert.SlopeBox.lineShift line 38
theorem OAI.LipschitzHilbert.SlopeBox.radius_nonnegative line 40
theorem OAI.LipschitzHilbert.SlopeBox.weight_pos line 43
theorem OAI.LipschitzHilbert.SlopeBox.radius_line_motion line 50
theorem OAI.LipschitzHilbert.SlopeBox.log_weight line 78
theorem OAI.LipschitzHilbert.SlopeBox.log_weight_line_motion line 88
Source documentation
No differentiability of absolute values is needed: the logarithm of the actual weight has this global reference-line motion bound.
```
theorem log_weight_line_motion (T : SlopeBox) {K D : ℝ} (hK : 0 < K) (hD : 0 ≤ D)
    (s t : ℝ) (z : ℝ × ℝ) :
    |Real.log (T.weight K D (lineShift s t z)) - Real.log (T.weight K D z)| ≤
      (D / K) * (1 / T.length + |s - T.slope| / T.width) * |t| := by
…
```
Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.SlopeBox.lineShift
theorem OAI.LipschitzHilbert.SlopeBox.log_weight_same_slope line 115
Source documentation
On a cell of length at most the top length, the logarithm of its weight varies by an absolute constant along its own reference direction.
```
theorem log_weight_same_slope (T : SlopeBox) {K D t : ℝ}
    (hK : 1 ≤ K) (hD : 0 ≤ D) (ht : |t| ≤ T.length) (z : ℝ × ℝ) :
    |Real.log (T.weight K D (lineShift T.slope t z)) - Real.log (T.weight K D z)| ≤ D := by
…
```
Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.SlopeBox.lineShift

theorem OAI.LipschitzHilbert.positive_sum_log_motion line 133

Source documentation

Termwise logarithmic motion is inherited by every nonempty positive subsum, with the same constant. This applies equally to complementary masses.

theorem positive_sum_log_motion {ι : Type*} (s : Finset ι) (hne : s.Nonempty)
    (a b : ι → ℝ) {δ : ℝ}
    (ha : ∀ i ∈ s, 0 < a i) (hb : ∀ i ∈ s, 0 < b i)
    (hmotion : ∀ i ∈ s, |Real.log (b i) - Real.log (a i)| ≤ δ) :
    |Real.log (∑ i ∈ s, b i) - Real.log (∑ i ∈ s, a i)| ≤ δ := by
…

theorem OAI.LipschitzHilbert.top_mass_log_line_motion line 163

Source documentation

The manuscript's mass motion bound for any fixed nonempty top set, proved directly from its actual weights on every reference line.

theorem top_mass_log_line_motion {ι : Type*} (tops : ι → SlopeBox) (a : Finset ι)
    (hne : a.Nonempty) {K D C : ℝ} (hK : 0 < K) (hD : 0 ≤ D)
    (s t : ℝ) (z : ℝ × ℝ)
    (hlocal : ∀ i ∈ a,
      (D / K) * (1 / (tops i).length + |s - (tops i).slope| / (tops i).width) ≤ C) :
    |Real.log (∑ i ∈ a, (tops i).weight K D (SlopeBox.lineShift s t z)) -
      Real.log (∑ i ∈ a, (tops i).weight K D z)| ≤ C * |t| := by
…

Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.SlopeBox.lineShift