MRTAdaptiveDisk.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

A local analytic disk estimate with an explicit logarithmic growth budget. The statement is independent of the physical radius, so it can be used on the shrinking disks required by a Vinogradov--Korobov growth estimate.

def OAI.TwoPointCorrelations.mrtDiskZeros line 14
lemma OAI.TwoPointCorrelations.mrtDiskZeros_finite line 17
lemma OAI.TwoPointCorrelations.mrt_disk_factorization line 23

theorem OAI.TwoPointCorrelations.mrt_disk_logderiv line 46

Source documentation

Logarithmic derivative equals the actual finite zero sum with an error linear in the logarithmic growth budget.

theorem mrt_disk_logderiv (f : ℂ → ℂ)
    (hf : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, AnalyticAt ℂ f z)
    (h0 : f 0 = 1) {B : ℝ} (hB : 0 < B)
    (hbound : ∀ z ∈ Metric.closedBall (0 : ℂ) (15 / 16), ‖f z‖ ≤ Real.exp B)
    {z : ℂ} (hz : ‖z‖ ≤ 3 / 4) (hn : f z ≠ 0) :
    ‖deriv f z / f z -
      ∑ ρ ∈ (mrtDiskZeros_finite f hf h0).toFinset,
        (analyticOrderAt f ρ).toNat / (z - ρ)‖ ≤
      mrtCharacterLogDerivativeConstant * B := by
…

Mentions: OAI.TwoPointCorrelations.mrtDiskZeros_finite, OAI.TwoPointCorrelations.mrtCharacterLogDerivativeConstant

theorem OAI.TwoPointCorrelations.mrt_disk_zero_count line 66

Source documentation

The total multiplicity in the inner disk has the same logarithmic cost.

theorem mrt_disk_zero_count (f : ℂ → ℂ)
    (hf : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, AnalyticAt ℂ f z)
    (h0 : f 0 = 1) {B : ℝ} (hB : 0 < B)
    (hbound : ∀ z ∈ Metric.closedBall (0 : ℂ) (15 / 16), ‖f z‖ ≤ Real.exp B) :
    (∑ ρ ∈ (mrtDiskZeros_finite f hf h0).toFinset,
      ((analyticOrderAt f ρ).toNat : ℝ)) ≤
      (1 / Real.log ((15 / 16 : ℝ) / (7 / 8))) * B := by
…

Mentions: OAI.TwoPointCorrelations.mrtDiskZeros_finite

theorem OAI.TwoPointCorrelations.mrt_disk_logderiv_norm line 80

Source documentation

A zero separation estimate completes the local norm bound.

theorem mrt_disk_logderiv_norm (f : ℂ → ℂ)
    (hf : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, AnalyticAt ℂ f z)
    (h0 : f 0 = 1) {B : ℝ} (hB : 0 < B)
    (hbound : ∀ z ∈ Metric.closedBall (0 : ℂ) (15 / 16), ‖f z‖ ≤ Real.exp B)
    {z : ℂ} (hz : ‖z‖ ≤ 3 / 4) (hn : f z ≠ 0)
    {η : ℝ} (hη : 0 < η)
    (hd : ∀ ρ ∈ mrtDiskZeros f, η ≤ ‖z - ρ‖) :
    ‖deriv f z / f z‖ ≤
      (mrtCharacterLogDerivativeConstant +
        (1 / Real.log ((15 / 16 : ℝ) / (7 / 8))) / η) * B := by
…

Mentions: OAI.TwoPointCorrelations.mrtDiskZeros, OAI.TwoPointCorrelations.mrtCharacterLogDerivativeConstant