FrozenDirection.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Frozen-direction sampling

The sampling maps and positive-time representation of the short Hilbert transform in §1 of A uniform Hilbert transform estimate for Lipschitz directions. The direction in these definitions is evaluated at the output point.

abbrev OAI.LipschitzHilbert.DirectionPlane line 26
Also declared: ComparatorChallenges/LipschitzHilbert.lean:16 (same declaration text).
def OAI.LipschitzHilbert.sample line 29
Source documentation
Sampling along the straight line through the output point.
Also declared: ComparatorChallenges/LipschitzHilbert.lean:18 (same declaration text).
```
def sample (v : DirectionPlane → DirectionPlane) (t : ℝ) (x : DirectionPlane) :
    DirectionPlane := x - t • v x
```
Mentions: OAI.LipschitzHilbert.DirectionPlane
def OAI.LipschitzHilbert.shortTransform line 33
Source documentation
The positive-time, symmetrized short directional Hilbert transform.
Also declared: ComparatorChallenges/LipschitzHilbert.lean:22 (same declaration text).
```
def shortTransform (v : DirectionPlane → DirectionPlane) (ε a : ℝ)
    (f : DirectionPlane → ℂ) (x : DirectionPlane) : ℂ :=
…
```
Mentions: OAI.LipschitzHilbert.DirectionPlane
theorem OAI.LipschitzHilbert.sample_sub line 37

theorem OAI.LipschitzHilbert.sample_dist_le line 44

Source documentation

The elementary upper distortion estimate used before changing variables.

theorem sample_dist_le {v : DirectionPlane → DirectionPlane} {K : ℝ≥0}
    (hv : LipschitzWith K v) (t : ℝ) (x y : DirectionPlane) :
    dist (sample v t x) (sample v t y) ≤
      (1 + |t| * (K : ℝ)) * dist x y := by
…

Mentions: OAI.LipschitzHilbert.DirectionPlane, OAI.LipschitzHilbert.sample

theorem OAI.LipschitzHilbert.sample_dist_ge line 60

Source documentation

The lower distortion estimate; it has content when |t| K < 1.

theorem sample_dist_ge {v : DirectionPlane → DirectionPlane} {K : ℝ≥0}
    (hv : LipschitzWith K v) (t : ℝ) (x y : DirectionPlane) :
    (1 - |t| * (K : ℝ)) * dist x y ≤ dist (sample v t x) (sample v t y) := by
…

Mentions: OAI.LipschitzHilbert.DirectionPlane, OAI.LipschitzHilbert.sample

theorem OAI.LipschitzHilbert.sample_injective line 74
def OAI.LipschitzHilbert.rescaleField line 85
Source documentation
The usual reciprocal-Lipschitz normalization of a vector field.
```
def rescaleField (L : ℝ) (v : DirectionPlane → DirectionPlane) :
    DirectionPlane → DirectionPlane := fun x => v (L⁻¹ • x)
```
Mentions: OAI.LipschitzHilbert.DirectionPlane
def OAI.LipschitzHilbert.rescaleFunction line 88
theorem OAI.LipschitzHilbert.sample_rescale line 91
theorem OAI.LipschitzHilbert.rescaleField_unit line 96
theorem OAI.LipschitzHilbert.rescaleField_lipschitz line 100

theorem OAI.LipschitzHilbert.shortTransform_rescale line 114

Source documentation

Dilation intertwines the two hard truncation endpoints exactly.

theorem shortTransform_rescale {L : ℝ} (hL : L ≠ 0)
    (v : DirectionPlane → DirectionPlane) (ε a : ℝ)
    (f : DirectionPlane → ℂ) (x : DirectionPlane) :
    shortTransform (rescaleField L v) (L * ε) (L * a) (rescaleFunction L f) (L • x) =
      shortTransform v ε a f x := by
…

Mentions: OAI.LipschitzHilbert.DirectionPlane, OAI.LipschitzHilbert.shortTransform, OAI.LipschitzHilbert.rescaleField, OAI.LipschitzHilbert.rescaleFunction