Truncation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The relation between the two-sided hard cutoff and positive-time symmetrization.

def OAI.LipschitzHilbert.directionalKernel line 13
Also declared: ComparatorChallenges/LipschitzHilbert.lean:26 (same declaration text).
def OAI.LipschitzHilbert.twoSidedTruncation line 18
Source documentation
The negative and positive parts of the original hard-truncated integral.
Also declared: ComparatorChallenges/LipschitzHilbert.lean:31 (same declaration text).
```
def twoSidedTruncation (v : DirectionPlane → DirectionPlane) (ε a : ℝ)
    (f : DirectionPlane → ℂ) (x : DirectionPlane) : ℂ :=
…
```
Mentions: OAI.LipschitzHilbert.DirectionPlane
theorem OAI.LipschitzHilbert.directionalKernel_intervalIntegrable line 23
theorem OAI.LipschitzHilbert.twoSidedTruncation_eq_shortTransform line 33
Source documentation
Symmetrization is an exact identity for every positive hard inner cutoff.
```
theorem twoSidedTruncation_eq_shortTransform
    (v : DirectionPlane → DirectionPlane) {f : DirectionPlane → ℂ} (hf : Continuous f)
    {ε a : ℝ} (hε : 0 < ε) (ha : ε ≤ a) (x : DirectionPlane) :
    twoSidedTruncation v ε a f x = shortTransform v ε a f x := by
…
```
Mentions: OAI.LipschitzHilbert.DirectionPlane, OAI.LipschitzHilbert.twoSidedTruncation, OAI.LipschitzHilbert.shortTransform