eq_zero_on_right_half_plane_of_superexponential_decay

English

In any ordered additive group with a left‑monotone order, −a ≤ 0 iff 0 ≤ a.

Русский

Во всякой упорядоченной аддитивной группе с монотонным слева порядком, −a ≤ 0 тогда и только тогда, когда 0 ≤ a.

LaTeX

$$$$(-a) \\le 0 \\quad\\text{iff}\\quad 0 \\le a.$$$$

Lean4

/-- **Phragmen-Lindelöf principle** in the right half-plane. Let `f : ℂ → E` be a function such that

* `f` is differentiable in the open right half-plane and is continuous on its closure;
* `‖f z‖` is bounded from above by `A * exp(B * ‖z‖ ^ c)` on the open right half-plane
  for some `c < 2`;
* `‖f z‖` is bounded from above by a constant on the imaginary axis;
* `f x`, `x : ℝ`, tends to zero superexponentially fast as `x → ∞`:
  for any natural `n`, `exp (n * x) * ‖f x‖` tends to zero as `x → ∞`.

Then `f` is equal to zero on the closed right half-plane. -/
theorem eq_zero_on_right_half_plane_of_superexponential_decay (hd : DiffContOnCl ℂ f {z | 0 < z.re})
    (hexp : ∃ c < (2 : ℝ), ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ‖z‖ ^ c))
    (hre : SuperpolynomialDecay atTop expR fun x => ‖f x‖) (him : ∃ C, ∀ x : ℝ, ‖f (x * I)‖ ≤ C) :
    EqOn f 0 {z : ℂ | 0 ≤ z.re} :=
  by
  rcases him with
    ⟨C, hC⟩
      -- Due to continuity, it suffices to prove the equality on the open right half-plane.

  suffices ∀ z : ℂ, 0 < z.re → f z = 0 by
    simpa only [closure_setOf_lt_re] using
      EqOn.of_subset_closure this hd.continuousOn continuousOn_const subset_closure Subset.rfl
  set g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) => exp z ^ n • f z
  have hg : ∀ n z, ‖g n z‖ = expR z.re ^ n * ‖f z‖ := fun n z ↦ by simp only [g, norm_smul, norm_pow, norm_exp]
  intro z hz
  suffices H : ∀ n : ℕ, ‖g n z‖ ≤ C by
    contrapose! H
    simp only [hg]
    exact
      (((tendsto_pow_atTop_atTop_of_one_lt (Real.one_lt_exp_iff.2 hz)).atTop_mul_const (norm_pos_iff.2 H)).eventually
          (eventually_gt_atTop C)).exists
  intro n
  refine
    right_half_plane_of_tendsto_zero_on_real ((differentiable_exp.pow n).diffContOnCl.smul hd) ?_ ?_ (fun y => ?_) hz.le
  · rcases hexp with ⟨c, hc, B, hO⟩
    refine ⟨max c 1, max_lt hc one_lt_two, n + max B 0, .of_norm_left ?_⟩
    simp only [hg]
    refine ((isBigO_refl (fun z : ℂ => expR z.re ^ n) _).mul hO.norm_left).trans (.of_bound' ?_)
    filter_upwards [(eventually_cobounded_le_norm 1).filter_mono inf_le_left] with z hz
    simp only [← Real.exp_nat_mul, ← Real.exp_add, Real.norm_eq_abs, Real.abs_exp, add_mul]
    gcongr
    ·
      calc
        z.re ≤ ‖z‖ := re_le_norm _
        _ = ‖z‖ ^ (1 : ℝ) := (Real.rpow_one _).symm
        _ ≤ ‖z‖ ^ max c 1 := Real.rpow_le_rpow_of_exponent_le hz (le_max_right _ _)
    exacts [le_max_left _ _, hz, le_max_left _ _]
  · rw [tendsto_zero_iff_norm_tendsto_zero]; simp only [hg]
    exact hre n
  · rw [hg, re_ofReal_mul, I_re, mul_zero, Real.exp_zero, one_pow, one_mul]
    exact hC y

Похожие утверждения