Analytic phase functions, conjugation compatibility, and the uniform norm. AnalyticOnNhd requires a convergent power series in an ambient neighborhood at each domain point. Bounded continuous restrictions supply the actual supremum norm, including on empty domains.

def KamProject.Arnold1963.NormBoundOn {E : Type u_1} {F : Type u_2} [NormedAddCommGroup F] (f : E → F) (S : Set E) (M : ℝ) : Prop

A nonnegative uniform norm bound on the specified set.

Equations

• KamProject.Arnold1963.NormBoundOn f S M = (0 ≤ M ∧ ∀ x ∈ S, ‖f x‖ ≤ M)

theorem KamProject.Arnold1963.NormBoundOn.nonneg {E : Type u_1} {F : Type u_2} [NormedAddCommGroup F] {f : E → F} {S : Set E} {M : ℝ} (h : NormBoundOn f S M) : 0 ≤ M

theorem KamProject.Arnold1963.NormBoundOn.norm_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup F] {f : E → F} {S : Set E} {M : ℝ} (h : NormBoundOn f S M) {x : E} (hx : x ∈ S) : ‖f x‖ ≤ M

@[simp]

theorem KamProject.Arnold1963.normBoundOn_empty {E : Type u_1} {F : Type u_2} [NormedAddCommGroup F] (f : E → F) (M : ℝ) : NormBoundOn f ∅ M ↔ 0 ≤ M

@[reducible, inline]

abbrev KamProject.Arnold1963.BoundedOnDomain {E : Type u_1} {F : Type u_2} [NormedAddCommGroup F] [TopologicalSpace E] (S : Set E) : Type (max u_1 u_2)

Bounded continuous functions on a domain, with the domain's subspace topology.

Equations

• KamProject.Arnold1963.BoundedOnDomain S = BoundedContinuousFunction (↑S) F

noncomputable def KamProject.Arnold1963.supNorm {E : Type u_1} {F : Type u_2} [NormedAddCommGroup F] [TopologicalSpace E] {S : Set E} (f : BoundedOnDomain S) : ℝ

The supremum norm inherited from bounded continuous functions on the domain.

Equations

• KamProject.Arnold1963.supNorm f = ‖f‖

def KamProject.Arnold1963.boundedRestriction {E : Type u_1} {F : Type u_2} [NormedAddCommGroup F] [TopologicalSpace E] (f : E → F) (S : Set E) (hf : ContinuousOn f S) (M : ℝ) (hM : NormBoundOn f S M) : BoundedOnDomain S

Packaging a continuous function restricted to a set together with its uniform bound.

Equations

• KamProject.Arnold1963.boundedRestriction f S hf M hM = BoundedContinuousFunction.ofNormedAddCommGroup (fun (x : ↑S) => f ↑x) ⋯ M ⋯

@[simp]

theorem KamProject.Arnold1963.boundedRestriction_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup F] [TopologicalSpace E] (f : E → F) (S : Set E) (hf : ContinuousOn f S) (M : ℝ) (hM : NormBoundOn f S M) (x : ↑S) : (boundedRestriction f S hf M hM) x = f ↑x

theorem KamProject.Arnold1963.norm_apply_le_supNorm {E : Type u_1} {F : Type u_2} [NormedAddCommGroup F] [TopologicalSpace E] {S : Set E} (f : BoundedOnDomain S) (x : ↑S) : ‖f x‖ ≤ supNorm f

theorem KamProject.Arnold1963.supNorm_le_iff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup F] [TopologicalSpace E] {S : Set E} (f : BoundedOnDomain S) {M : ℝ} (hM : 0 ≤ M) : supNorm f ≤ M ↔ ∀ (x : ↑S), ‖f x‖ ≤ M

theorem KamProject.Arnold1963.supNorm_lt_iff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup F] [TopologicalSpace E] {S : Set E} (f : BoundedOnDomain S) (M : ℝ) : supNorm f < M ↔ ∃ (C : ℝ), 0 ≤ C ∧ C < M ∧ ∀ (x : ↑S), ‖f x‖ ≤ C

theorem KamProject.Arnold1963.supNorm_boundedRestriction_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup F] [TopologicalSpace E] (f : E → F) (S : Set E) (hf : ContinuousOn f S) {M : ℝ} (hM : NormBoundOn f S M) : supNorm (boundedRestriction f S hf M hM) ≤ M

theorem KamProject.Arnold1963.analyticOnNhd_iff_forall_analyticAt {n : ℕ} (f : ComplexPhaseSpace n → ℂ) (S : Set (ComplexPhaseSpace n)) : AnalyticOnNhd ℂ f S ↔ ∀ x ∈ S, AnalyticAt ℂ f x

theorem KamProject.Arnold1963.analyticOnNhd_iff_exists_open {n : ℕ} (f : ComplexPhaseSpace n → ℂ) (S : Set (ComplexPhaseSpace n)) : AnalyticOnNhd ℂ f S ↔ ∃ (U : Set (ComplexPhaseSpace n)), IsOpen U ∧ S ⊆ U ∧ AnalyticOnNhd ℂ f U

def KamProject.Arnold1963.ConjCompatibleOn {n : ℕ} (f : ComplexPhaseSpace n → ℂ) (S : Set (ComplexPhaseSpace n)) : Prop

Compatibility of a phase function with complex conjugation on the specified set.

Equations

• KamProject.Arnold1963.ConjCompatibleOn f S = ∀ z ∈ S, f (KamProject.Arnold1963.conjPhase z) = star (f z)

structure KamProject.Arnold1963.AnalyticPhaseFunction (n : ℕ) (G : Set (ComplexSpace n)) (ρ : NNReal) : Type

A bounded analytic phase function with angle periodicity and real compatibility.

• toFun : ComplexPhaseSpace n → ℂ

  The underlying complex-valued function on action-angle phase space.

• domain_conj : ConjInvariant G
• analytic : AnalyticOnNhd ℂ self.toFun (phaseDomain G ρ)
• periodic : AnglePeriodicOn G ρ self.toFun
• conj_compatible : ConjCompatibleOn self.toFun (phaseDomain G ρ)
• bounded : ∃ (M : ℝ), NormBoundOn self.toFun (phaseDomain G ρ) M

noncomputable def KamProject.Arnold1963.AnalyticPhaseFunction.toBounded {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) : BoundedOnDomain (phaseDomain G ρ)

The bounded continuous restriction of an analytic phase function to its phase domain.

Equations

• f.toBounded = KamProject.Arnold1963.boundedRestriction f.toFun (KamProject.Arnold1963.phaseDomain G ρ) ⋯ ⋯.choose ⋯

noncomputable def KamProject.Arnold1963.AnalyticPhaseFunction.uniformNorm {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) : ℝ

The uniform norm of the phase function on its prescribed action-angle domain.

Equations

• f.uniformNorm = KamProject.Arnold1963.supNorm f.toBounded

theorem KamProject.Arnold1963.AnalyticPhaseFunction.norm_le_iff {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {M : ℝ} : f.uniformNorm ≤ M ↔ NormBoundOn f.toFun (phaseDomain G ρ) M

theorem KamProject.Arnold1963.AnalyticPhaseFunction.real_value {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) (p q : RealSpace n) (hp : complexify p ∈ G) : (f.toFun (complexify p, complexify q)).im = 0

def KamProject.Arnold1963.AnalyticPhaseFunction.constReal {n : ℕ} (G : Set (ComplexSpace n)) (ρ : NNReal) (hG : ConjInvariant G) (c : ℝ) : AnalyticPhaseFunction n G ρ

A real constant packaged as an analytic phase function on a conjugation-invariant domain.

Equations

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

theorem KamProject.Arnold1963.AnalyticPhaseFunction.uniformNorm_constReal {n : ℕ} (G : Set (ComplexSpace n)) (ρ : NNReal) (hG : ConjInvariant G) (hne : G.Nonempty) (c : ℝ) : (constReal G ρ hG c).uniformNorm = |c|