PhragmenLindelof.eq_zero_on_right_half_plane_of_superexponential_decay
theorem PhragmenLindelof.eq_zero_on_right_half_plane_of_superexponential_decay :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E},
DiffContOnCl ℂ f {z | 0 < z.re} →
(∃ c < 2,
∃ B, f =O[Bornology.cobounded ℂ ⊓ Filter.principal {z | 0 < z.re}] fun z => (B * Complex.abs z ^ c).exp) →
(Asymptotics.SuperpolynomialDecay Filter.atTop Real.exp fun x => ‖f ↑x‖) →
(∃ C, ∀ (x : ℝ), ‖f (↑x * Complex.I)‖ ≤ C) → Set.EqOn f 0 {z | 0 ≤ z.re}
The Phragmén-Lindelöf principle in the right half-plane states the following: consider a function `f : ℂ → E` with the following properties:
- `f` is differentiable in the open right half-plane and is continuous on its closure,
- The norm of `f(z)`, `‖f z‖`, is bounded from above by `A * exp(B * (abs z) ^ c)` on the open right half-plane for some `c < 2`,
- The norm of `f(z)`, `‖f z‖`, is bounded from above by a constant on the imaginary axis,
- `f(x)`, where `x` is a real number, tends to zero superexponentially fast as `x → ∞` in the sense that for any natural number `n`, the product `exp (n * x) * ‖f x‖` tends to zero as `x → ∞`.
Then, the theorem asserts that `f` is equal to zero on the closed right half-plane. This theorem is a complex analysis result which provides a condition under which a bounded holomorphic function can be extended to a constant function. The name "Phragmén-Lindelöf" is in honor of the mathematicians Per Leonard Phragmén and Ernst Leonard Lindelöf who first proved similar results.
More concisely: If a differentiable function `f : ℂ → E` with bounded growth in the right half-plane and superexponential decay on the imaginary axis is continuous on its closure, then `f` is the zero function on the closed right half-plane.
|
PhragmenLindelof.right_half_plane_of_bounded_on_real
theorem PhragmenLindelof.right_half_plane_of_bounded_on_real :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {C : ℝ} {f : ℂ → E} {z : ℂ},
DiffContOnCl ℂ f {z | 0 < z.re} →
(∃ c < 2,
∃ B, f =O[Bornology.cobounded ℂ ⊓ Filter.principal {z | 0 < z.re}] fun z => (B * Complex.abs z ^ c).exp) →
(Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) Filter.atTop fun x => ‖f ↑x‖) →
(∀ (x : ℝ), ‖f (↑x * Complex.I)‖ ≤ C) → 0 ≤ z.re → ‖f z‖ ≤ C
**Phragmén-Lindelöf Principle in the Right Half-Plane**. Given a function `f : ℂ → E`, where `E` is a normed additive commutative group and also a normed space over the complex numbers, that is differentiable in the open right half-plane and continuous on its closure, the theorem states that if the norm of `f(z)`, ‖f z‖, satisfies the following conditions:
* It is bounded from above by `A * exp(B * (abs z) ^ c)` on the open right half-plane, where `c` is a real number less than `2`.
* It is bounded from above by a constant `C` on the imaginary axis.
* It is bounded from above by a constant for large real values of `x`.
Then, the norm ‖f z‖ is bounded from above by `C` on the closed right half-plane, given that the real part of `z` is non-negative.
More concisely: If a complex-valued differentiable function `f` on the open right half-plane of the complex plane, with norm continuous on its closure, satisfies the given bounds on the norm, then the norm of `f` is bounded on the closed right half-plane.
|
PhragmenLindelof.quadrant_II
theorem PhragmenLindelof.quadrant_II :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {C : ℝ} {f : ℂ → E} {z : ℂ},
DiffContOnCl ℂ f (Set.Iio 0 ×ℂ Set.Ioi 0) →
(∃ c < 2,
∃ B,
f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Iio 0 ×ℂ Set.Ioi 0)] fun z =>
(B * Complex.abs z ^ c).exp) →
(∀ x ≤ 0, ‖f ↑x‖ ≤ C) → (∀ (x : ℝ), 0 ≤ x → ‖f (↑x * Complex.I)‖ ≤ C) → z.re ≤ 0 → 0 ≤ z.im → ‖f z‖ ≤ C
**Phragmén–Lindelöf Principle** in the second quadrant.
Consider a complex function `f` satisfying the following conditions:
- It is differentiable in the open second quadrant and is continuous on its closure.
- The norm of `f(z)`, denoted `‖f z‖`, is bounded from above by `A * exp(B * (abs z) ^ c)` on the open second quadrant for some `c < 2`.
- The norm of `f(z)` is bounded from above by a constant `C` on the boundary of the second quadrant.
Then the theorem states that if these conditions hold, the norm of `f(z)` is also bounded from above by the same constant `C` on the closed second quadrant. Here, the second quadrant refers to the set of complex numbers `z` with negative real part and positive imaginary part.
The theorem is formalized with several Lean definitions, including intervals (`Set.Iio` and `Set.Ioi`), filters (`Bornology.cobounded` and `Filter.principal`), the complex absolute value (`Complex.abs`), and the imaginary unit (`Complex.I`). This theorem is a crucial result in complex analysis, particularly in the study of boundedness of analytic functions.
More concisely: If a complex function is differentiable in the open second quadrant, continuous on its closure, and its norm is bounded above by `A * exp(B * (abs z) ^ c)` on the open second quadrant and by a constant `C` on its boundary, then its norm is bounded above by `C` on the closed second quadrant.
|
PhragmenLindelof.eq_zero_on_quadrant_II
theorem PhragmenLindelof.eq_zero_on_quadrant_II :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E},
DiffContOnCl ℂ f (Set.Iio 0 ×ℂ Set.Ioi 0) →
(∃ c < 2,
∃ B,
f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Iio 0 ×ℂ Set.Ioi 0)] fun z =>
(B * Complex.abs z ^ c).exp) →
(∀ x ≤ 0, f ↑x = 0) → (∀ (x : ℝ), 0 ≤ x → f (↑x * Complex.I) = 0) → Set.EqOn f 0 {z | z.re ≤ 0 ∧ 0 ≤ z.im}
This theorem is known as the **Phragmen-Lindelöf principle** in the second quadrant. It states that if we have a function `f : ℂ → E`, where `E` is a normed additive commutative group and also a normed space over complex numbers, with the following properties:
* `f` is differentiable in the open second quadrant and is continuous on its closure,
* the norm of `f` at any point `z` in the open second quadrant is bounded from above by `A * exp(B * (abs z) ^ c)` for some `A`, `B`, and `c < 2`,
* `f` equals zero on the boundary of the second quadrant.
Then, `f` must be equal to zero everywhere on the closed second quadrant. Here, the second quadrant refers to the set of complex numbers where the real part is less than or equal to zero and the imaginary part is greater than or equal to zero.
More concisely: If a differentiable function `f : ℂ → E` with values in a normed additive commutative group and normed space over the complex numbers, is bounded and equals zero on the boundary of the second quadrant, then it is identically zero on the closed second quadrant.
|
PhragmenLindelof.eq_zero_on_horizontal_strip
theorem PhragmenLindelof.eq_zero_on_horizontal_strip :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b : ℝ} {f : ℂ → E},
DiffContOnCl ℂ f (Complex.im ⁻¹' Set.Ioo a b) →
(∃ c < Real.pi / (b - a),
∃ B,
f =O[Filter.comap (abs ∘ Complex.re) Filter.atTop ⊓ Filter.principal (Complex.im ⁻¹' Set.Ioo a b)]
fun z => (B * (c * |z.re|).exp).exp) →
(∀ (z : ℂ), z.im = a → f z = 0) →
(∀ (z : ℂ), z.im = b → f z = 0) → Set.EqOn f 0 (Complex.im ⁻¹' Set.Icc a b)
This is the Phragmén-Lindelöf Principle for a strip \( U = \{z \in \mathbb{C} \,|\, a < \text{Im} \, z < b\}\). Given a function \(f : \mathbb{C} \rightarrow E\) where \(E\) is a normed additive commutative group with a normed space over the complex numbers, assuming the following conditions:
1. \(f\) is differentiable on \(U\) and continuous on its closure.
2. The norm of \(f(z)\) is bounded from above by \(A \cdot \exp(B \cdot \exp(c \cdot |\text{Re} \, z|))\) on \(U\) for some \(c < \pi / (b - a)\).
3. \(f(z) = 0\) on the boundary of \(U\).
Then, \(f\) is identically zero on the closed strip \(\{z \in \mathbb{C} \,|\, a \leq \text{Im} \, z \leq b\}\).
More concisely: If a function \(f : \mathbb{C} \rightarrow E\) is differentiable on a strip \(U = \{z \in \mathbb{C} \,|\, a < \text{Im} \, z < b\}\), continuous on its closure, and satisfies \(f(z) = 0\) on the boundary and \(|f(z)| \leq A \cdot \exp(B \cdot \exp(c \cdot |\text{Re} \, z|))\) on \(U\) for some \(c < \pi / (b - a)\), then \(f\) is the zero function on the closed strip \(a \leq \text{Im} \, z \leq b\).
|
PhragmenLindelof.quadrant_III
theorem PhragmenLindelof.quadrant_III :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {C : ℝ} {f : ℂ → E} {z : ℂ},
DiffContOnCl ℂ f (Set.Iio 0 ×ℂ Set.Iio 0) →
(∃ c < 2,
∃ B,
f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Iio 0 ×ℂ Set.Iio 0)] fun z =>
(B * Complex.abs z ^ c).exp) →
(∀ x ≤ 0, ‖f ↑x‖ ≤ C) → (∀ x ≤ 0, ‖f (↑x * Complex.I)‖ ≤ C) → z.re ≤ 0 → z.im ≤ 0 → ‖f z‖ ≤ C
This is the Phragmen-Lindelöf principle in the third quadrant. The theorem states that if we have a function `f : ℂ → E`, satisfying three conditions, then the norm of `f z` is bounded from above by a given constant in the closed third quadrant. The conditions are as follows:
1. The function `f` is differentiable in the open third quadrant and continuous on its closure.
2. The norm of `f z` is bounded from above by `A * exp (B * (abs z) ^ c)` on the open third quadrant for some `c < 2`.
3. The norm of `f z` is bounded from above by a constant `C` on the boundary of the third quadrant.
In formal terms, the limit of the function `f` is dominated by an exponential function in the filter of cobounded sets in the Bornology of complex numbers intersected with the principal filter of the left-infinite right-open real interval, on the open third quadrant. Additionally, the norm of `f` evaluated at any boundary point of the third quadrant (either on the real or imaginary axis) is less than or equal to `C`. If all these conditions hold, then for any complex number `z` in the closed third quadrant (i.e., `z.re ≤ 0` and `z.im ≤ 0`), the norm of `f z` is also less than or equal to `C`.
More concisely: Given a complex function `f` differentiable in the open third quadrant and continuous on its closure, if the norm of `f` is bounded by an exponential function and a constant on the open and boundary of the third quadrant, respectively, then the norm of `f` is bounded by the constant in the closed third quadrant.
|
PhragmenLindelof.eqOn_quadrant_III
theorem PhragmenLindelof.eqOn_quadrant_III :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E},
DiffContOnCl ℂ f (Set.Iio 0 ×ℂ Set.Iio 0) →
(∃ c < 2,
∃ B,
f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Iio 0 ×ℂ Set.Iio 0)] fun z =>
(B * Complex.abs z ^ c).exp) →
DiffContOnCl ℂ g (Set.Iio 0 ×ℂ Set.Iio 0) →
(∃ c < 2,
∃ B,
g =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Iio 0 ×ℂ Set.Iio 0)] fun z =>
(B * Complex.abs z ^ c).exp) →
(∀ x ≤ 0, f ↑x = g ↑x) →
(∀ x ≤ 0, f (↑x * Complex.I) = g (↑x * Complex.I)) → Set.EqOn f g {z | z.re ≤ 0 ∧ z.im ≤ 0}
This is the **Phragmen-Lindelöf principle** applied to the third quadrant of the complex plane. It states that if we have two functions `f` and `g` from complex numbers to some normed additive commutative group `E` that are differentiable within the open third quadrant and continuous on its closure, and if the norms of `f(z)` and `g(z)` are both bounded above by `A * exp(B * (abs z) ^ c)` for some `A`, `B`, and `c < 2` within this quadrant, and if `f` equals `g` on the boundary of this quadrant, then `f` equals `g` throughout the closed third quadrant. The third quadrant is defined as the set of complex numbers where both the real and imaginary parts are less than or equal to zero. The boundary of the third quadrant is the x-axis and y-axis in the negative direction.
More concisely: If two differentiable functions from the complex third quadrant to a normed additive commutative group, with continuous extensions to its closure and bounded by `A * exp(B * |z|^c)`, agree on the boundary, then they are equal throughout the closed third quadrant.
|
PhragmenLindelof.eq_zero_on_quadrant_IV
theorem PhragmenLindelof.eq_zero_on_quadrant_IV :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E},
DiffContOnCl ℂ f (Set.Ioi 0 ×ℂ Set.Iio 0) →
(∃ c < 2,
∃ B,
f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Ioi 0 ×ℂ Set.Iio 0)] fun z =>
(B * Complex.abs z ^ c).exp) →
(∀ (x : ℝ), 0 ≤ x → f ↑x = 0) → (∀ x ≤ 0, f (↑x * Complex.I) = 0) → Set.EqOn f 0 {z | 0 ≤ z.re ∧ z.im ≤ 0}
The **Phragmen-Lindelöf principle** in the fourth quadrant states that given a function `f : ℂ → E` which is differentiable in the open fourth quadrant and continuous on its closure, if the norm of `f` at a complex number `z`, denoted `‖f z‖`, is bounded from above by `A * exp(B * (abs z) ^ c)` on the open fourth quadrant for some constants `A`, `B`, and `c < 2`, and the function `f` is zero on the boundary of the fourth quadrant, then the function `f` is zero on the entire closed fourth quadrant. Here, the fourth quadrant refers to the set of complex numbers where the real part is greater than 0 and the imaginary part is less than 0.
More concisely: If a differentiable function $f : \mathbb{C} \rightarrow E$ is continuous on the closed fourth quadrant, has norm bounded by $Ae^{B|z|^c}$ for $z \in \mathbb{C}$ and some constants $A, B, c < 2$, and is zero on the boundary, then $f$ is the zero function on the entire closed fourth quadrant.
|
PhragmenLindelof.eq_zero_on_quadrant_I
theorem PhragmenLindelof.eq_zero_on_quadrant_I :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E},
DiffContOnCl ℂ f (Set.Ioi 0 ×ℂ Set.Ioi 0) →
(∃ c < 2,
∃ B,
f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Ioi 0 ×ℂ Set.Ioi 0)] fun z =>
(B * Complex.abs z ^ c).exp) →
(∀ (x : ℝ), 0 ≤ x → f ↑x = 0) →
(∀ (x : ℝ), 0 ≤ x → f (↑x * Complex.I) = 0) → Set.EqOn f 0 {z | 0 ≤ z.re ∧ 0 ≤ z.im}
The **Phragmen-Lindelöf principle** in the first quadrant states that given a function `f : ℂ → E` satisfying certain conditions, the function equals zero on the closed first quadrant. The conditions are as follows:
1- The function `f` is differentiable in the open first quadrant and is continuous on its closure.
2- The norm of `f(z)`, denoted as `‖f z‖`, is bounded from above by `A * exp(B * (abs z) ^ c)` on the open first quadrant for some constants `A`, `B`, and `c < 2`.
3- The function `f` equals zero on the boundary of the first quadrant.
If these three conditions are met, then `f` equals zero on the closed first quadrant.
More concisely: If a complex-valued function `f` is differentiable in the open first quadrant, continuous on its closure, and satisfies a bounded growth condition on the open first quadrant with constants `A`, `B`, and `c < 2`, while also equals zero on the boundary of the first quadrant, then `f` equals zero on the closed first quadrant.
|
PhragmenLindelof.quadrant_IV
theorem PhragmenLindelof.quadrant_IV :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {C : ℝ} {f : ℂ → E} {z : ℂ},
DiffContOnCl ℂ f (Set.Ioi 0 ×ℂ Set.Iio 0) →
(∃ c < 2,
∃ B,
f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Ioi 0 ×ℂ Set.Iio 0)] fun z =>
(B * Complex.abs z ^ c).exp) →
(∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C) → (∀ x ≤ 0, ‖f (↑x * Complex.I)‖ ≤ C) → 0 ≤ z.re → z.im ≤ 0 → ‖f z‖ ≤ C
This is the Phragmén-Lindelöf principle specific to the fourth quadrant. The theorem states that given a function `f : ℂ → E`, where `E` is a normed additive commutative group and is also a complex normed space, if the following conditions are met:
* `f` is differentiable in the open fourth quadrant and is continuous on its closure
* The norm of `f` at point `z`, `‖f z‖`, is bounded from above by `A * exp(B * (abs z) ^ c)` on the open fourth quadrant for some `c < 2`
* The norm of `f` at point `z`, `‖f z‖`, is bounded from above by a constant `C` on the boundary of the fourth quadrant
then the norm of `f` at point `z`, `‖f z‖`, is bounded from above by the same constant `C` on the closed fourth quadrant. This theorem gives a bound for the norm of a function on the closed fourth quadrant given its behavior on the open quadrant and the boundary.
More concisely: If a differentiable and continuous complex-valued function `f` on the closed fourth quadrant satisfies a specific growth condition on its open subset and on the boundary, then `f` is bounded on the closed fourth quadrant.
|
PhragmenLindelof.isBigO_sub_exp_rpow
theorem PhragmenLindelof.isBigO_sub_exp_rpow :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] {a : ℝ} {f g : ℂ → E} {l : Filter ℂ},
(∃ c < a, ∃ B, f =O[Bornology.cobounded ℂ ⊓ l] fun z => (B * Complex.abs z ^ c).exp) →
(∃ c < a, ∃ B, g =O[Bornology.cobounded ℂ ⊓ l] fun z => (B * Complex.abs z ^ c).exp) →
∃ c < a, ∃ B, (f - g) =O[Bornology.cobounded ℂ ⊓ l] fun z => (B * Complex.abs z ^ c).exp
The theorem `PhragmenLindelof.isBigO_sub_exp_rpow` is an auxiliary lemma in the context of complex analysis and big O notation regarding estimation of exponential functions of powers. It states that given two functions `f` and `g` that map from Complex numbers to a Normed Additive Commutative Group `E`, and a filter `l` on Complex numbers, if there exists a real number `B` and an exponent `c` less than a given real number `a` such that both `f` and `g` are bounded by the function `z => Real.exp (B * Complex.abs z ^ c)` under the filter obtained by intersecting the cobounded filter of the bornology of Complex numbers with `l`, then there also exists a such a real number `B` and an exponent `c` less than `a` for the difference of the functions `f` and `g`.
More concisely: If functions `f` and `g` are bounded by `Real.exp(B * |z|^c)` under filter `l` for some `B` and `c` (with `c < a`), then `f - g` is also bounded by `Real.exp(B' * |z|^{c'})` for some `B'` and `c'` (with `c' < a`).
|
PhragmenLindelof.eqOn_horizontal_strip
theorem PhragmenLindelof.eqOn_horizontal_strip :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b : ℝ} {f g : ℂ → E},
DiffContOnCl ℂ f (Complex.im ⁻¹' Set.Ioo a b) →
(∃ c < Real.pi / (b - a),
∃ B,
f =O[Filter.comap (abs ∘ Complex.re) Filter.atTop ⊓ Filter.principal (Complex.im ⁻¹' Set.Ioo a b)]
fun z => (B * (c * |z.re|).exp).exp) →
DiffContOnCl ℂ g (Complex.im ⁻¹' Set.Ioo a b) →
(∃ c < Real.pi / (b - a),
∃ B,
g =O[Filter.comap (abs ∘ Complex.re) Filter.atTop ⊓ Filter.principal (Complex.im ⁻¹' Set.Ioo a b)]
fun z => (B * (c * |z.re|).exp).exp) →
(∀ (z : ℂ), z.im = a → f z = g z) →
(∀ (z : ℂ), z.im = b → f z = g z) → Set.EqOn f g (Complex.im ⁻¹' Set.Icc a b)
This is the Phragmen-Lindelöf principle in a horizontal strip `U = {z : ℂ | a < im z < b}`. Given two functions `f` and `g` from the complex numbers to a normed additive commutative group `E` that satisfy certain conditions such as: they are differentiable on `U` and continuous on its closure; their norms are bounded from above by `A * exp(B * exp(c * |re z|))` on `U` for some `c < π / (b - a)`; and they are equal on the boundary of `U`, the theorem states that `f` is equal to `g` on the closed strip `{z : ℂ | a ≤ im z ≤ b}`. In other words, if `f` and `g` agree on the boundary of the strip and satisfy certain growth conditions within the strip, then `f` and `g` must be equal everywhere in the strip.
More concisely: If complex functions $f$ and $g$ are equal on the boundary of a horizontal strip $U$, and their norms are bounded by $Ae^{Be^{c|re|}}$ on $U$ for some $c<\pi/(b-a)$, then $f=g$ on the closed strip.
|
PhragmenLindelof.eqOn_vertical_strip
theorem PhragmenLindelof.eqOn_vertical_strip :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b : ℝ} {f g : ℂ → E},
DiffContOnCl ℂ f (Complex.re ⁻¹' Set.Ioo a b) →
(∃ c < Real.pi / (b - a),
∃ B,
f =O[Filter.comap (abs ∘ Complex.im) Filter.atTop ⊓ Filter.principal (Complex.re ⁻¹' Set.Ioo a b)]
fun z => (B * (c * |z.im|).exp).exp) →
DiffContOnCl ℂ g (Complex.re ⁻¹' Set.Ioo a b) →
(∃ c < Real.pi / (b - a),
∃ B,
g =O[Filter.comap (abs ∘ Complex.im) Filter.atTop ⊓ Filter.principal (Complex.re ⁻¹' Set.Ioo a b)]
fun z => (B * (c * |z.im|).exp).exp) →
(∀ (z : ℂ), z.re = a → f z = g z) →
(∀ (z : ℂ), z.re = b → f z = g z) → Set.EqOn f g (Complex.re ⁻¹' Set.Icc a b)
This is the Phragmén-Lindelöf Principle, specifically for a vertical strip `U` in the complex plane, defined by `{z : ℂ | a < Re(z) < b}` where `a` and `b` are real numbers. Suppose we have two functions `f` and `g` from the complex numbers to a normed space `E`. If `f` and `g` are differentiable on `U` and continuous on its closure, and their norms are bounded from above by `A * exp(B * exp(c * |Im(z)|))` on `U` for some `c < π / (b - a)`, and if `f` and `g` are equal on the boundary of `U`, then `f` and `g` are equal on the closed strip `{z : ℂ | a ≤ Re(z) ≤ b}`. Essentially, if two complex-valued functions agree on the boundary of a region and their growth is sufficiently controlled, then they agree in the entire region.
More concisely: If complex-valued functions `f` and `g` are differentiable on a vertical strip `U`, continuous on its closure, equal on its boundary, and their norms are bounded by a function of `|Im(z)|` on `U`, then `f` and `g` are equal on the closed strip `U`.
|
PhragmenLindelof.eqOn_right_half_plane_of_superexponential_decay
theorem PhragmenLindelof.eqOn_right_half_plane_of_superexponential_decay :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E},
DiffContOnCl ℂ f {z | 0 < z.re} →
DiffContOnCl ℂ g {z | 0 < z.re} →
(∃ c < 2,
∃ B, f =O[Bornology.cobounded ℂ ⊓ Filter.principal {z | 0 < z.re}] fun z => (B * Complex.abs z ^ c).exp) →
(∃ c < 2,
∃ B,
g =O[Bornology.cobounded ℂ ⊓ Filter.principal {z | 0 < z.re}] fun z => (B * Complex.abs z ^ c).exp) →
(Asymptotics.SuperpolynomialDecay Filter.atTop Real.exp fun x => ‖f ↑x - g ↑x‖) →
(∃ C, ∀ (x : ℝ), ‖f (↑x * Complex.I)‖ ≤ C) →
(∃ C, ∀ (x : ℝ), ‖g (↑x * Complex.I)‖ ≤ C) → Set.EqOn f g {z | 0 ≤ z.re}
The **Phragmen-Lindelöf principle** in the right half-plane is a theorem about two functions, `f` and `g`, from the complex numbers to a normed add-commutative group `E`. Suppose `f` and `g` have the following properties:
* They are differentiable in the open right half-plane and continuous on its closure;
* The norms `‖f z‖` and `‖g z‖` are bounded from above by `A * exp(B * (abs z) ^ c)` on the open right half-plane for some `c` less than 2;
* The norms `‖f z‖` and `‖g z‖` are bounded from above by constants on the imaginary axis;
* The difference `f x - g x`, where `x` is a real number, tends to zero superexponentially fast as `x → ∞`: for any natural number `n`, `exp (n * x) * ‖f x - g x‖` tends to zero as `x → ∞`.
Then the theorem states that `f` is equal to `g` on the closed right half-plane. This means that for all complex numbers `z` with a nonnegative real part, `f(z) = g(z)`.
More concisely: If two functions from the complex numbers to a normed add-commutative group are differentiable in the open right half-plane, continuous on its closure, have bounded norms that grow no faster than an exponential function in the right half-plane with exponent less than 2, and have superexponentially converging differences on the imaginary axis, then they are equal on the closed right half-plane.
|
PhragmenLindelof.eq_zero_on_quadrant_III
theorem PhragmenLindelof.eq_zero_on_quadrant_III :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E},
DiffContOnCl ℂ f (Set.Iio 0 ×ℂ Set.Iio 0) →
(∃ c < 2,
∃ B,
f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Iio 0 ×ℂ Set.Iio 0)] fun z =>
(B * Complex.abs z ^ c).exp) →
(∀ x ≤ 0, f ↑x = 0) → (∀ x ≤ 0, f (↑x * Complex.I) = 0) → Set.EqOn f 0 {z | z.re ≤ 0 ∧ z.im ≤ 0}
**Phragmén-Lindelöf Principle in the third quadrant**: This theorem states that given a function `f` mapping from the complex numbers to a normed additive commutative group `E`, if the function satisfies the following conditions:
1. It is differentiable in the open third quadrant and continuous on its closure,
2. The norm of `f(z)`, `‖f z‖`, is bounded from above by `A * exp(B * (abs z) ^ c)` in the open third quadrant, for some constants `A`, `B`, and `c < 2`,
3. `f` equals zero on the boundary of the third quadrant,
then the function `f` also equals zero on the entire closed third quadrant. Here, the third quadrant is defined as the set of complex numbers where both the real and the imaginary parts are less than or equal to zero. The principle is a key result in complex analysis providing a measure of control over entire functions based on their growth rates.
More concisely: If a differentiable function `f` mapping from the complex numbers to a normed additive commutative group with continuous closure, bounded growth rate `A * exp(B * (abs z) ^ c)` in the open third quadrant, and `f` equals zero on the third quadrant boundary, then `f` equals zero on the entire closed third quadrant.
|
PhragmenLindelof.eqOn_quadrant_II
theorem PhragmenLindelof.eqOn_quadrant_II :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E},
DiffContOnCl ℂ f (Set.Iio 0 ×ℂ Set.Ioi 0) →
(∃ c < 2,
∃ B,
f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Iio 0 ×ℂ Set.Ioi 0)] fun z =>
(B * Complex.abs z ^ c).exp) →
DiffContOnCl ℂ g (Set.Iio 0 ×ℂ Set.Ioi 0) →
(∃ c < 2,
∃ B,
g =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Iio 0 ×ℂ Set.Ioi 0)] fun z =>
(B * Complex.abs z ^ c).exp) →
(∀ x ≤ 0, f ↑x = g ↑x) →
(∀ (x : ℝ), 0 ≤ x → f (↑x * Complex.I) = g (↑x * Complex.I)) → Set.EqOn f g {z | z.re ≤ 0 ∧ 0 ≤ z.im}
This is the Phragmen-Lindelöf principle in the second quadrant. The theorem states that if we have two complex functions `f` and `g` that satisfy the following conditions:
- `f` and `g` are both differentiable in the open second quadrant and continuous on its closure.
- The norms of `f(z)` and `g(z)` are bounded from above by `A * exp(B * (abs z) ^ c)` on the open second quadrant for some real numbers `A`, `B`, and `c`, where `c` is less than `2`.
- `f` is equal to `g` on the boundary of the second quadrant.
Then, the theorem asserts that `f` is equal to `g` on the closed second quadrant.
In the context of this theorem, the second quadrant is defined as the set of complex numbers where the real part is less than or equal to `0` and the imaginary part is greater than or equal to `0`. The boundary of the second quadrant is defined as the union of the negative real axis and the positive imaginary axis.
More concisely: If complex functions `f` and `g` are differentiable in the open second quadrant, continuous on its closure, and satisfy `f = g` on the boundary with the norms of `f` and `g` bounded by `A * exp(B * |z|^c)`, then `f = g` on the closed second quadrant.
|
PhragmenLindelof.vertical_strip
theorem PhragmenLindelof.vertical_strip :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b C : ℝ} {f : ℂ → E} {z : ℂ},
DiffContOnCl ℂ f (Complex.re ⁻¹' Set.Ioo a b) →
(∃ c < Real.pi / (b - a),
∃ B,
f =O[Filter.comap (abs ∘ Complex.im) Filter.atTop ⊓ Filter.principal (Complex.re ⁻¹' Set.Ioo a b)]
fun z => (B * (c * |z.im|).exp).exp) →
(∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C) → (∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C) → a ≤ z.re → z.re ≤ b → ‖f z‖ ≤ C
This is the **Phragmen-Lindelöf principle** in a vertical strip `U = {z : ℂ | a < Re(z) < b}`. Let's say we have a function `f : ℂ → E` that meets the following conditions:
1. `f` is differentiable on `U` and continuous on its closure (i.e., including the boundary points),
2. the norm of `f(z)` is bounded from above by `A * exp(B * exp(c * |Im(z)|))` on `U` for some `c` that is less than `π / (b - a)`, and
3. the norm of `f(z)` is bounded from above by a constant `C` on the boundary of `U`.
Then, the theorem states that the norm of `f(z)` is bounded by the same constant `C` on the closed strip `{z : ℂ | a ≤ Re(z) ≤ b}`. Furthermore, it's enough to check the second condition only for sufficiently large values of `|Im(z)|`.
In plain terms, if a complex function behaves nicely within a vertical strip and its boundary, it will also behave nicely when we include the boundary points.
More concisely: Given a complex function `f` differentiable on a vertical strip `U` with continuous boundary values, bounded by `C` on the boundary, and satisfying the condition that `||f(z)|| ≤ A * exp(B * exp(c * |Im(z)|))` for `c < π / (b - a)` and large enough `|Im(z)|`, then `||f(z)|| ≤ C` holds for all `z` in the closed strip `{z : ℂ | a ≤ Re(z) ≤ b}`.
|
PhragmenLindelof.right_half_plane_of_tendsto_zero_on_real
theorem PhragmenLindelof.right_half_plane_of_tendsto_zero_on_real :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {C : ℝ} {f : ℂ → E} {z : ℂ},
DiffContOnCl ℂ f {z | 0 < z.re} →
(∃ c < 2,
∃ B, f =O[Bornology.cobounded ℂ ⊓ Filter.principal {z | 0 < z.re}] fun z => (B * Complex.abs z ^ c).exp) →
Filter.Tendsto (fun x => f ↑x) Filter.atTop (nhds 0) →
(∀ (x : ℝ), ‖f (↑x * Complex.I)‖ ≤ C) → 0 ≤ z.re → ‖f z‖ ≤ C
The Phragmen-Lindelöf principle in the right half-plane is a theorem about complex functions. The theorem states that if we have a function `f` from the complex numbers to a normed space `E` that satisfies the following conditions:
* `f` is differentiable in the open right half-plane and continuous on its closure.
* The norm of `f(z)` is bounded from above by `A * exp(B * (abs z) ^ c)` on the open right-half plane, where `c` is less than 2.
* The norm of `f(z)` is bounded from above by a constant `C` on the imaginary axis.
* The value of `f(x)` approaches 0 as `x`, a real number, tends to infinity.
Then, the norm of `f(z)` is bounded from above by the same constant `C` on the closed right half-plane. It is a stronger version of this principle where `f(z)` is bounded on the real axis instead of tending to zero at infinity.
More concisely: If a complex function `f` is differentiable in the open right half-plane, continuous on its closure, and satisfies the condition that its norm is bounded above by `A * exp(B * (abs z) ^ c)` in the open right half-plane with `c < 2`, and is bounded above by a constant `C` on the imaginary axis, then its norm is also bounded above by `C` in the closed right half-plane.
|
PhragmenLindelof.isBigO_sub_exp_exp
theorem PhragmenLindelof.isBigO_sub_exp_exp :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] {a : ℝ} {f g : ℂ → E} {l : Filter ℂ} {u : ℂ → ℝ},
(∃ c < a, ∃ B, f =O[l] fun z => (B * (c * |u z|).exp).exp) →
(∃ c < a, ∃ B, g =O[l] fun z => (B * (c * |u z|).exp).exp) →
∃ c < a, ∃ B, (f - g) =O[l] fun z => (B * (c * |u z|).exp).exp
The theorem `PhragmenLindelof.isBigO_sub_exp_exp` states that for any normed additive commutative group `E`, real number `a`, complex functions `f` and `g`, filter `l` on complex numbers, and function `u` from complex numbers to real numbers, if `f` and `g` both have exponential growth rates bounded by a constant times the exponential of `c` times the absolute value of `u(z)` (where `c` is less than `a`), then the difference between `f` and `g` also has a similar exponential growth rate. In other words, if both `f` and `g` grow no faster than a double exponential function, their difference also grows no faster than a similar double exponential function.
More concisely: If functions `f` and `g` have exponential growth rates bounded by a constant times the exponential of `c` times the absolute value of `u(z)` for some constant `c` less than `a`, then the growth rate of `|f(z) - g(z)|` is also bounded by a constant times the exponential of `c` times the absolute value of `u(z)`.
|
PhragmenLindelof.quadrant_I
theorem PhragmenLindelof.quadrant_I :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {C : ℝ} {f : ℂ → E} {z : ℂ},
DiffContOnCl ℂ f (Set.Ioi 0 ×ℂ Set.Ioi 0) →
(∃ c < 2,
∃ B,
f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Ioi 0 ×ℂ Set.Ioi 0)] fun z =>
(B * Complex.abs z ^ c).exp) →
(∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C) →
(∀ (x : ℝ), 0 ≤ x → ‖f (↑x * Complex.I)‖ ≤ C) → 0 ≤ z.re → 0 ≤ z.im → ‖f z‖ ≤ C
The **Phragmén-Lindelöf principle** in the first quadrant states the following: Suppose we have a function `f : ℂ → E`, where `E` is a normed additive commutative group over the complex numbers. Assume that `f` is differentiable in the open first quadrant and is continuous on its closure; the norm of `f(z)`, `‖f z‖`, is bounded from above by `A * exp(B * (abs z) ^ c)` on the open first quadrant for some `c < 2`; and `‖f z‖` is bounded from above by a constant `C` on the boundary of the first quadrant. Then, the theorem asserts that `‖f z‖` is bounded from above by the same constant `C` on the closed first quadrant.
More concisely: Given a differentiable and continuous function `f : ℂ → E` with bounded growth in the first quadrant of the complex plane, the norm `‖f z‖` is also bounded on the closed first quadrant.
|
PhragmenLindelof.eqOn_quadrant_I
theorem PhragmenLindelof.eqOn_quadrant_I :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E},
DiffContOnCl ℂ f (Set.Ioi 0 ×ℂ Set.Ioi 0) →
(∃ c < 2,
∃ B,
f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Ioi 0 ×ℂ Set.Ioi 0)] fun z =>
(B * Complex.abs z ^ c).exp) →
DiffContOnCl ℂ g (Set.Ioi 0 ×ℂ Set.Ioi 0) →
(∃ c < 2,
∃ B,
g =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Ioi 0 ×ℂ Set.Ioi 0)] fun z =>
(B * Complex.abs z ^ c).exp) →
(∀ (x : ℝ), 0 ≤ x → f ↑x = g ↑x) →
(∀ (x : ℝ), 0 ≤ x → f (↑x * Complex.I) = g (↑x * Complex.I)) → Set.EqOn f g {z | 0 ≤ z.re ∧ 0 ≤ z.im}
This is the **Phragmen-Lindelöf principle** specifically for the first quadrant. The theorem states that if we have two functions `f` and `g` from the complex numbers to a normed additive commutative group `E`, and if these functions are continuously differentiable in the open first quadrant and continuous on its closure, and both their norms are bounded above by `A * exp(B * (abs z) ^ c)` on the open first quadrant for some real numbers `A`, `B`, and `c` where `c < 2`, and if `f` and `g` are equal on the boundary of the first quadrant, then `f` is equal to `g` on the entire closed first quadrant.
In more detail, the theorem doesn't explicitly mention `A`, but expects `f` and `g` to be `O` of the function `(B * Complex.abs z ^ c).exp` in the filter generated by the intersection of the cobounded sets in the bornology of complex numbers and the principal filter of the set of pairs `(x, y)` in the open first quadrant. The theorem also requires that `f` and `g` be equal along the real axis and the imaginary axis within the first quadrant.
More concisely: If two continuously differentiable functions from the complex numbers to a normed additive commutative group, with bounded norms in the first quadrant by a function of the form `A * exp(B * abs z ^ c)` for `c < 2`, and equal on the first quadrant's boundary and axes, are equal in the first quadrant's filter topology, then they are equal throughout the closed first quadrant.
|
PhragmenLindelof.eqOn_quadrant_IV
theorem PhragmenLindelof.eqOn_quadrant_IV :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E},
DiffContOnCl ℂ f (Set.Ioi 0 ×ℂ Set.Iio 0) →
(∃ c < 2,
∃ B,
f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Ioi 0 ×ℂ Set.Iio 0)] fun z =>
(B * Complex.abs z ^ c).exp) →
DiffContOnCl ℂ g (Set.Ioi 0 ×ℂ Set.Iio 0) →
(∃ c < 2,
∃ B,
g =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Ioi 0 ×ℂ Set.Iio 0)] fun z =>
(B * Complex.abs z ^ c).exp) →
(∀ (x : ℝ), 0 ≤ x → f ↑x = g ↑x) →
(∀ x ≤ 0, f (↑x * Complex.I) = g (↑x * Complex.I)) → Set.EqOn f g {z | 0 ≤ z.re ∧ z.im ≤ 0}
This is the Phragmén-Lindelöf principle in the fourth quadrant for complex analysis. Given two functions `f` and `g` from the complex numbers to a normed add-commutative group `E`, the theorem states that if `f` and `g` are differentiable in the open fourth quadrant and continuous on its closure, and if the norms of `f(z)` and `g(z)` are both bounded from above by `A * exp(B * (abs z) ^ c)` on the open fourth quadrant for some constants `A`, `B`, and `c` less than 2, and if `f` and `g` are equal on the boundary of the fourth quadrant, then `f` is equal to `g` on the closed fourth quadrant. Here, the fourth quadrant is defined as the set of complex numbers where the real part is positive and the imaginary part is negative.
More concisely: If two complex functions are differentiable in the open fourth quadrant, continuous on its closure, and satisfy certain norm bounds and equality on the boundary, then they are equal throughout the closed fourth quadrant.
|
PhragmenLindelof.horizontal_strip
theorem PhragmenLindelof.horizontal_strip :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b C : ℝ} {f : ℂ → E} {z : ℂ},
DiffContOnCl ℂ f (Complex.im ⁻¹' Set.Ioo a b) →
(∃ c < Real.pi / (b - a),
∃ B,
f =O[Filter.comap (abs ∘ Complex.re) Filter.atTop ⊓ Filter.principal (Complex.im ⁻¹' Set.Ioo a b)]
fun z => (B * (c * |z.re|).exp).exp) →
(∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) → (∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) → a ≤ z.im → z.im ≤ b → ‖f z‖ ≤ C
This is a statement of the Phragmen-Lindelof Principle in the context of a strip in the complex plane. Suppose we have a strip `U`, defined as a set of complex numbers where the imaginary part lies strictly between two real numbers `a` and `b`. Now, let there be a function `f` from the complex numbers to a normed add commutative group `E`, which is differentiable on `U` and continuous on its closure. If the norm of `f(z)` is upper bounded by `A * exp(B * exp(c * |re z|))` on `U` for some real number `c` less than `π / (b - a)`, and the norm of `f(z)` is upper bounded by a constant `C` on the boundary of `U`, then the norm of `f(z)` is bounded by the same constant `C` throughout the closed strip `{z : ℂ | a ≤ im z ≤ b}`. Furthermore, it is sufficient to verify the second assumption only for large enough values of the absolute value of the real part of `z`.
More concisely: Given a differentiable and continuous function `f` from a complex strip `U` to a normed additive commutative group `E`, if the norm of `f` is bounded on `U` by `A * exp(B * exp(c * |z|))` for `c < π / (b-a)` and on the boundary by a constant `C`, then `f` is bounded by `C` throughout the closed strip. The verification of the boundary condition for large enough real parts of `z` is sufficient.
|
PhragmenLindelof.eq_zero_on_vertical_strip
theorem PhragmenLindelof.eq_zero_on_vertical_strip :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b : ℝ} {f : ℂ → E},
DiffContOnCl ℂ f (Complex.re ⁻¹' Set.Ioo a b) →
(∃ c < Real.pi / (b - a),
∃ B,
f =O[Filter.comap (abs ∘ Complex.im) Filter.atTop ⊓ Filter.principal (Complex.re ⁻¹' Set.Ioo a b)]
fun z => (B * (c * |z.im|).exp).exp) →
(∀ (z : ℂ), z.re = a → f z = 0) →
(∀ (z : ℂ), z.re = b → f z = 0) → Set.EqOn f 0 (Complex.re ⁻¹' Set.Icc a b)
This is the statement of the Phragmen-Lindelöf Principle in the context of a strip `U = {z ∈ ℂ | a < Re(z) < b}` in the complex plane. Suppose `f : ℂ → E` is a function that is differentiable on `U` and continuous on its closure, and the norm `‖f z‖` is bounded from above by `A * exp(B * exp(c * |Im(z)|))` on `U` for some `c < π / (b - a)`, and `f(z) = 0` on the boundary of `U`. Then the theorem states that `f` is identically zero on the closed strip `{z ∈ ℂ | a ≤ Re(z) ≤ b}`. In other words, if `f` vanishes on the boundary of `U` and its norm doesn't grow too fast within `U`, then `f` must vanish everywhere in the closed strip.
More concisely: If a complex function `f` is differentiable on an open strip `U`, continuous on its closure, and satisfies `‖f z‖ ≤ A * exp(B * exp(c * |Im(z)|))` on `U` for some `c < π / (b - a)` with `f(z) = 0` on `U`'s boundary, then `f` is the identically zero function on the closed strip `{z ∈ ℂ | a ≤ Re(z) ≤ b}`.
|