MDifferentiableOn.eqOn_of_isPreconnected_of_isMaxOn_norm
theorem MDifferentiableOn.eqOn_of_isPreconnected_of_isMaxOn_norm :
โ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace โ E] {F : Type u_2}
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace โ F] {H : Type u_3} [inst_4 : TopologicalSpace H]
{I : ModelWithCorners โ E H} [inst_5 : I.Boundaryless] {M : Type u_4} [inst_6 : TopologicalSpace M]
[inst_7 : ChartedSpace H M] [inst_8 : SmoothManifoldWithCorners I M] [inst_9 : StrictConvexSpace โ F] {f : M โ F}
{U : Set M} {c : M},
MDifferentiableOn I (modelWithCornersSelf โ F) f U โ
IsPreconnected U โ IsOpen U โ c โ U โ IsMaxOn (norm โ f) U c โ Set.EqOn f (Function.const M (f c)) U
The Maximum Modulus Principle on a Connected Set theorem states that for a preconnected open set `U` in a complex normed space with a function `f : E โ F` that is complex differentiable on `U`, if the norm of `f` attains its maximum value at `c โ U`, then `f` takes the same value at every point in `U`, i.e., `f x = f c` for all `x โ U`.
In technical terms, for each types `E`, `F`, `H`, `M` with the appropriate typeclass instances, and for a given model with corners `I`, a function `f : M โ F`, a set `U : Set M` and a point `c : M`, if `f` is differentiable on `U`, `U` is preconnected and open, and `c` is in `U`, and if the norm of `f` has its maximum on `U` at `c`, then `f` is equal to the constant function with value `f c` on `U`. This implies that `f` takes the same value at every point in the preconnected open set `U`.
More concisely: If a complex differentiable function reaches its maximum norm on a preconnected open set, then it is constant on that set.
|
MDifferentiable.isLocallyConstant
theorem MDifferentiable.isLocallyConstant :
โ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace โ E] {F : Type u_2}
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace โ F] {H : Type u_3} [inst_4 : TopologicalSpace H]
{I : ModelWithCorners โ E H} [inst_5 : I.Boundaryless] {M : Type u_4} [inst_6 : TopologicalSpace M]
[inst_7 : CompactSpace M] [inst_8 : ChartedSpace H M] [inst_9 : SmoothManifoldWithCorners I M] {f : M โ F},
MDifferentiable I (modelWithCornersSelf โ F) f โ IsLocallyConstant f
This theorem states that a holomorphic function on a compact complex manifold is locally constant. More specifically, for any function `f` from a manifold `M` to a normed additive commutative group `F`, where `M` is a compact space equipped with a smooth manifold structure and `F` is a normed space over the complex numbers, if `f` is holomorphically differentiable with respect to the model with corners given by `I` and the identity on `F`, then `f` is locally constant. This means that, for any set `s` in `F`, the preimage of `s` under `f` is an open set in `M`.
More concisely: A holomorphic function on a compact complex manifold is locally constant, i.e., the preimage of any set under a holomorphically differentiable function is an open set.
|
Complex.norm_eventually_eq_of_mdifferentiableAt_of_isLocalMax
theorem Complex.norm_eventually_eq_of_mdifferentiableAt_of_isLocalMax :
โ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace โ E] {F : Type u_2}
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace โ F] {H : Type u_3} [inst_4 : TopologicalSpace H]
{I : ModelWithCorners โ E H} [inst_5 : I.Boundaryless] {M : Type u_4} [inst_6 : TopologicalSpace M]
[inst_7 : ChartedSpace H M] [inst_8 : SmoothManifoldWithCorners I M] {f : M โ F} {c : M},
(โแถ (z : M) in nhds c, MDifferentiableAt I (modelWithCornersSelf โ F) f z) โ
IsLocalMax (norm โ f) c โ โแถ (y : M) in nhds c, โf yโ = โf cโ
The **Maximum modulus principle** states that if a complex function `f`, mapped from manifold `M` to normed additively commutative group `F`, is complex differentiable in a neighborhood around a point `c` and if the norm of `f(z)`, denoted as `โf zโ`, has a local maximum at `c`, then the norm `โf zโ` is constant within that neighborhood of `c`. This theorem is a manifold version of the lemma `Complex.norm_eventually_eq_of_isLocalMax`. Particularly, in Lean 4 terms, if for all points `z` in the neighborhood of `c` (expressed as `nhds c`), `f` is differentiable at `z` (`MDifferentiableAt I (modelWithCornersSelf โ F) f z`), and if there's a local maximum of the function `norm โ f` at `c` (`IsLocalMax (norm โ f) c`), then for all points `y` in the neighborhood of `c`, the norm of `f(y)` is equal to the norm of `f(c)` (`โf yโ = โf cโ`).
More concisely: If a complex differentiable function from a manifold to a normed additively commutative group has a local maximum of its norm at a point, then the norm of the function is constant in a neighborhood of that point.
|
MDifferentiableOn.norm_eqOn_of_isPreconnected_of_isMaxOn
theorem MDifferentiableOn.norm_eqOn_of_isPreconnected_of_isMaxOn :
โ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace โ E] {F : Type u_2}
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace โ F] {H : Type u_3} [inst_4 : TopologicalSpace H]
{I : ModelWithCorners โ E H} [inst_5 : I.Boundaryless] {M : Type u_4} [inst_6 : TopologicalSpace M]
[inst_7 : ChartedSpace H M] [inst_8 : SmoothManifoldWithCorners I M] {f : M โ F} {U : Set M} {c : M},
MDifferentiableOn I (modelWithCornersSelf โ F) f U โ
IsPreconnected U โ IsOpen U โ c โ U โ IsMaxOn (norm โ f) U c โ Set.EqOn (norm โ f) (Function.const M โf cโ) U
The **Maximum Modulus Principle** states that given a preconnected open set `U` in a complex normed space, and a function `f` that is complex differentiable on `U`, if the norm of `f`, denoted as `โf xโ`, takes its maximum value at a point `c` which is an element of `U`, then the norm of `f` is constant on `U`, i.e., `โf xโ` equals `โf cโ` for all `x` within `U`. The theorem is applicable in the context of smooth manifolds with a modeled corners structure, and relies on the assumptions that the input function is complex differentiable, the set `U` is preconnected and open, and `c` is an element of `U` where the norm of the function achieves its maximum.
More concisely: If a complex differentiable function on a preconnected open set in a complex normed space attains its maximum norm at an interior point, then the norm is constant throughout the set.
|
MDifferentiable.apply_eq_of_compactSpace
theorem MDifferentiable.apply_eq_of_compactSpace :
โ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace โ E] {F : Type u_2}
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace โ F] {H : Type u_3} [inst_4 : TopologicalSpace H]
{I : ModelWithCorners โ E H} [inst_5 : I.Boundaryless] {M : Type u_4} [inst_6 : TopologicalSpace M]
[inst_7 : CompactSpace M] [inst_8 : ChartedSpace H M] [inst_9 : SmoothManifoldWithCorners I M]
[inst_10 : PreconnectedSpace M] {f : M โ F},
MDifferentiable I (modelWithCornersSelf โ F) f โ โ (a b : M), f a = f b
This theorem states that if we have a holomorphic function `f` defined on a compact, connected complex manifold `M`, then the function `f` is constant, meaning that for any two points `a` and `b` in `M`, the value of `f` at `a` is the same as the value of `f` at `b`. Here, a holomorphic function is a complex-differentiable function, and a compact, connected complex manifold is a topological space that is compact, connected, and locally similar to the complex plane.
More concisely: If `f` is a holomorphic function on the compact, connected complex manifold `M`, then `f` is constant.
|
MDifferentiableOn.apply_eq_of_isPreconnected_isCompact_isOpen
theorem MDifferentiableOn.apply_eq_of_isPreconnected_isCompact_isOpen :
โ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace โ E] {F : Type u_2}
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace โ F] {H : Type u_3} [inst_4 : TopologicalSpace H]
{I : ModelWithCorners โ E H} [inst_5 : I.Boundaryless] {M : Type u_4} [inst_6 : TopologicalSpace M]
[inst_7 : ChartedSpace H M] [inst_8 : SmoothManifoldWithCorners I M] {f : M โ F} {U : Set M} {a b : M},
MDifferentiableOn I (modelWithCornersSelf โ F) f U โ
IsPreconnected U โ IsCompact U โ IsOpen U โ a โ U โ b โ U โ f a = f b
The theorem states that if a function `f` maps from a complex manifold `M` to a complex normed space `F` and is holomorphic on a set `U` that is preconnected, compact, and open, then the function `f` is constant on this set `U`. This means that for any two points `a` and `b` in the set `U`, the value of the function `f` at `a` is equal to the value of the function `f` at `b`.
More concisely: If `f` is a holomorphic function from a preconnected, compact, and open set `U` in a complex manifold `M` to a complex normed space `F`, then `f` is constant on `U`.
|
MDifferentiable.exists_eq_const_of_compactSpace
theorem MDifferentiable.exists_eq_const_of_compactSpace :
โ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace โ E] {F : Type u_2}
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace โ F] {H : Type u_3} [inst_4 : TopologicalSpace H]
{I : ModelWithCorners โ E H} [inst_5 : I.Boundaryless] {M : Type u_4} [inst_6 : TopologicalSpace M]
[inst_7 : CompactSpace M] [inst_8 : ChartedSpace H M] [inst_9 : SmoothManifoldWithCorners I M]
[inst_10 : PreconnectedSpace M] {f : M โ F},
MDifferentiable I (modelWithCornersSelf โ F) f โ โ v, f = Function.const M v
The theorem `MDifferentiable.exists_eq_const_of_compactSpace` states that for any holomorphic function `f` defined on a compact, connected complex manifold `M`, there exists a complex number `v` such that `f` is the constant function equal to `v` everywhere on `M`. This is a formalization of Liouville's theorem in complex analysis. Here, `M` is a topological space that is compact (meaning every open cover has a finite subcover) and preconnected (meaning it cannot be represented as the union of two disjoint nonempty open subsets). The model with corners `I` provides the necessary context for differentiability in this setting. The function `f` is assumed to be `MDifferentiable`, signaling it is differentiable with respect to the complex numbers.
More concisely: On a compact, connected complex manifold, every holomorphic and `MDifferentiable` function is constant.
|