OAI/Analysis/LipschitzHilbert/Estimates/SmoothPrincipalValue.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Pointwise symmetric principal values for smooth inputs. At a fixed output point the direction is frozen, so differentiability of the input removes the singularity in the positive-time symmetric quotient.

  1. def OAI.LipschitzHilbert.smoothPrincipalValue line 20

    Source documentation

    The continuous extension at zero is integrated on the closed short scale. The value at zero has no effect on the integral.

    Distinct definitions of this name: ComparatorChallenges/LipschitzHilbert.lean:37 (same statement text; different proof or body). Qualify references as OAI.LipschitzHilbert.smoothPrincipalValue@path.

    def smoothPrincipalValue (v : DirectionPlane → DirectionPlane) (a : ℝ)
    (f : DirectionPlane → ℂ) (x : DirectionPlane) : ℂ :=
…

    Mentions: OAI.LipschitzHilbert.DirectionPlane

  2. theorem OAI.LipschitzHilbert.shortTransform_tendsto_smoothPrincipalValue line 25
  3. theorem OAI.LipschitzHilbert.twoSidedTruncation_tendsto_smoothPrincipalValue line 67