Complex.eqOn_of_eqOn_frontier
theorem Complex.eqOn_of_eqOn_frontier :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
[inst_3 : NormedSpace ℂ F] [inst_4 : Nontrivial E] {f g : E → F} {U : Set E},
Bornology.IsBounded U → DiffContOnCl ℂ f U → DiffContOnCl ℂ g U → Set.EqOn f g (frontier U) → Set.EqOn f g U
The theorem states that if we have two complex differentiable functions `f` and `g` from a type `E` to a type `F` (where `E` is a nontrivial normed additive commutative group with a complex normed space structure and `F` is a normed additive commutative group with a complex normed space structure), and we have a set `U` of type `E` that is bounded under a bornology, then if `f` and `g` are equal on the boundary (or frontier) of `U`, they must be equal everywhere on `U`. In other words, two complex differentiable functions that are equal on the frontier of a bounded set will be identical on the entire set.
More concisely: If `f` and `g` are complex differentiable functions from a bounded, nontrivial normed additive commutative group `E` to another normed additive commutative group `F`, and `f(x) = g(x)` for all `x` in the boundary of `E`, then `f(x) = g(x)` for all `x` in `E`.
|
Complex.eq_of_isMaxOn_of_ball_subset
theorem Complex.eq_of_isMaxOn_of_ball_subset :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
[inst_3 : NormedSpace ℂ F] [inst_4 : StrictConvexSpace ℝ F] {f : E → F} {s : Set E} {z w : E},
DiffContOnCl ℂ f s → IsMaxOn (norm ∘ f) s z → Metric.ball z (dist w z) ⊆ s → f w = f z
The **Maximum modulus principle** states that if there is a function `f` from a complex normed space `E` to a strictly convex space `F` that is complex differentiable on a set `s` and continuous on the closure of `s`, and the norm of `f` reaches its maximum on `s` at a point `z`, then for any point `w` such that the closed ball centered at `z` with radius equal to the distance from `w` to `z` is entirely within `s`, the function `f` has the same value at `w` and `z`, that is, `f(w) = f(z)`.
More concisely: If a complex differentiable function from a complex normed space to a strictly convex space, which is continuous on the closure of its domain, attains its maximum norm on the domain at a point, then that function is constant on the closed ball centered at that point with radius equal to the distance to the point.
|
Complex.eventually_eq_of_isLocalMax_norm
theorem Complex.eventually_eq_of_isLocalMax_norm :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
[inst_3 : NormedSpace ℂ F] [inst_4 : StrictConvexSpace ℝ F] {f : E → F} {c : E},
(∀ᶠ (z : E) in nhds c, DifferentiableAt ℂ f z) → IsLocalMax (norm ∘ f) c → ∀ᶠ (y : E) in nhds c, f y = f c
This theorem is known as the **Maximum modulus principle**. It states that if we have a complex function `f : E → F` which is differentiable in a neighborhood of a point `c`, and the norm of this function `‖f z‖` attains a local maximum at `c`, then the function `f` is locally constant in a neighborhood of `c`. In other words, for all points `y` sufficiently close to `c`, `f(y)` equals `f(c)`.
More concisely: If a complex differentiable function attains a local maximum at a point, then it is locally constant around that point.
|
Complex.eqOn_closure_of_eqOn_frontier
theorem Complex.eqOn_closure_of_eqOn_frontier :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
[inst_3 : NormedSpace ℂ F] [inst_4 : Nontrivial E] {f g : E → F} {U : Set E},
Bornology.IsBounded U →
DiffContOnCl ℂ f U → DiffContOnCl ℂ g U → Set.EqOn f g (frontier U) → Set.EqOn f g (closure U)
The theorem states that for any type `E` which is a normed addition commutative group and a complex normed space, and any type `F` which is also a normed addition commutative group and a complex normed space, if `f` and `g` are two complex differentiable functions from `E` to `F` and `U` is a bounded set of elements of type `E`, then if `f` and `g` are equal on the frontier (the set of points between the closure and interior) of `U`, they are also equal on the closure of `U`. The closure of a set is the smallest closed set containing the set. This theorem applies under the condition that `f` and `g` are differentiable with continuity on the closure of `U`, and `U` is bounded.
More concisely: If `f` and `g` are complex differentiable functions from a bounded, closed set `U` in two complex normed additive commutative groups `E` and `F`, respectively, with `f` and `g` equal on the frontier of `U` and differentiable with continuity on `U`'s closure, then `f` and `g` are equal on `U`'s closure.
|
Complex.eqOn_closedBall_of_isMaxOn_norm
theorem Complex.eqOn_closedBall_of_isMaxOn_norm :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
[inst_3 : NormedSpace ℂ F] [inst_4 : StrictConvexSpace ℝ F] {f : E → F} {z : E} {r : ℝ},
DiffContOnCl ℂ f (Metric.ball z r) →
IsMaxOn (norm ∘ f) (Metric.ball z r) z → Set.EqOn f (Function.const E (f z)) (Metric.closedBall z r)
The **Maximum modulus principle** on a closed ball states that for a function `f` mapping from a normed complex space to a strictly convex normed complex space, if the function `f` has the following properties:
- `f` is continuous on a closed ball centered at `z` with radius `r`,
- `f` is complex differentiable on the open ball corresponding to the closed ball, and
- the norm of `f(w)`, denoted as `‖f w‖`, attains its maximum value on the open ball at its center `z`.
Then, the function `f` behaves like a constant on the closed ball, that is, for all points `w` in the closed ball, `f(w) = f(z)`.
More concisely: If a continuous, complex differentiable function `f` on a closed ball in a strictly convex normed complex space attains its maximum modulus at the center of the ball, then `f` is constant on the entire closed ball.
|
Complex.norm_eventually_eq_of_isLocalMax
theorem Complex.norm_eventually_eq_of_isLocalMax :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
[inst_3 : NormedSpace ℂ F] {f : E → F} {c : E},
(∀ᶠ (z : E) in nhds c, DifferentiableAt ℂ f z) → IsLocalMax (norm ∘ f) c → ∀ᶠ (y : E) in nhds c, ‖f y‖ = ‖f c‖
The theorem, known as the **Maximum modulus principle**, states that if you have a function `f` mapping from a complex vector space `E` to another complex vector space `F`, and this function is complex differentiable in a neighborhood around a certain point `c`, and furthermore the norm `‖f z‖` of this function reaches a local maximum at this point `c`, then the norm `‖f z‖` must be locally constant in a neighborhood of `c`. In other words, for every point `y` close to `c`, the norm `‖f y‖` equals `‖f c‖`. This is a key result in complex analysis, reflecting the fact that holomorphic functions cannot have local maxima.
More concisely: If a complex differentiable function from a complex vector space to another attains a local maximum at a point, then the norm of the function is constant in a neighborhood of that point.
|
Complex.norm_eq_norm_of_isMaxOn_of_ball_subset
theorem Complex.norm_eq_norm_of_isMaxOn_of_ball_subset :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
[inst_3 : NormedSpace ℂ F] {f : E → F} {s : Set E} {z w : E},
DiffContOnCl ℂ f s → IsMaxOn (norm ∘ f) s z → Metric.ball z (dist w z) ⊆ s → ‖f w‖ = ‖f z‖
This theorem is known as the **Maximum modulus principle**. It states that if we have a complex differentiable function `f` from a normed additive commutative group `E` to another normed additive commutative group `F`, operating on a set `s`, and the norm of `f` reaches its maximum on `s` at a point `z`, then for any point `w` such that the closed ball with center `z` and radius equal to the distance between `w` and `z` is contained within `s`, the norm of `f` at `w` is equal to the norm of `f` at `z`. In other words, the maximum of the norm of a complex differentiable function on a set is attained at the boundary of any closed ball within that set.
More concisely: If a complex differentiable function reaches its norm maximum on a set at a point, then the norm is equal to that maximum value at any point in the closed ball centered at that point and contained within the set.
|
Complex.norm_eqOn_closure_of_isPreconnected_of_isMaxOn
theorem Complex.norm_eqOn_closure_of_isPreconnected_of_isMaxOn :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
[inst_3 : NormedSpace ℂ F] {f : E → F} {U : Set E} {c : E},
IsPreconnected U →
IsOpen U →
DiffContOnCl ℂ f U →
c ∈ U → IsMaxOn (norm ∘ f) U c → Set.EqOn (norm ∘ f) (Function.const E ‖f c‖) (closure U)
This theorem is known as the **Maximum modulus principle** on a connected set. It states that given `U`, a preconnected open set in a complex normed space `E`, and a function `f : E → F` that is complex differentiable on `U` and is continuous on its closure. If the norm of `f`, denoted as `‖f x‖`, attains its maximum value at some point `c` within `U`, then the norm of `f` is equal to `‖f c‖` for all points `x` within the closure of `U`. In other words, the function `f` has a constant norm, equal to its maximum value, throughout the closure of the preconnected set `U`.
More concisely: If `U` is a connected open set in a complex normed space, `f : E → F` is complex differentiable on `U` and continuous on its closure, and `‖f‖` attains its maximum value at some `c` in `U`, then `��||f x��|| = ��||f c��||` for all `x` in the closure of `U`.
|
Complex.norm_eqOn_of_isPreconnected_of_isMaxOn
theorem Complex.norm_eqOn_of_isPreconnected_of_isMaxOn :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
[inst_3 : NormedSpace ℂ F] {f : E → F} {U : Set E} {c : E},
IsPreconnected U →
IsOpen U →
DifferentiableOn ℂ f U → c ∈ U → IsMaxOn (norm ∘ f) U c → Set.EqOn (norm ∘ f) (Function.const E ‖f c‖) U
This theorem is known as the **Maximum Modulus Principle** on a connected set. Suppose we have `U`, a preconnected open set in a complex normed space, and `f` a function from `E` to `F` that is complex differentiable on `U`. If the norm of `f`, denoted as `‖f x‖`, achieves its maximum value at `c ∈ U`, then the theorem asserts that the norm of `f` is constant on `U`, i.e., `‖f x‖ = ‖f c‖` for all `x ∈ U`. This is a fundamental result in the theory of complex functions, and comes from the observation that holomorphic functions cannot have local maxima.
More concisely: If a complex differentiable function achieves its maximum modulus in a connected open set, then it has a constant modulus throughout that set.
|
Complex.eqOn_closure_of_isPreconnected_of_isMaxOn_norm
theorem Complex.eqOn_closure_of_isPreconnected_of_isMaxOn_norm :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
[inst_3 : NormedSpace ℂ F] [inst_4 : StrictConvexSpace ℝ F] {f : E → F} {U : Set E} {c : E},
IsPreconnected U →
IsOpen U →
DiffContOnCl ℂ f U → c ∈ U → IsMaxOn (norm ∘ f) U c → Set.EqOn f (Function.const E (f c)) (closure U)
The Maximum modulus principle on a connected set is a theorem about a function in a complex normed space. Specifically, if we consider an open and preconnected set `U` in this space and a function `f` that is complex differentiable on `U` and continuous on its closure. If the norm of `f`, denoted `‖f x‖`, attains its maximum value at a point `c` within `U`, then we can conclude that `f` is constant on the closure of `U`, i.e., `f x = f c` for all `x` in the closure of `U`.
More concisely: If a complex differentiable function on an open and connected set in a complex normed space attains its maximum modulus inside the set, then the function is constant on the set's closure.
|
Complex.eqOn_of_isPreconnected_of_isMaxOn_norm
theorem Complex.eqOn_of_isPreconnected_of_isMaxOn_norm :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
[inst_3 : NormedSpace ℂ F] [inst_4 : StrictConvexSpace ℝ F] {f : E → F} {U : Set E} {c : E},
IsPreconnected U →
IsOpen U → DifferentiableOn ℂ f U → c ∈ U → IsMaxOn (norm ∘ f) U c → Set.EqOn f (Function.const E (f c)) U
This theorem, known as the **Maximum modulus principle**, states that if `U` is a preconnected open set in a complex normed space, and `f : E → F` is a complex differentiable function on `U`, such that the norm of `f(x)`, denoted as `‖f x‖`, achieves its maximum value at a point `c` that belongs to `U`, then `f(x)` equals `f(c)` for every `x` in `U`. The theorem also indicates a possible desire to change the `IsMaxOn` assumption to `IsLocalMax` in future versions. It's worth noting that the theorem applies to a strict convex space `F` over the real numbers.
More concisely: If `U` is a preconnected open set in a complex normed space, `f : E → F` is complex differentiable on `U`, and the maximum norm of `f` in `U` is achieved at `c` in `U`, then `f(x) = f(c)` for all `x` in `U`, assuming `F` is a strict convex real normed space.
|
Complex.norm_le_of_forall_mem_frontier_norm_le
theorem Complex.norm_le_of_forall_mem_frontier_norm_le :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
[inst_3 : NormedSpace ℂ F] [inst_4 : Nontrivial E] {f : E → F} {U : Set E},
Bornology.IsBounded U →
DiffContOnCl ℂ f U → ∀ {C : ℝ}, (∀ z ∈ frontier U, ‖f z‖ ≤ C) → ∀ {z : E}, z ∈ closure U → ‖f z‖ ≤ C
The theorem states the **Maximum Modulus Principle** in complex analysis. In specific terms, given a function `f` from a nontrivial complex normed vector space `E` to a complex normed vector space `F`, and a bounded set `U` in `E`, if `f` is complex differentiable on the closure of `U`, and the norm of `f(z)` is less than or equal to a real number `C` for any `z` in the frontier of `U`, then the same inequality holds for any `z` in the closure of `U`. This principle essentially says that a holomorphic function attains its maximum on the boundary of a set.
More concisely: If a complex differentiable function on a bounded, closed set in a complex normed vector space attains its maximum value on the boundary, then it attains that maximum value throughout the set.
|
Complex.exists_mem_frontier_isMaxOn_norm
theorem Complex.exists_mem_frontier_isMaxOn_norm :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
[inst_3 : NormedSpace ℂ F] [inst_4 : Nontrivial E] [inst_5 : FiniteDimensional ℂ E] {f : E → F} {U : Set E},
Bornology.IsBounded U → U.Nonempty → DiffContOnCl ℂ f U → ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure U) z
The **Maximum modulus principle** states that for a complex differentiable function `f` from a nonempty and bounded set `U` of a complex finite-dimensional normed additive commutative group `E` to a complex normed additive commutative group `F`, if `f` is continuous on the closure of `U`, then there exists a point `z` on the frontier of `U` such that the norm of `f`, denoted by `‖f ·‖`, achieves its maximum value on the closure of `U` at `z`. The frontier of a set is the set of points between the closure and the interior of the set. The closure of a set is the smallest closed set that contains the set. Being bounded relative to the ambient bornology means that the complement of the set is cobounded.
More concisely: If a complex differentiable function on a nonempty, bounded, and connected subset of a complex normed additive commutative group achieves its maximum norm on the closure of the subset, then there exists a point on the boundary of the subset where the maximum is attained.
|
Complex.norm_eqOn_closedBall_of_isMaxOn
theorem Complex.norm_eqOn_closedBall_of_isMaxOn :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
[inst_3 : NormedSpace ℂ F] {f : E → F} {z : E} {r : ℝ},
DiffContOnCl ℂ f (Metric.ball z r) →
IsMaxOn (norm ∘ f) (Metric.ball z r) z → Set.EqOn (norm ∘ f) (Function.const E ‖f z‖) (Metric.closedBall z r)
The **Maximum modulus principle** for a closed ball states that if we have a function `f` mapping from a normed additive commutative group `E` to another `F`, both with a complex normed space structure, and this function is continuously differentiable on an open ball (centered at `z` with radius `r`), and the norm of `f`, denoted as `‖f w‖`, achieves its maximum value at the center of this open ball, then the norm `‖f w‖` is constant throughout the corresponding closed ball. In other words, for any point `w` in the closed ball, the norm `‖f w‖` equals `‖f z‖`, the norm of `f` evaluated at the center of the ball.
More concisely: If a continuously differentiable function from one complex normed space to another achieves its maximum norm on the closed ball around its center, then the norm is constant throughout the ball.
|