Joint smoothness of even descent

This module treats a real auxiliary parameter and a real radial coordinate. The full derivative on the closed half-plane is proved before any higher-order regularity is inferred. Separate smoothness is not used as a substitute for joint smoothness.

@[reducible, inline]

abbrev NavierStokes.ParametricEvenDescent.Plane : Type

Plane: an abbreviation for ℝ × ℝ.

Equations

• NavierStokes.ParametricEvenDescent.Plane = (ℝ × ℝ)

noncomputable def NavierStokes.ParametricEvenDescent.EvenRadial {E : Type u} (F : Plane → E) : Prop

Even radial, given by ∀ p, Function.Even (fun r => F (p, r)).

Equations

• NavierStokes.ParametricEvenDescent.EvenRadial F = ∀ (p : ℝ), Function.Even fun (r : ℝ) => F (p, r)

noncomputable def NavierStokes.ParametricEvenDescent.parameterPartial {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : Plane → E) (q : Plane) : E

Parameter partial, given by deriv (fun p => F (p, q.2)) q.1.

Equations

• NavierStokes.ParametricEvenDescent.parameterPartial F q = deriv (fun (p : ℝ) => F (p, q.2)) q.1

noncomputable def NavierStokes.ParametricEvenDescent.radialPartial {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : Plane → E) (q : Plane) : E

Radial partial, given by deriv (fun r => F (q.1, r)) q.2.

Equations

• NavierStokes.ParametricEvenDescent.radialPartial F q = deriv (fun (r : ℝ) => F (q.1, r)) q.2

noncomputable def NavierStokes.ParametricEvenDescent.radialReduce {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : Plane → E) (q : Plane) : E

Radial reduce, given by EvenSmoothDescent.radialDerivative (fun r => F (q.1, r)) q.2.

Equations

• NavierStokes.ParametricEvenDescent.radialReduce F q = NavierStokes.EvenSmoothDescent.radialDerivative (fun (r : ℝ) => F (q.1, r)) q.2

noncomputable def NavierStokes.ParametricEvenDescent.descend {E : Type u} (F : Plane → E) (q : Plane) : E

Descend, given by F (q.1, Real.sqrt q.2).

Equations

• NavierStokes.ParametricEvenDescent.descend F q = F (q.1, √q.2)

noncomputable def NavierStokes.ParametricEvenDescent.planeDerivative {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : Plane → E) (q : Plane) : Plane →L[ℝ] E

Plane derivative, given by `(ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight (parameterPartial F q)

• (ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight (radialReduce F q)`.

Equations

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

theorem NavierStokes.ParametricEvenDescent.parameterPartial_eq_fderiv {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Plane → E} (hF : ContDiff ℝ (↑⊤) F) (q : Plane) : parameterPartial F q = (fderiv ℝ F q) (1, 0)

theorem NavierStokes.ParametricEvenDescent.radialPartial_eq_fderiv {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Plane → E} (hF : ContDiff ℝ (↑⊤) F) (q : Plane) : radialPartial F q = (fderiv ℝ F q) (0, 1)

theorem NavierStokes.ParametricEvenDescent.fderiv_decompose {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Plane → E} (hF : ContDiff ℝ (↑⊤) F) (q v : Plane) : (fderiv ℝ F q) v = v.1 • parameterPartial F q + v.2 • radialPartial F q

theorem NavierStokes.ParametricEvenDescent.contDiff_parameterPartial {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Plane → E} (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ (↑⊤) (parameterPartial F)

theorem NavierStokes.ParametricEvenDescent.contDiff_radialPartial {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Plane → E} (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ (↑⊤) (radialPartial F)

theorem NavierStokes.ParametricEvenDescent.radialReduce_integral {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : Plane → E) (q : Plane) : radialReduce F q = (1 / 2) • ∫ (t : ℝ) in 0..1, radialPartial (radialPartial F) (q.1, t * q.2)

theorem NavierStokes.ParametricEvenDescent.contDiff_radialReduce {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Plane → E} (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ (↑⊤) (radialReduce F)

theorem NavierStokes.ParametricEvenDescent.even_parameterPartial {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Plane → E} (hEven : EvenRadial F) : EvenRadial (parameterPartial F)

theorem NavierStokes.ParametricEvenDescent.even_radialReduce {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Plane → E} (hEven : EvenRadial F) : EvenRadial (radialReduce F)

theorem NavierStokes.ParametricEvenDescent.contDiff_planeDerivative {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Plane → E} (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ (↑⊤) (planeDerivative F)

theorem NavierStokes.ParametricEvenDescent.even_planeDerivative {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Plane → E} (hEven : EvenRadial F) : EvenRadial (planeDerivative F)

theorem NavierStokes.ParametricEvenDescent.continuous_descend {E : Type u} [NormedAddCommGroup E] {F : Plane → E} (hF : Continuous F) : Continuous (descend F)

theorem NavierStokes.ParametricEvenDescent.radialPartial_identity {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {F : Plane → E} (hF : ContDiff ℝ (↑⊤) F) (hEven : EvenRadial F) (q : Plane) : radialPartial F q = (2 * q.2) • radialReduce F q

theorem NavierStokes.ParametricEvenDescent.hasFDerivAt_descend_pos {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {F : Plane → E} (hF : ContDiff ℝ (↑⊤) F) (hEven : EvenRadial F) {q : Plane} (hq : 0 < q.2) : HasFDerivAt (descend F) (descend (planeDerivative F) q) q

theorem NavierStokes.ParametricEvenDescent.hasFDerivWithinAt_descend {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {F : Plane → E} (hF : ContDiff ℝ (↑⊤) F) (hEven : EvenRadial F) (q : Plane) : HasFDerivWithinAt (descend F) (descend (planeDerivative F) q) (Set.univ ×ˢ Set.Ici 0) q

The full Fréchet derivative extends to the boundary of the half-plane.

theorem NavierStokes.ParametricEvenDescent.contDiffOn_descend {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {F : Plane → E} (hF : ContDiff ℝ (↑⊤) F) (hEven : EvenRadial F) : ContDiffOn ℝ (↑⊤) (descend F) (Set.univ ×ˢ Set.Ici 0)

Joint smoothness in the auxiliary parameter and the squared radial variable.

noncomputable def NavierStokes.ParametricEvenDescent.localized {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (a A R : ℝ) (F : Plane → E) (q : Plane) : E

Localized, given by (EvenSmoothDescent.evenCutoff A (q.1 - a) * EvenSmoothDescent.evenCutoff R q.2) • F q.

Equations

• NavierStokes.ParametricEvenDescent.localized a A R F q = (NavierStokes.EvenSmoothDescent.evenCutoff A (q.1 - a) * NavierStokes.EvenSmoothDescent.evenCutoff R q.2) • F q

theorem NavierStokes.ParametricEvenDescent.localized_eventually_zero_parameter {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {a A R : ℝ} (hA : 0 < A) {q : Plane} (hq : A ≤ |q.1 - a|) (F : Plane → E) : localized a A R F =ᶠ[nhds q] fun (x : Plane) => 0

theorem NavierStokes.ParametricEvenDescent.localized_eventually_zero_radial {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {a A R : ℝ} (hR : 0 < R) {q : Plane} (hq : R ≤ |q.2|) (F : Plane → E) : localized a A R F =ᶠ[nhds q] fun (x : Plane) => 0

theorem NavierStokes.ParametricEvenDescent.contDiff_localized {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {a A R : ℝ} (hA : 0 < A) (hR : 0 < R) {F : Plane → E} (hF : ContDiffOn ℝ (↑⊤) F (Set.Ioo (a - A) (a + A) ×ˢ Set.Ioo (-R) R)) : ContDiff ℝ (↑⊤) (localized a A R F)

theorem NavierStokes.ParametricEvenDescent.even_localized {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {a A R : ℝ} (hA : 0 < A) (hR : 0 < R) {F : Plane → E} (he : ∀ p ∈ Set.Ioo (a - A) (a + A), ∀ r ∈ Set.Ioo (-R) R, F (p, -r) = F (p, r)) : EvenRadial (localized a A R F)

theorem NavierStokes.ParametricEvenDescent.localized_eventuallyEq {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (a A R : ℝ) (F : Plane → E) : localized a A R F =ᶠ[nhds (a, 0)] F

theorem NavierStokes.ParametricEvenDescent.descend_localized_eventuallyEq {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (a A R : ℝ) (F : Plane → E) : descend (localized a A R F) =ᶠ[nhds (a, 0)] descend F

theorem NavierStokes.ParametricEvenDescent.contDiffWithinAt_descend_axis_local {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a A R : ℝ} (hA : 0 < A) (hR : 0 < R) {F : Plane → E} (hF : ContDiffOn ℝ (↑⊤) F (Set.Ioo (a - A) (a + A) ×ˢ Set.Ioo (-R) R)) (he : ∀ p ∈ Set.Ioo (a - A) (a + A), ∀ r ∈ Set.Ioo (-R) R, F (p, -r) = F (p, r)) : ContDiffWithinAt ℝ (↑⊤) (descend F) (Set.univ ×ˢ Set.Ici 0) (a, 0)

Joint smoothness at the axis uses only an actual smooth, radially even germ.

theorem NavierStokes.ParametricEvenDescent.contDiffOn_descend_local {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {U : Set ℝ} (hU : IsOpen U) {R : ℝ} (hR : 0 < R) {F : Plane → E} (hF : ContDiffOn ℝ (↑⊤) F (U ×ˢ Set.Ioo (-R) R)) (he : ∀ p ∈ U, ∀ r ∈ Set.Ioo (-R) R, F (p, -r) = F (p, r)) : ContDiffOn ℝ (↑⊤) (descend F) (U ×ˢ Set.Ico 0 (R ^ 2))

Local joint smoothness on an open parameter set and a closed radial half-interval.

theorem NavierStokes.ParametricEvenDescent.descend_square_local {E : Type u} {U : Set ℝ} {R : ℝ} {F : Plane → E} (he : ∀ p ∈ U, ∀ r ∈ Set.Ioo (-R) R, F (p, -r) = F (p, r)) {p r : ℝ} (hp : p ∈ U) (hr : r ∈ Set.Ioo (-R) R) : descend F (p, r ^ 2) = F (p, r)

Exact recovery of the original radial field after substituting a square.

theorem NavierStokes.ParametricEvenDescent.iteratedDerivWithin_descend_axis_local {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {U : Set ℝ} {R : ℝ} (hR : 0 < R) {F : Plane → E} (hF : ContDiffOn ℝ (↑⊤) F (U ×ˢ Set.Ioo (-R) R)) (he : ∀ p ∈ U, ∀ r ∈ Set.Ioo (-R) R, F (p, -r) = F (p, r)) {p : ℝ} (hp : p ∈ U) (n : ℕ) : iteratedDerivWithin n (fun (X : ℝ) => descend F (p, X)) (Set.Ici 0) 0 = (↑n.factorial / ↑(2 * n).factorial) • iteratedDeriv (2 * n) (fun (r : ℝ) => F (p, r)) 0

The radial right jets in the joint descent are the exact even radial jets.