Real-slice Jacobian estimates. The maximum-norm unit cube gives the sharp C ^ n determinant bound without an additional dimension factor.

noncomputable def KamProject.Arnold1963.complexifyCLM (n : ℕ) : RealSpace n →L[ℝ] ComplexSpace n

Coordinatewise complexification as a real continuous linear map.

Equations

• KamProject.Arnold1963.complexifyCLM n = ContinuousLinearMap.pi fun (j : Fin n) => Complex.ofRealCLM ∘SL ContinuousLinearMap.proj j

noncomputable def KamProject.Arnold1963.realPartCLM (n : ℕ) : ComplexSpace n →L[ℝ] RealSpace n

Coordinatewise real-part projection as a real continuous linear map.

Equations

• KamProject.Arnold1963.realPartCLM n = ContinuousLinearMap.pi fun (j : Fin n) => Complex.reCLM ∘SL ContinuousLinearMap.proj j

@[simp]

theorem KamProject.Arnold1963.complexifyCLM_apply {n : ℕ} (x : RealSpace n) : (complexifyCLM n) x = complexify x

@[simp]

theorem KamProject.Arnold1963.realPartCLM_apply {n : ℕ} (z : ComplexSpace n) : (realPartCLM n) z = realPart z

theorem KamProject.Arnold1963.norm_realPart_le {n : ℕ} (z : ComplexSpace n) : ‖realPart z‖ ≤ ‖z‖

def KamProject.Arnold1963.realRestriction {n : ℕ} (f : ComplexSpace n → ComplexSpace n) : RealSpace n → RealSpace n

Restriction of a complex action map to real input and output coordinates.

Equations

• KamProject.Arnold1963.realRestriction f = KamProject.Arnold1963.realPart ∘ f ∘ KamProject.Arnold1963.complexify

noncomputable def KamProject.Arnold1963.realDerivative {n : ℕ} (L : ComplexSpace n →L[ℂ] ComplexSpace n) : RealSpace n →L[ℝ] RealSpace n

The real continuous linear map induced by restricting a complex derivative.

Equations

• KamProject.Arnold1963.realDerivative L = KamProject.Arnold1963.realPartCLM n ∘SL ContinuousLinearMap.restrictScalars ℝ L ∘SL KamProject.Arnold1963.complexifyCLM n

theorem KamProject.Arnold1963.hasFDerivAt_realRestriction {n : ℕ} {f : ComplexSpace n → ComplexSpace n} {x : RealSpace n} (hf : DifferentiableAt ℂ f (complexify x)) : HasFDerivAt (realRestriction f) (realDerivative (fderiv ℂ f (complexify x))) x

theorem KamProject.Arnold1963.norm_realDerivative_le {n : ℕ} (L : ComplexSpace n →L[ℂ] ComplexSpace n) : ‖realDerivative L‖ ≤ ‖L‖

theorem KamProject.Arnold1963.abs_det_le_pow_of_opNorm_le {n : ℕ} (L : RealSpace n →L[ℝ] RealSpace n) {C : ℝ} (hC : 0 ≤ C) (hL : ‖L‖ ≤ C) : |LinearMap.det ↑L| ≤ C ^ n

theorem KamProject.Arnold1963.real_image_measure_le {n : ℕ} {f : RealSpace n → RealSpace n} {s : Set (RealSpace n)} {C : ℝ} (hs : MeasurableSet s) (hC : 0 ≤ C) (hf : ∀ x ∈ s, DifferentiableAt ℝ f x) (hd : ∀ x ∈ s, ‖fderiv ℝ f x‖ ≤ C) : MeasureTheory.volume (f '' s) ≤ ENNReal.ofReal (C ^ n) * MeasureTheory.volume s