WitnessTransfer.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Moving an actual popularity witness to a fixed reference line.

def OAI.LipschitzHilbert.SlopeBox.referencePoint line 16
Source documentation
The point at horizontal coordinate w.1 on the reference line through z.
```
def referencePoint (s : ℝ) (z w : ℝ × ℝ) : ℝ × ℝ :=
…
```
theorem OAI.LipschitzHilbert.SlopeBox.horizontal_sub_identity line 19
theorem OAI.LipschitzHilbert.SlopeBox.transverse_sub_identity line 25
theorem OAI.LipschitzHilbert.SlopeBox.referencePoint_vertical_distance line 36
Source documentation
Box coordinates give the vertical distance to the reference line using only the two actual points, with no choice of a point in a projection fiber.
```
theorem referencePoint_vertical_distance (T : SlopeBox) (s : ℝ) (z w : ℝ × ℝ) :
    |w.2 - (referencePoint s z w).2| ≤
      (T.radius w + T.radius z) * (T.width + T.length * |T.slope - s|) := by
…
```
Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.SlopeBox.referencePoint
theorem OAI.LipschitzHilbert.SlopeBox.referencePoint_vertical_distance_le line 70

theorem OAI.LipschitzHilbert.SlopeBox.referencePoint_slope_error line 82

Source documentation

The two points have the same horizontal coordinate, so a Lipschitz slope field loses precisely their vertical distance.

theorem referencePoint_slope_error (T : SlopeBox) (s : ℝ) (z w : ℝ × ℝ)
    (u : ℝ × ℝ → ℝ) {L : ℝ≥0} (hu : LipschitzWith L u) {δ A K : ℝ}
    (huw : |u w - T.slope| ≤ δ) (hw : T.radius w ≤ A) (hz : T.radius z ≤ K) :
    |u (referencePoint s z w) - T.slope| ≤
      δ + L * ((A + K) * (T.width + T.length * |T.slope - s|)) := by
…

Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.SlopeBox.referencePoint

theorem OAI.LipschitzHilbert.SlopeBox.transferred_slope_precision line 102

Source documentation

The paper's small-time condition transfers a witness of precision d to the reference line with angular error at most (c+1)Δ/B². The width is the actual enlarged width m * length * d, and B² ≤ m.

theorem transferred_slope_precision (T : SlopeBox) (s : ℝ) (z w : ℝ × ℝ)
    (u : ℝ × ℝ → ℝ) {L : ℝ≥0} (hu : LipschitzWith L u)
    {d m B c A K P : ℝ} (hd : 0 ≤ d) (hB : 0 < B) (hc : 0 ≤ c)
    (hw : T.radius w ≤ A) (hz : T.radius z ≤ K) (hP : A + K ≤ P)
    (hwidth : T.width = m * T.length * d) (hm : B ^ 2 ≤ m)
    (hprecision : d ≤ |T.slope - s| / B ^ 2)
    (hsmall : L * P * m * T.length ≤ 1 / 2)
    (huw : |u w - T.slope| ≤ c * d) :
    |u (referencePoint s z w) - T.slope| ≤ (c + 1) * |T.slope - s| / B ^ 2 := by
…

Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.SlopeBox.referencePoint