HalaszStationaryPhase.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Locate the unique possible stationary point and quantify the slope away from it on a positive finite interval.

lemma OAI.TwoPointCorrelations.halasz_log_slope_drop line 13
lemma OAI.TwoPointCorrelations.halasz_log_stationary_center line 24
theorem OAI.TwoPointCorrelations.halasz_log_stationary_integral line 58
Source documentation
Uniform square-root cancellation for an individual Poisson integral.
```
theorem halasz_log_stationary_integral (u v a b : ℝ) (hu : 0 < u)
    (ha : 0 < a) (hab : a ≤ b) :
    ‖∫ x in a..b, halaszLogPhase u v x‖ ≤ 10*b/Real.sqrt u := by
…
```
Mentions: OAI.TwoPointCorrelations.halaszLogPhase