maximum modulus principle

Stream: maths

[Yury G. Kudryashov]

Do we need some assumptions on the codomain of f : ℂ → E to prove the maximum modulus principle? I can easily prove that

• if is_max_on (norm ∘ f) (closed_ball c R) c, R > 0, then norm ∘ f is constant on this disc (+ corollaries);
• if the norm on E is strictly convex, then is_local_max (norm ∘ f) a implies f x = f a near a (+ corollaries).

Is the second statement true without the "strictly convex" assumption?
@Patrick Massot @Sebastien Gouezel @Heather Macbeth :up:

[Yaël Dillies]

Btw Yury I'm defining strictly convex spaces.

[Sebastien Gouezel]

You need some assumption. Let $E = \mathbb{C}^2$ with the sup norm. Let $f(z) = (1, z)$. Then, for $z$ around $0$, the norm of $f(z)$ is constant equal to $1$, and still $f$ is not constant.

[Sebastien Gouezel]

See https://www.ams.org/journals/proc/1967-018-04/S0002-9939-1967-0214794-2/ for instance.

[Yury G. Kudryashov]

For now, I'll formalize the weaker version and add a reference to this paper. Thanks!

[Yury G. Kudryashov]

@Yaël Dillies Do you have some draft? I have (some versions of the) strict Jensen inequality in #11552 and I would prefer to have a typeclass saying "norm is strictly convex".

[Yury G. Kudryashov]

With instances for complex and (less urgent) Lp.

[Yaël Dillies]

We have (something close to) strict convexity of $L_2$ on branch#behrend. We use it in combinatorics!

[Yaël Dillies]

I haven't yet written the definition of strict_convex_space because it is quite trivial from what we already have and I thought I would at least have the modulus of convexity on top to make it worth a PR, but if you need it now I can do it.

[Yury G. Kudryashov]

I just want to take "the norm is strictly convex" as a typeclass argument instead of an explicit one.

[Yaël Dillies]

Ah then wait a few minutes!

[Yury G. Kudryashov]

Thank you!

[Yaël Dillies]

Just to make sure, do we agree that a strictly convex space is a space where the norm is strictly convex? Because I never saw the equivalence with the fact that the unit ball is strictly convex.

[Yaël Dillies]

This really bugs me, because "strictly convex norm" refers to "the balls are strictly convex", not "the norm is a strictly convex function".

[Yaël Dillies]

Here are the two options

import analysis.convex.strict
import analysis.convex.topology

open metric set

class strict_convex_space_through_balls (𝕜 E : Type*) [normed_linear_ordered_field 𝕜]
  [semi_normed_group E] [normed_space 𝕜 E] : Prop :=
(norm_strict_convex : strict_convex 𝕜 (ball (0 : E) 1))

class strict_convex_space_through_norm (E : Type*) [semi_normed_group E] [normed_space ℝ E] :
  Prop :=
(norm_strict_convex : strict_convex_on ℝ univ (@norm E _))

lemma are_they_equivalent (E : Type*) [semi_normed_group E] [normed_space ℝ E] :
  strict_convex_space_through_norm E ↔ strict_convex_space_through_balls ℝ E := sorry

The first one seems strictly convex more general?

[Yury G. Kudryashov]

Do you mean closed_ball?

[Yury G. Kudryashov]

I shouldn't formalize things after midnight: clearly, norm is not a strictly convex function on complex (take x = 1, y = 2, any a, b)

[Yury G. Kudryashov]

So, I should redo the last theorem assuming that closed_ball 0 R is convex.

[Yaël Dillies]

Yury G. Kudryashov said:

Do you mean closed_ball?

Uh, yes

[Yaël Dillies]

So the correct definition is the second one, right?

[Yury G. Kudryashov]

The correct definition is the first one with closed_ball: strict_convex_space_through_norm is never true on a non-trivial normed space (just take v and v + v).

[Yury G. Kudryashov]

(I'm not sure about radius 1 vs ∀ R but they're equivalent for real)

[Yaël Dillies]

That's what I meant :sweat_smile:

[Yury G. Kudryashov]

@Yaël Dillies Any news?

[Yury G. Kudryashov]

(if not, then I'll add a simple class with a couple of instances tonight)

[Yaël Dillies]

Yup, I have the stuff ready-ish if you need it.

[Yury G. Kudryashov]

PR?

[Yaël Dillies]

Will open it this evening.

[Yury G. Kudryashov]

Any news? @Yaël Dillies

[Yaël Dillies]

Just need to find an hour to put everything together.

[Yury G. Kudryashov]

Could you please open a PR with whatever you have on this subject?

[Yury G. Kudryashov]

@Yaël Dillies I'm sorry for poking you again but I would prefer if you either open a (possibly, not finalized) PR, or release the lock on this feature and let me implement it.

[Yaël Dillies]

Yes sorry, I've been having too much fun defining order categories. Doing it now.

[Yaël Dillies]

Are you happy with the PR?

[Yury G. Kudryashov]

I'll review it tonight. I'm trying to write a paper for ITP (deadline Feb. 8)

[Yaël Dillies]

Me too. Help :upside_down:

[Yaël Dillies]

@Yury G. Kudryashov, are you happy with the "two semirings" lemmas from #11794?

[Yury G. Kudryashov]

I'm trying to formalize a version of the maximum principle for strictly convex codomain.

[Yury G. Kudryashov]

I have the following problem: the completion of a strictly convex space may be not strictly convex. So, I have to either require [strict_convex_space F] [complete_space F] or [strict_convex_space (completion F)].

[Yury G. Kudryashov]

Are there any better options?

[Yury G. Kudryashov]

E.g., I don't know whether the principle is true in a strictly convex space if the completion is not strictly convex.