First derivative bounds from one-variable Cauchy estimates along complex lines. All ambient operator estimates use the specified maximum norm.
theorem
KamProject.Arnold1963.norm_fderiv_apply_le_div_of_mem_erosion
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
[NormedAddCommGroup F]
[NormedSpace ℂ F]
{f : E → F}
{U : Set E}
{r : NNReal}
{M : ℝ}
{x v : E}
(hr : 0 < r)
(hf : AnalyticOnNhd ℂ f U)
(hM : NormBoundOn f U M)
(hx : x ∈ erosion U r)
(hv : ‖v‖ ≤ 1)
:
theorem
KamProject.Arnold1963.norm_fderiv_le_div_of_mem_erosion
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
[NormedAddCommGroup F]
[NormedSpace ℂ F]
{f : E → F}
{U : Set E}
{r : NNReal}
{M : ℝ}
{x : E}
(hr : 0 < r)
(hf : AnalyticOnNhd ℂ f U)
(hM : NormBoundOn f U M)
(hx : x ∈ erosion U r)
:
theorem
KamProject.Arnold1963.norm_pGradient_le_div
{n : ℕ}
{H : ComplexPhaseSpace n → ℂ}
{U : Set (ComplexPhaseSpace n)}
{r : NNReal}
{M : ℝ}
{x : ComplexPhaseSpace n}
(hr : 0 < r)
(hH : AnalyticOnNhd ℂ H U)
(hM : NormBoundOn H U M)
(hx : x ∈ erosion U r)
:
theorem
KamProject.Arnold1963.norm_qGradient_le_div
{n : ℕ}
{H : ComplexPhaseSpace n → ℂ}
{U : Set (ComplexPhaseSpace n)}
{r : NNReal}
{M : ℝ}
{x : ComplexPhaseSpace n}
(hr : 0 < r)
(hH : AnalyticOnNhd ℂ H U)
(hM : NormBoundOn H U M)
(hx : x ∈ erosion U r)
:
theorem
KamProject.Arnold1963.norm_hamiltonianVectorField_le_div
{n : ℕ}
{H : ComplexPhaseSpace n → ℂ}
{U : Set (ComplexPhaseSpace n)}
{r : NNReal}
{M : ℝ}
{x : ComplexPhaseSpace n}
(hr : 0 < r)
(hH : AnalyticOnNhd ℂ H U)
(hM : NormBoundOn H U M)
(hx : x ∈ erosion U r)
:
theorem
KamProject.Arnold1963.AnalyticPhaseFunction.norm_vectorField_le_div
{n : ℕ}
{G : Set (ComplexSpace n)}
{ρ r : NNReal}
(f : AnalyticPhaseFunction n G ρ)
(hr : 0 < r)
{x : ComplexPhaseSpace n}
(hx : x ∈ erosion (phaseDomain G ρ) r)
: