Elementary bounds

theorem CommutingRepetition.StripCauchy.abs_sinh_im_le_norm_sin (z : ℂ) : |Real.sinh z.im| ≤ ‖Complex.sin z‖

|sinh (Im z)| ≤ ‖sin z‖.

theorem CommutingRepetition.StripCauchy.exp_div_four_le_sinh {x : ℝ} (hx : 1 ≤ x) : Real.exp x / 4 ≤ Real.sinh x

e^x / 4 ≤ sinh x for x ≥ 1.

theorem CommutingRepetition.StripCauchy.exp_abs_div_two_le_cosh (x : ℝ) : Real.exp |x| / 2 ≤ Real.cosh x

e^{|x|} / 2 ≤ cosh x.

theorem CommutingRepetition.StripCauchy.exp_neg_le_inv_one_add_sq {a : ℝ} (ha : 0 < a) {s : ℝ} (hs : 0 ≤ s) : Real.exp (-(a * s)) ≤ max 1 (2 / a ^ 2) * (1 + s ^ 2)⁻¹

e^{-a s} ≤ C_a (1 + s²)⁻¹ for s ≥ 0, a > 0.

noncomputable def CommutingRepetition.StripCauchy.w (φ t : ℝ) : ℝ

The weight w φ t = e^{-φt} / (2 cosh(πt)).

Equations

• CommutingRepetition.StripCauchy.w φ t = Real.exp (-φ * t) / (2 * Real.cosh (Real.pi * t))

theorem CommutingRepetition.StripCauchy.continuous_w (φ : ℝ) : Continuous (w φ)

theorem CommutingRepetition.StripCauchy.w_pos (φ t : ℝ) : 0 < w φ t

theorem CommutingRepetition.StripCauchy.w_le_exp {φ : ℝ} (t : ℝ) : w φ t ≤ Real.exp (-((Real.pi - |φ|) * |t|))

w φ t ≤ e^{-(π-|φ|)|t|}.

theorem CommutingRepetition.StripCauchy.w_le_inv_one_add_sq {φ : ℝ} (hφ : |φ| < Real.pi) (t : ℝ) : w φ t ≤ max 1 (2 / (Real.pi - |φ|) ^ 2) * (1 + t ^ 2)⁻¹

w φ is dominated by C (1 + t²)⁻¹.

theorem CommutingRepetition.StripCauchy.integrable_w_mul {φ : ℝ} (hφ : |φ| < Real.pi) {v : ℝ → ℂ} (hv : MeasureTheory.AEStronglyMeasurable v MeasureTheory.volume) {C : ℝ} (hC : ∀ (t : ℝ), ‖v t‖ ≤ C) : MeasureTheory.Integrable (fun (t : ℝ) => ↑(w φ t) * v t) MeasureTheory.volume

Integrability of t ↦ w φ t • v t for bounded measurable v.

Values of sin on the boundary lines and the kernel (1/4 + t²)⁻¹

theorem CommutingRepetition.StripCauchy.sin_pi_mul_half_add (t : ℝ) : Complex.sin (↑Real.pi * (1 / 2 + ↑t * Complex.I)) = ↑(Real.cosh (Real.pi * t))

theorem CommutingRepetition.StripCauchy.sin_pi_mul_neg_half_add (t : ℝ) : Complex.sin (↑Real.pi * (-1 / 2 + ↑t * Complex.I)) = -↑(Real.cosh (Real.pi * t))

theorem CommutingRepetition.StripCauchy.half_add_ne_zero (t : ℝ) : 1 / 2 + ↑t * Complex.I ≠ 0

theorem CommutingRepetition.StripCauchy.neg_half_add_ne_zero (t : ℝ) : -1 / 2 + ↑t * Complex.I ≠ 0

theorem CommutingRepetition.StripCauchy.inv_sub_inv_eq (t : ℝ) : (1 / 2 + ↑t * Complex.I)⁻¹ - (-1 / 2 + ↑t * Complex.I)⁻¹ = ↑(1 / 4 + t ^ 2)⁻¹

theorem CommutingRepetition.StripCauchy.integrable_inv_quarter_add_sq : MeasureTheory.Integrable (fun (t : ℝ) => (1 / 4 + t ^ 2)⁻¹) MeasureTheory.volume

theorem CommutingRepetition.StripCauchy.integral_inv_quarter_add_sq : ∫ (t : ℝ), (1 / 4 + t ^ 2)⁻¹ = 2 * Real.pi

The functions S, ψ, G, H

def CommutingRepetition.StripCauchy.strip : Set ℂ

The closed strip.

Equations

• CommutingRepetition.StripCauchy.strip = {z : ℂ | |z.re| ≤ 1 / 2}

def CommutingRepetition.StripCauchy.ostrip : Set ℂ

The open strip.

Equations

• CommutingRepetition.StripCauchy.ostrip = {z : ℂ | |z.re| < 1 / 2}

theorem CommutingRepetition.StripCauchy.isOpen_ostrip : IsOpen ostrip

theorem CommutingRepetition.StripCauchy.ostrip_subset_strip : ostrip ⊆ strip

theorem CommutingRepetition.StripCauchy.zero_mem_ostrip : 0 ∈ ostrip

theorem CommutingRepetition.StripCauchy.ostrip_mem_nhds : ostrip ∈ nhds 0

theorem CommutingRepetition.StripCauchy.strip_mem_nhds : strip ∈ nhds 0

noncomputable def CommutingRepetition.StripCauchy.S : ℂ → ℂ

S z = sin(πz)/z, with S 0 = π.

Equations

• CommutingRepetition.StripCauchy.S = dslope (fun (z : ℂ) => Complex.sin (↑Real.pi * z)) 0

theorem CommutingRepetition.StripCauchy.differentiable_sinPi : Differentiable ℂ fun (z : ℂ) => Complex.sin (↑Real.pi * z)

theorem CommutingRepetition.StripCauchy.differentiable_S : Differentiable ℂ S

theorem CommutingRepetition.StripCauchy.S_zero : S 0 = ↑Real.pi

theorem CommutingRepetition.StripCauchy.S_of_ne {z : ℂ} (hz : z ≠ 0) : S z = Complex.sin (↑Real.pi * z) / z

theorem CommutingRepetition.StripCauchy.S_ne_zero {z : ℂ} (hz : z ∈ strip) : S z ≠ 0

noncomputable def CommutingRepetition.StripCauchy.ψ : ℂ → ℂ

ψ z = πz / sin(πz) = π / S z.

Equations

• CommutingRepetition.StripCauchy.ψ z = ↑Real.pi / CommutingRepetition.StripCauchy.S z

theorem CommutingRepetition.StripCauchy.ψ_zero : ψ 0 = 1

theorem CommutingRepetition.StripCauchy.differentiableOn_ψ : DifferentiableOn ℂ ψ strip

theorem CommutingRepetition.StripCauchy.ψ_of_ne {z : ℂ} (hz : z ≠ 0) : ψ z = ↑Real.pi * z / Complex.sin (↑Real.pi * z)

noncomputable def CommutingRepetition.StripCauchy.g (f : ℂ → ℂ) (φ : ℝ) : ℂ → ℂ

g z = e^{iφz} f z.

Equations

• CommutingRepetition.StripCauchy.g f φ z = Complex.exp (Complex.I * ↑φ * z) * f z

noncomputable def CommutingRepetition.StripCauchy.G (f : ℂ → ℂ) (φ : ℝ) : ℂ → ℂ

G = g ψ.

Equations

• CommutingRepetition.StripCauchy.G f φ z = CommutingRepetition.StripCauchy.g f φ z * CommutingRepetition.StripCauchy.ψ z

noncomputable def CommutingRepetition.StripCauchy.H (f : ℂ → ℂ) (φ : ℝ) : ℂ → ℂ

H = dslope G 0.

Equations

• CommutingRepetition.StripCauchy.H f φ = dslope (CommutingRepetition.StripCauchy.G f φ) 0

theorem CommutingRepetition.StripCauchy.G_zero (f : ℂ → ℂ) (φ : ℝ) : G f φ 0 = f 0

theorem CommutingRepetition.StripCauchy.continuousOn_G (f : ℂ → ℂ) (φ : ℝ) (hf_cont : ContinuousOn f strip) (hf_diff : DifferentiableOn ℂ f ostrip) : ContinuousOn (G f φ) strip

theorem CommutingRepetition.StripCauchy.differentiableOn_G (f : ℂ → ℂ) (φ : ℝ) (hf_cont : ContinuousOn f strip) (hf_diff : DifferentiableOn ℂ f ostrip) : DifferentiableOn ℂ (G f φ) ostrip

theorem CommutingRepetition.StripCauchy.differentiableAt_G_zero (f : ℂ → ℂ) (φ : ℝ) (hf_cont : ContinuousOn f strip) (hf_diff : DifferentiableOn ℂ f ostrip) : DifferentiableAt ℂ (G f φ) 0

theorem CommutingRepetition.StripCauchy.continuousOn_H (f : ℂ → ℂ) (φ : ℝ) (hf_cont : ContinuousOn f strip) (hf_diff : DifferentiableOn ℂ f ostrip) : ContinuousOn (H f φ) strip

theorem CommutingRepetition.StripCauchy.differentiableOn_H (f : ℂ → ℂ) (φ : ℝ) (hf_cont : ContinuousOn f strip) (hf_diff : DifferentiableOn ℂ f ostrip) : DifferentiableOn ℂ (H f φ) ostrip

theorem CommutingRepetition.StripCauchy.H_of_ne (f : ℂ → ℂ) (φ : ℝ) {z : ℂ} (hz : z ≠ 0) : H f φ z = (G f φ z - f 0) / z

theorem CommutingRepetition.StripCauchy.rect_eq_zero (f : ℂ → ℂ) (φ : ℝ) (hf_cont : ContinuousOn f strip) (hf_diff : DifferentiableOn ℂ f ostrip) (N : ℝ) : (((∫ (x : ℝ) in -1 / 2..1 / 2, H f φ (↑x + -↑N * Complex.I)) - ∫ (x : ℝ) in -1 / 2..1 / 2, H f φ (↑x + ↑N * Complex.I)) + Complex.I • ∫ (y : ℝ) in -N..N, H f φ (1 / 2 + ↑y * Complex.I)) - Complex.I • ∫ (y : ℝ) in -N..N, H f φ (-1 / 2 + ↑y * Complex.I) = 0

The rectangle [-1/2, 1/2] × [-N, N]: Cauchy–Goursat for H.

theorem CommutingRepetition.StripCauchy.zero_mem_strip : 0 ∈ strip

theorem CommutingRepetition.StripCauchy.half_add_mem_strip (y : ℝ) : 1 / 2 + ↑y * Complex.I ∈ strip

theorem CommutingRepetition.StripCauchy.neg_half_add_mem_strip (y : ℝ) : -1 / 2 + ↑y * Complex.I ∈ strip

theorem CommutingRepetition.StripCauchy.norm_exp_I_mul (φ : ℝ) (z : ℂ) : ‖Complex.exp (Complex.I * ↑φ * z)‖ = Real.exp (-(φ * z.im))

theorem CommutingRepetition.StripCauchy.norm_G_le (f : ℂ → ℂ) (φ : ℝ) {C : ℝ} (hf_bdd : ∀ z ∈ strip, ‖f z‖ ≤ C) {z : ℂ} (hz : z ∈ strip) (hN : 1 ≤ |z.im|) : ‖G f φ z‖ ≤ 8 * Real.pi * C * |z.im| * Real.exp (-((Real.pi - |φ|) * |z.im|))

The bound on G away from the real axis.

theorem CommutingRepetition.StripCauchy.norm_H_le (f : ℂ → ℂ) (φ : ℝ) {C : ℝ} (hf_bdd : ∀ z ∈ strip, ‖f z‖ ≤ C) {z : ℂ} (hz : z ∈ strip) (hN : 1 ≤ |z.im|) : ‖H f φ z‖ ≤ 8 * Real.pi * C * Real.exp (-((Real.pi - |φ|) * |z.im|)) + ‖f 0‖ / |z.im|

The bound on H away from the real axis.

theorem CommutingRepetition.StripCauchy.norm_edge_le (f : ℂ → ℂ) (φ : ℝ) {C : ℝ} (hf_bdd : ∀ z ∈ strip, ‖f z‖ ≤ C) {y : ℝ} (hy : 1 ≤ |y|) : ‖∫ (x : ℝ) in -1 / 2..1 / 2, H f φ (↑x + ↑y * Complex.I)‖ ≤ 8 * Real.pi * C * Real.exp (-((Real.pi - |φ|) * |y|)) + ‖f 0‖ / |y|

The horizontal edges: ‖∫ H(x + yI) dx‖ ≤ 8πC e^{-(π-|φ|)|y|} + ‖f 0‖/|y| for |y| ≥ 1.

theorem CommutingRepetition.StripCauchy.tendsto_edges (f : ℂ → ℂ) (φ : ℝ) {C : ℝ} (hf_bdd : ∀ z ∈ strip, ‖f z‖ ≤ C) (hφ : |φ| < Real.pi) : Filter.Tendsto (fun (N : ℕ) => (∫ (x : ℝ) in -1 / 2..1 / 2, H f φ (↑x + -↑N * Complex.I)) - ∫ (x : ℝ) in -1 / 2..1 / 2, H f φ (↑x + ↑N * Complex.I)) Filter.atTop (nhds 0)

The horizontal edges vanish as N → ∞.

noncomputable def CommutingRepetition.StripCauchy.V (f : ℂ → ℂ) (φ : ℝ) : ℝ → ℂ

The vertical-edge integrand: V t = G(1/2+it)/(1/2+it) − G(-1/2+it)/(-1/2+it).

Equations

• One or more equations did not get rendered due to their size.

theorem CommutingRepetition.StripCauchy.H_sub_H (f : ℂ → ℂ) (φ y : ℝ) : H f φ (1 / 2 + ↑y * Complex.I) - H f φ (-1 / 2 + ↑y * Complex.I) = V f φ y - f 0 * ↑(1 / 4 + y ^ 2)⁻¹

theorem CommutingRepetition.StripCauchy.V_eq (f : ℂ → ℂ) (φ y : ℝ) : V f φ y = 2 * ↑Real.pi * (↑(w φ y) * (Complex.exp (Complex.I * ↑φ / 2) * f (1 / 2 + ↑y * Complex.I) + Complex.exp (-(Complex.I * ↑φ / 2)) * f (-1 / 2 + ↑y * Complex.I)))

The explicit form of V.

theorem CommutingRepetition.StripCauchy.continuous_V (f : ℂ → ℂ) (φ : ℝ) (hf_cont : ContinuousOn f strip) (hf_diff : DifferentiableOn ℂ f ostrip) : Continuous (V f φ)

theorem CommutingRepetition.StripCauchy.integrable_V (f : ℂ → ℂ) (φ : ℝ) (hf_cont : ContinuousOn f strip) (hf_diff : DifferentiableOn ℂ f ostrip) {C : ℝ} (hf_bdd : ∀ z ∈ strip, ‖f z‖ ≤ C) (hφ : |φ| < Real.pi) : MeasureTheory.Integrable (V f φ) MeasureTheory.volume

theorem CommutingRepetition.StripCauchy.integral_V (f : ℂ → ℂ) (φ : ℝ) (hf_cont : ContinuousOn f strip) (hf_diff : DifferentiableOn ℂ f ostrip) {C : ℝ} (hf_bdd : ∀ z ∈ strip, ‖f z‖ ≤ C) (hφ : |φ| < Real.pi) : ∫ (y : ℝ), V f φ y = 2 * ↑Real.pi * f 0

∫ V = 2π f 0.

theorem CommutingRepetition.StripCauchy.strip_cauchy (f : ℂ → ℂ) (φ : ℝ) (hf_cont : ContinuousOn f strip) (hf_diff : DifferentiableOn ℂ f ostrip) {C : ℝ} (hf_bdd : ∀ z ∈ strip, ‖f z‖ ≤ C) (hφ : |φ| < Real.pi) : f 0 = ∫ (t : ℝ), ↑(w φ t) * (Complex.exp (Complex.I * ↑φ / 2) * f (1 / 2 + ↑t * Complex.I) + Complex.exp (-(Complex.I * ↑φ / 2)) * f (-1 / 2 + ↑t * Complex.I))

RvD Lemma 4.6 (Cauchy's formula on the strip): for f bounded continuous on |Re z| ≤ 1/2 and analytic inside, and |φ| < π, f 0 = ∫ t, e^{-φt}/(2cosh πt) · (e^{iφ/2} f(1/2 + it) + e^{-iφ/2} f(-1/2 + it)) dt.