pulling continuity past integrals

Stream: Is there code for X?

[Alex Kontorovich]

Here's a funny situation. I have a continuous function $f$ on ℂ, and I want to know that, as $w \to z$, the vertical integral of $f$ from $\Im(z)$ to $\Im(w)$ having real part $\Re(w)$ differs from the same having real part $\Re(z)$ by $o(w-z)$. Basically, the integral should be bounded by $w-z$ times the difference of the functions inside, but the difference is going to zero too...? Is there a simple way to combine the two limits? Thanks!

example {f : ℂ → ℂ} (hf : Continuous f) {z : ℂ} :
  (fun (w : ℂ) => (∫ (y : ℝ) in z.im..w.im, f (w.re + y * I))
    - ∫ (y : ℝ) in z.im..w.im, f (z.re + y * I))
    =o[𝓝 z] fun w => w - z := by
  sorry

[Terence Tao]

You can subtract f z from both integrands and now you are integrating things of size $o(1)$ on integrals of length $O(|w-z|)$, so simple estimates would suffice here.

[Alex Kontorovich]

Interesting suggestion. I was instead thinking that it'd be easier to start by putting the two integrals together into ∫ (y : ℝ) in z.im..w.im, f (w.re + y * I) - f (z.re + y * I). Either way, it's that last part that I wanted help with.

Here's perhaps an even simpler setting that would already point me in the right direction: Say $f=o(1)$ as $w\to0$; is there a simple way of showing that this integral is $o(w)$?

import Mathlib

open Topology

example {f : ℂ → ℂ} (hf : Continuous f) (hf0 : f =o[𝓝 0] (1 : ℂ → ℂ)) :
    (fun (w : ℂ) ↦ ∫ (y : ℝ) in (0:ℝ)..w.im, f (w.re + y * I)) =o[𝓝 0] fun w => w := by
  sorry

[Alex Kontorovich]

I can do it if I resort to epsilons and deltas. I'm trying to see whether there is a "right" Mathlib-y way to do this...?

[Alex Kontorovich]

Let me try to be even more precise about where I'm stuck. How do I prove KeyFact below?

import Mathlib

open Topology

example {f : ℂ → ℂ} (hf : Continuous f) (hf0 : f =o[𝓝 0] (1 : ℂ → ℂ)) :
    (fun (w : ℂ) ↦ ∫ (y : ℝ) in (0:ℝ)..w.im, f (w.re + y * I)) =o[𝓝 0] fun w => w := by
  rw [Asymptotics.IsLittleO] at hf0 ⊢
  intro c c_pos
  have := hf0 c_pos
  rw [Asymptotics.isBigOWith_iff] at this ⊢
  simp only [Complex.norm_eq_abs, Pi.one_apply, norm_one, mul_one] at this
  filter_upwards [this]
  intro w hw
  have KeyFact : ∀ y > 0, y < w.im → Complex.abs (f (w.re + y * I)) ≤ c := sorry -- this is what I want!
  calc
    _ ≤ ‖∫ (y : ℝ) in (0 : ℝ)..w.im, c‖ := ?_
    _ ≤ c * ‖w‖ := ?_
  · sorry
  · simp only [intervalIntegral.integral_const, sub_zero, smul_eq_mul, norm_mul, Real.norm_eq_abs,
    Complex.norm_eq_abs]
    sorry

[Alex Kontorovich]

I'm using filter_upwards in the wrong way, but I don't know what the right way is...

[Terence Tao]

Honestly I would just epsilon-and-delta this claim rather than try to mess around with filters. (Filter_upwards is only useful when you only need finitely many points to lie in some suitable neighbourhood, but you want an entire interval, and so you may as as well first get a ball in the neighbourhood and then fit the interval inside the ball.)

[Terence Tao]

One can also get what you want from dominated convergence (and that continuous functions are bounded on compacta), after using an affine change of variables to keep the domain of integration a fixed interval, but this is using a sledgehammer to swat a fly. Or you could restrict to a compact set to make the function uniformly continuous and then invoke a modulus of continuity using e.g., docs#ContinuousMap.dist_lt_of_dist_lt_modulus , but again this is overkill.

[Patrick Massot]

I got nerd-snipped by the claim that epsilon-delta are better than filters here. I initially wanted to disprove this, but indeed in this situation I think that proving an abstract filter version wouldn't beat the elementary proof using the specific geometry of the situation. What I call the geometry of the situation is the claim that

$$\forall r \in \R, \forall w \in \mathbb C, w \in B_r(0) \implies \forall y \in \mathbb R, y \in [0, \Im w] \implies \Re w + iy \in B_r(0).$$

Clearly this geometrical fact isn't essential, but it does make the proof easier. However I couldn't find some lemmas that I wanted to use this geometry. So I came up with

import Mathlib

open Topology Complex

lemma le_iff_sq_le {R : Type*} [LinearOrderedRing R] {x y : R} (hx : 0 ≤ x) (hy : 0 ≤ y) :
    x ≤ y ↔ x^2 ≤ y^2 := by
  rw [sq_le_sq, _root_.abs_of_nonneg hx, _root_.abs_of_nonneg hy]

lemma abs_le_of_mem_uIoc_zero {A : Type*} [LinearOrderedAddCommGroup A] {x y : A} (h : x ∈ Ι 0 y) :
    |x| ≤ |y| := by
  rcases Set.mem_uIoc.1 h with (⟨hx, hxy⟩ | ⟨hxy, hx⟩)
  · rwa [abs_of_pos hx, abs_of_pos <| hx.trans_le hxy]
  · rw [abs_of_nonpos hx, abs_of_neg <| hxy.trans_le hx]
    exact neg_le_neg hxy.le

lemma sq_le_of_mem_uIoc_zero {R : Type*} [LinearOrderedRing R] {x y : R} (h : x ∈ Ι 0 y) :
    x^2 ≤ y^2 := by
  simpa using pow_le_pow_left (abs_nonneg x) (abs_le_of_mem_uIoc_zero h) 2

example {f : ℂ → ℂ} (hf0 : f =o[𝓝 0] (1 : ℂ → ℂ)) :
    (fun (w : ℂ) ↦ ∫ (y : ℝ) in (0:ℝ)..w.im, f (w.re + y * I)) =o[𝓝 0] fun w ↦ w := by
  rw [Asymptotics.IsLittleO] at hf0 ⊢
  intro c c_pos
  have := hf0 c_pos
  simp only [Asymptotics.isBigOWith_iff,Pi.one_apply, norm_one, mul_one ] at this ⊢
  have : ∀ᶠ (w : ℂ) in 𝓝 0, ∀ y ∈ Ι 0 w.im, ‖f (w.re + y * I)‖ ≤ c := by
    rw [Metric.nhds_basis_closedBall.eventually_iff] at this ⊢
    peel this with hε ε ε_pos
    intro w hw y hy
    apply hε
    rw [mem_closedBall_zero_iff, le_iff_sq_le, IsROrC.norm_sq_eq_def, ← pow_two, ← pow_two] at *
    suffices w.re^2 + y ^2 ≤ ε ^ 2 by simpa
    calc w.re^2 + y^2 ≤ w.re^2 + w.im^2 := by gcongr w.re^2 + ?_; exact sq_le_of_mem_uIoc_zero hy
     _                ≤ ε ^ 2  := by simpa using hw
    all_goals positivity
  exact this.mono fun w hw ↦ calc
    _ ≤ c * |w.im - 0|  := intervalIntegral.norm_integral_le_of_norm_le_const hw
    _ ≤ c * ‖w‖ := by gcongr; simp [w.abs_im_le_abs]

[Patrick Massot]

I think it isn't the first time I don't manage to find the first lemma above. Is it really missing?

[Johan Commelin]

Is there an auto-implicit $w$ in your math-display above?

[Patrick Massot]

No, it was a notation change in the middle.

[Johan Commelin]

Makes sense (-; My unusedVariable linter should have told me so.

[Patrick Massot]

I moved messages about the stupid ordered remiring lemma to clarify.

[Patrick Massot]

Returning to the main topic, notice the title of this thread is not very accurate since I removed the useless continuity assumption.

[Terence Tao]

If one really wants to avoid epsilon/delta, another way to proceed is to encode the geometric fact isolated by Patrick as the claim that the function $t \mapsto \mathrm{Re} w + i t \mathrm{Im} w$ converges in $t \in [0,1]$ uniformly to zero as $w \to w_0$, and then to have a general lemma that if $f(z)$ converges to $L$ as $z \to z_0$, and $t \mapsto g(w,t)$ converges uniformly in $t$ to $t \mapsto z_0$, then $t \mapsto f(g(w,t))$ converges uniformly in $t$ to $L$ as $w \to w_0$. (One can phrase this in terms of product filters, the uniform filter, and filter maps if desired.)