Descent of an even smooth curve through the square map

The regularized radial derivative is obtained from the integral Hadamard formula, not from a convergent power series. Its iterates are the genuine one-sided derivatives of X ↦ f (sqrt X).

theorem NavierStokes.EvenSmoothDescent.contDiff_iteratedDeriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) : ContDiff ℝ (↑⊤) (iteratedDeriv n f)

theorem NavierStokes.EvenSmoothDescent.iteratedDeriv_iteratedDeriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) (m n : ℕ) : iteratedDeriv m (iteratedDeriv n f) = iteratedDeriv (m + n) f

noncomputable def NavierStokes.EvenSmoothDescent.average {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) (x : ℝ) : E

Average, given by ∫ t in (0 : ℝ)..1, f (t * x).

Equations

• NavierStokes.EvenSmoothDescent.average f x = ∫ (t : ℝ) in 0..1, f (t * x)

theorem NavierStokes.EvenSmoothDescent.iteratedDeriv_scale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x t : ℝ) : iteratedDeriv n (fun (y : ℝ) => f (t * y)) x = t ^ n • iteratedDeriv n f (t * x)

theorem NavierStokes.EvenSmoothDescent.continuous_scaled_jet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) : Continuous fun (z : ℝ × ℝ) => iteratedDeriv n (fun (x : ℝ) => f (z.2 * x)) z.1

theorem NavierStokes.EvenSmoothDescent.measurable_scaled_jet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : ℝ) : MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => iteratedDeriv n (fun (y : ℝ) => f (t * y)) x) (MeasureTheory.volume.restrict (Set.Ioc 0 1))

theorem NavierStokes.EvenSmoothDescent.dominated_scaled_jet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} (hf : ContDiff ℝ (↑⊤) f) : SmoothParameterIntegral.LocallyDominatedDeriv (fun (x t : ℝ) => f (t * x)) (MeasureTheory.volume.restrict (Set.Ioc 0 1))

theorem NavierStokes.EvenSmoothDescent.contDiff_average {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (average f)

theorem NavierStokes.EvenSmoothDescent.iteratedDeriv_average {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : ℝ) : iteratedDeriv n (average f) x = ∫ (t : ℝ) in 0..1, t ^ n • iteratedDeriv n f (t * x)

theorem NavierStokes.EvenSmoothDescent.iteratedDeriv_average_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) : iteratedDeriv n (average f) 0 = (1 / (↑n + 1)) • iteratedDeriv n f 0

theorem NavierStokes.EvenSmoothDescent.average_deriv_identity {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} (hf : ContDiff ℝ (↑⊤) f) (x : ℝ) : x • average (deriv f) x = f x - f 0

noncomputable def NavierStokes.EvenSmoothDescent.radialDerivative {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) (x : ℝ) : E

Radial derivative, given by (1 / 2 : ℝ) • average (iteratedDeriv 2 f) x.

Equations

• NavierStokes.EvenSmoothDescent.radialDerivative f x = (1 / 2) • NavierStokes.EvenSmoothDescent.average (iteratedDeriv 2 f) x

theorem NavierStokes.EvenSmoothDescent.contDiff_radialDerivative {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (radialDerivative f)

theorem NavierStokes.EvenSmoothDescent.even_iteratedDeriv_two {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} (he : Function.Even f) : Function.Even (iteratedDeriv 2 f)

theorem NavierStokes.EvenSmoothDescent.even_average {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} (he : Function.Even f) : Function.Even (average f)

theorem NavierStokes.EvenSmoothDescent.even_radialDerivative {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} (he : Function.Even f) : Function.Even (radialDerivative f)

theorem NavierStokes.EvenSmoothDescent.deriv_zero_of_even {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} (he : Function.Even f) : deriv f 0 = 0

theorem NavierStokes.EvenSmoothDescent.radialDerivative_identity {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} (hf : ContDiff ℝ (↑⊤) f) (he : Function.Even f) (x : ℝ) : (2 * x) • radialDerivative f x = deriv f x

theorem NavierStokes.EvenSmoothDescent.radialDerivative_eq_div {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} (hf : ContDiff ℝ (↑⊤) f) (he : Function.Even f) {x : ℝ} (hx : x ≠ 0) : radialDerivative f x = (1 / (2 * x)) • deriv f x

theorem NavierStokes.EvenSmoothDescent.iteratedDeriv_radialDerivative_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) : iteratedDeriv n (radialDerivative f) 0 = (1 / (2 * (↑n + 1))) • iteratedDeriv (n + 2) f 0

noncomputable def NavierStokes.EvenSmoothDescent.descent {E : Type u_1} (f : ℝ → E) (X : ℝ) : E

Descent, given by f (Real.sqrt X).

Equations

• NavierStokes.EvenSmoothDescent.descent f X = f √X

theorem NavierStokes.EvenSmoothDescent.descent_square {E : Type u_1} {f : ℝ → E} (he : Function.Even f) (x : ℝ) : descent f (x ^ 2) = f x

theorem NavierStokes.EvenSmoothDescent.continuous_descent {E : Type u_1} [NormedAddCommGroup E] {f : ℝ → E} (hf : Continuous f) : Continuous (descent f)

theorem NavierStokes.EvenSmoothDescent.hasDerivAt_descent_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} (hf : ContDiff ℝ (↑⊤) f) (he : Function.Even f) {X : ℝ} (hX : 0 < X) : HasDerivAt (descent f) (descent (radialDerivative f) X) X

theorem NavierStokes.EvenSmoothDescent.hasDerivWithinAt_descent_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} (hf : ContDiff ℝ (↑⊤) f) (he : Function.Even f) : HasDerivWithinAt (descent f) (radialDerivative f 0) (Set.Ici 0) 0

theorem NavierStokes.EvenSmoothDescent.hasDerivWithinAt_descent {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} (hf : ContDiff ℝ (↑⊤) f) (he : Function.Even f) {X : ℝ} (hX : X ∈ Set.Ici 0) : HasDerivWithinAt (descent f) (descent (radialDerivative f) X) (Set.Ici 0) X

noncomputable def NavierStokes.EvenSmoothDescent.radialIterate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) (n : ℕ) : ℝ → E

Radial iterate, given by (radialDerivative^[n]) f.

Equations

• NavierStokes.EvenSmoothDescent.radialIterate f n = NavierStokes.EvenSmoothDescent.radialDerivative^[n] f

theorem NavierStokes.EvenSmoothDescent.radialIterate_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) : radialIterate f 0 = f

theorem NavierStokes.EvenSmoothDescent.radialIterate_succ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) (n : ℕ) : radialIterate f (n + 1) = radialDerivative (radialIterate f n)

theorem NavierStokes.EvenSmoothDescent.radialIterate_succ_right {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) (n : ℕ) : radialIterate f (n + 1) = radialIterate (radialDerivative f) n

theorem NavierStokes.EvenSmoothDescent.contDiff_radialIterate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) : ContDiff ℝ (↑⊤) (radialIterate f n)

theorem NavierStokes.EvenSmoothDescent.even_radialIterate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} (he : Function.Even f) (n : ℕ) : Function.Even (radialIterate f n)

theorem NavierStokes.EvenSmoothDescent.iteratedDerivWithin_descent {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} (hf : ContDiff ℝ (↑⊤) f) (he : Function.Even f) (n : ℕ) : Set.EqOn (iteratedDerivWithin n (descent f) (Set.Ici 0)) (descent (radialIterate f n)) (Set.Ici 0)

The iterates of the regularized radial derivative are the actual one-sided derivatives, including at the origin.

theorem NavierStokes.EvenSmoothDescent.contDiffOn_descent {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} (hf : ContDiff ℝ (↑⊤) f) (he : Function.Even f) : ContDiffOn ℝ (↑⊤) (descent f) (Set.Ici 0)

theorem NavierStokes.EvenSmoothDescent.radialIterate_at_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (n : ℕ) {f : ℝ → E} (hf : ContDiff ℝ (↑⊤) f) : radialIterate f n 0 = (↑n.factorial / ↑(2 * n).factorial) • iteratedDeriv (2 * n) f 0

theorem NavierStokes.EvenSmoothDescent.iteratedDerivWithin_descent_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} (hf : ContDiff ℝ (↑⊤) f) (he : Function.Even f) (n : ℕ) : iteratedDerivWithin n (descent f) (Set.Ici 0) 0 = (↑n.factorial / ↑(2 * n).factorial) • iteratedDeriv (2 * n) f 0

Exact right jets of the descended function.

The local theorem uses an explicit cutoff extension. This extension is constructed here; the input is not assumed to have a global even extension.

noncomputable def NavierStokes.EvenSmoothDescent.evenCutoff (r x : ℝ) : ℝ

Even cutoff, given by SmoothCutoffs.scaledCutoff (2 / r) x * SmoothCutoffs.scaledCutoff (2 / r) (-x).

Equations

• NavierStokes.EvenSmoothDescent.evenCutoff r x = NavierStokes.SmoothCutoffs.scaledCutoff (2 / r) x * NavierStokes.SmoothCutoffs.scaledCutoff (2 / r) (-x)

noncomputable def NavierStokes.EvenSmoothDescent.localized {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (r : ℝ) (f : ℝ → E) (x : ℝ) : E

Localized, given by evenCutoff r x • f x.

Equations

• NavierStokes.EvenSmoothDescent.localized r f x = NavierStokes.EvenSmoothDescent.evenCutoff r x • f x

theorem NavierStokes.EvenSmoothDescent.contDiff_evenCutoff (r : ℝ) : ContDiff ℝ (↑⊤) (evenCutoff r)

theorem NavierStokes.EvenSmoothDescent.even_evenCutoff (r : ℝ) : Function.Even (evenCutoff r)

theorem NavierStokes.EvenSmoothDescent.evenCutoff_eventually_one (r : ℝ) : evenCutoff r =ᶠ[nhds 0] fun (x : ℝ) => 1

theorem NavierStokes.EvenSmoothDescent.localized_eventuallyEq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (r : ℝ) (f : ℝ → E) : localized r f =ᶠ[nhds 0] f

theorem NavierStokes.EvenSmoothDescent.localized_eventually_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {r x : ℝ} (hr : 0 < r) (hx : r ≤ |x|) (f : ℝ → E) : localized r f =ᶠ[nhds x] fun (x : ℝ) => 0

theorem NavierStokes.EvenSmoothDescent.contDiff_localized {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} (hr : 0 < r) {f : ℝ → E} (hf : ContDiffOn ℝ (↑⊤) f (Set.Ioo (-r) r)) : ContDiff ℝ (↑⊤) (localized r f)

theorem NavierStokes.EvenSmoothDescent.even_localized {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} (hr : 0 < r) {f : ℝ → E} (he : ∀ x ∈ Set.Ioo (-r) r, f (-x) = f x) : Function.Even (localized r f)

theorem NavierStokes.EvenSmoothDescent.descent_localized_eventuallyEq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (r : ℝ) (f : ℝ → E) : descent (localized r f) =ᶠ[nhds 0] descent f

theorem NavierStokes.EvenSmoothDescent.contDiffWithinAt_descent_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {r : ℝ} (hr : 0 < r) {f : ℝ → E} (hf : ContDiffOn ℝ (↑⊤) f (Set.Ioo (-r) r)) (he : ∀ x ∈ Set.Ioo (-r) r, f (-x) = f x) : ContDiffWithinAt ℝ (↑⊤) (descent f) (Set.Ici 0) 0

Smoothness at the boundary requires only a smooth even germ on a symmetric open interval. The global cutoff extension is constructed in the proof.

theorem NavierStokes.EvenSmoothDescent.contDiffOn_descent_local {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {r : ℝ} (hr : 0 < r) {f : ℝ → E} (hf : ContDiffOn ℝ (↑⊤) f (Set.Ioo (-r) r)) (he : ∀ x ∈ Set.Ioo (-r) r, f (-x) = f x) : ContDiffOn ℝ (↑⊤) (descent f) (Set.Ico 0 (r ^ 2))

theorem NavierStokes.EvenSmoothDescent.descent_square_local {E : Type u_1} {r : ℝ} {f : ℝ → E} (he : ∀ x ∈ Set.Ioo (-r) r, f (-x) = f x) {x : ℝ} (hx : x ∈ Set.Ioo (-r) r) : descent f (x ^ 2) = f x

theorem NavierStokes.EvenSmoothDescent.iteratedDerivWithin_descent_zero_local {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {r : ℝ} (hr : 0 < r) {f : ℝ → E} (hf : ContDiffOn ℝ (↑⊤) f (Set.Ioo (-r) r)) (he : ∀ x ∈ Set.Ioo (-r) r, f (-x) = f x) (n : ℕ) : iteratedDerivWithin n (descent f) (Set.Ici 0) 0 = (↑n.factorial / ↑(2 * n).factorial) • iteratedDeriv (2 * n) f 0

The exact endpoint jets of the local descent, using actual within derivatives on the closed positive half-line.