Restrictions, sums, differences, and uniform norm bounds for analytic phase functions.

theorem KamProject.Arnold1963.NormBoundOn.mono {E : Type u_1} {F : Type u_2} [NormedAddCommGroup F] {f : E → F} {S T : Set E} {M : ℝ} (h : NormBoundOn f S M) (hTS : T ⊆ S) : NormBoundOn f T M

theorem KamProject.Arnold1963.NormBoundOn.add {E : Type u_1} {F : Type u_2} [NormedAddCommGroup F] {f g : E → F} {S : Set E} {M N : ℝ} (hf : NormBoundOn f S M) (hg : NormBoundOn g S N) : NormBoundOn (fun (x : E) => f x + g x) S (M + N)

theorem KamProject.Arnold1963.NormBoundOn.sub {E : Type u_1} {F : Type u_2} [NormedAddCommGroup F] {f g : E → F} {S : Set E} {M N : ℝ} (hf : NormBoundOn f S M) (hg : NormBoundOn g S N) : NormBoundOn (fun (x : E) => f x - g x) S (M + N)

def KamProject.Arnold1963.AnalyticPhaseFunction.restrict {n : ℕ} {G U : Set (ComplexSpace n)} {ρ σ : NNReal} (f : AnalyticPhaseFunction n G ρ) (hUG : U ⊆ G) (hσρ : σ ≤ ρ) (hU : ConjInvariant U) : AnalyticPhaseFunction n U σ

Restriction to a conjugation-invariant action subdomain and a narrower angle strip.

Equations

• f.restrict hUG hσρ hU = { toFun := f.toFun, domain_conj := hU, analytic := ⋯, periodic := ⋯, conj_compatible := ⋯, bounded := ⋯ }

theorem KamProject.Arnold1963.AnalyticPhaseFunction.uniformNorm_restrict_le {n : ℕ} {G U : Set (ComplexSpace n)} {ρ σ : NNReal} (f : AnalyticPhaseFunction n G ρ) (hUG : U ⊆ G) (hσρ : σ ≤ ρ) (hU : ConjInvariant U) : (f.restrict hUG hσρ hU).uniformNorm ≤ f.uniformNorm

def KamProject.Arnold1963.AnalyticPhaseFunction.add {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f g : AnalyticPhaseFunction n G ρ) : AnalyticPhaseFunction n G ρ

Addition of analytic phase functions on the same domain and strip.

Equations

• f.add g = { toFun := fun (z : KamProject.Arnold1963.ComplexPhaseSpace n) => f.toFun z + g.toFun z, domain_conj := ⋯, analytic := ⋯, periodic := ⋯, conj_compatible := ⋯, bounded := ⋯ }

def KamProject.Arnold1963.AnalyticPhaseFunction.sub {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f g : AnalyticPhaseFunction n G ρ) : AnalyticPhaseFunction n G ρ

Subtraction of analytic phase functions on the same domain and strip.

Equations

• f.sub g = { toFun := fun (z : KamProject.Arnold1963.ComplexPhaseSpace n) => f.toFun z - g.toFun z, domain_conj := ⋯, analytic := ⋯, periodic := ⋯, conj_compatible := ⋯, bounded := ⋯ }

theorem KamProject.Arnold1963.AnalyticPhaseFunction.uniformNorm_add_le {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f g : AnalyticPhaseFunction n G ρ) : (f.add g).uniformNorm ≤ f.uniformNorm + g.uniformNorm

theorem KamProject.Arnold1963.AnalyticPhaseFunction.uniformNorm_sub_le {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f g : AnalyticPhaseFunction n G ρ) : (f.sub g).uniformNorm ≤ f.uniformNorm + g.uniformNorm

noncomputable def KamProject.Arnold1963.AnalyticPhaseFunction.addOnInter {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} {H : Set (ComplexSpace n)} {τ : NNReal} (f : AnalyticPhaseFunction n G ρ) (g : AnalyticPhaseFunction n H τ) : AnalyticPhaseFunction n (G ∩ H) (min ρ τ)

Addition after restricting both functions to their common phase domain.

Equations

• f.addOnInter g = (f.restrict ⋯ ⋯ ⋯).add (g.restrict ⋯ ⋯ ⋯)

noncomputable def KamProject.Arnold1963.AnalyticPhaseFunction.subOnInter {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} {H : Set (ComplexSpace n)} {τ : NNReal} (f : AnalyticPhaseFunction n G ρ) (g : AnalyticPhaseFunction n H τ) : AnalyticPhaseFunction n (G ∩ H) (min ρ τ)

Subtraction after restricting both functions to their common phase domain.

Equations

• f.subOnInter g = (f.restrict ⋯ ⋯ ⋯).sub (g.restrict ⋯ ⋯ ⋯)

@[simp]

theorem KamProject.Arnold1963.AnalyticPhaseFunction.addOnInter_toFun {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} {H : Set (ComplexSpace n)} {τ : NNReal} (f : AnalyticPhaseFunction n G ρ) (g : AnalyticPhaseFunction n H τ) (z : ComplexPhaseSpace n) : (f.addOnInter g).toFun z = f.toFun z + g.toFun z

@[simp]

theorem KamProject.Arnold1963.AnalyticPhaseFunction.subOnInter_toFun {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} {H : Set (ComplexSpace n)} {τ : NNReal} (f : AnalyticPhaseFunction n G ρ) (g : AnalyticPhaseFunction n H τ) (z : ComplexPhaseSpace n) : (f.subOnInter g).toFun z = f.toFun z - g.toFun z

theorem KamProject.Arnold1963.AnalyticPhaseFunction.uniformNorm_addOnInter_le {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} {H : Set (ComplexSpace n)} {τ : NNReal} (f : AnalyticPhaseFunction n G ρ) (g : AnalyticPhaseFunction n H τ) : (f.addOnInter g).uniformNorm ≤ f.uniformNorm + g.uniformNorm

theorem KamProject.Arnold1963.AnalyticPhaseFunction.uniformNorm_subOnInter_le {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} {H : Set (ComplexSpace n)} {τ : NNReal} (f : AnalyticPhaseFunction n G ρ) (g : AnalyticPhaseFunction n H τ) : (f.subOnInter g).uniformNorm ≤ f.uniformNorm + g.uniformNorm