The logarithmic phase

Reusable facts about the logarithmic model phase, including its derivatives, separation on dyadic intervals, and the explicit main term of its oscillatory integral.

noncomputable def Expdb.logPhase : VariableFunction (VariableObject.fixed ℝ) ℝ

The fixed logarithmic phase u ↦ log u, regarded as a variable family.

Equations

• Expdb.logPhase x✝ = Real.log

theorem Expdb.iteratedDerivWithin_log_eq_rpow_neg_one (p : ℕ) (u : ↑phaseInterval) : iteratedDerivWithin (p + 1) Real.log phaseInterval ↑u = iteratedDerivWithin p (modelPhase 1) phaseInterval ↑u

The derivatives of log on the phase interval agree with the reference derivatives for model exponent one.

theorem Expdb.isModelPhaseFunction_log : IsModelPhaseFunction logPhase

The fixed logarithmic phase u ↦ log u is a model phase function, with model exponent σ = 1.

theorem Expdb.log_div_separated {N : ℝ} {a b : ℕ} (hN : 0 < N) (ha : N ≤ ↑a) (hb : ↑b ≤ 2 * N) : IsSeparatedFamily (1 / (2 * N)) fun (n : ↥(Finset.Icc a b)) => Real.log (↑↑n / N)

On a dyadic interval, log (n / N) is 1 / (2 * N)-separated.

noncomputable def Expdb.logPhaseMainTerm (N T : ℝ) : ℂ

The explicit main term for the logarithmic oscillatory integral, equal to that integral when N > 0. The 2π factor in the normalization comes from Lean's Fourier character 𝐞.

Equations

• Expdb.logPhaseMainTerm N T = ↑N * (2 * ↑(Real.fourierChar (T * Real.log 2)) - 1) / (1 + 2 * ↑Real.pi * Complex.I * ↑T)

theorem Expdb.logPhase_integral_eq_mainTerm {N T : ℝ} (hN : 0 < N) : ∫ (x : ℝ) in N..2 * N, ↑(Real.fourierChar (T * Real.log (x / N))) = logPhaseMainTerm N T

The logarithmic oscillatory integral is exactly logPhaseMainTerm.

theorem Expdb.norm_logPhaseMainTerm_bounds {N T : ℝ} (hN : 0 < N) (hT : 1 ≤ T) : 1 / (1 + 2 * Real.pi) * (N / T) ≤ ‖logPhaseMainTerm N T‖ ∧ ‖logPhaseMainTerm N T‖ ≤ 3 / (2 * Real.pi) * (N / T)

The logarithmic main term has size comparable to N / T.