Canonical axis jets without a negative squared-radius extension

The squared-radius jets are the iterates of the integral Hadamard operator on the signed radial variable. They are genuine right derivatives at the axis and genuine ordinary derivatives at positive squared radius.

noncomputable def NavierStokes.BoundaryAxisJets.radialJet {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : ℝ × P → E) (k : ℕ) (r : ℝ) (z : P) : E

Radial jet, given by EvenSmoothDescent.radialIterate (fun s => F (s, z)) k r.

Equations

• NavierStokes.BoundaryAxisJets.radialJet F k r z = NavierStokes.EvenSmoothDescent.radialIterate (fun (s : ℝ) => F (s, z)) k r

noncomputable def NavierStokes.BoundaryAxisJets.axisJet {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : ℝ × P → E) (k : ℕ) (p : ℝ × P) : E

Axis jet, given by radialJet F k (Real.sqrt p.1) p.2.

Equations

• NavierStokes.BoundaryAxisJets.axisJet F k p = NavierStokes.BoundaryAxisJets.radialJet F k (√p.1) p.2

theorem NavierStokes.BoundaryAxisJets.radialJet_succ {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : ℝ × P → E) (k : ℕ) (r : ℝ) (z : P) : radialJet F (k + 1) r z = EvenSmoothDescent.radialDerivative (fun (s : ℝ) => radialJet F k s z) r

theorem NavierStokes.BoundaryAxisJets.radialJet_even {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : ℝ × P → E} {z : P} (he : Function.Even fun (r : ℝ) => F (r, z)) (k : ℕ) : Function.Even fun (r : ℝ) => radialJet F k r z

theorem NavierStokes.BoundaryAxisJets.axisJet_square {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : ℝ × P → E} {z : P} (he : Function.Even fun (r : ℝ) => F (r, z)) (k : ℕ) (r : ℝ) : axisJet F k (r ^ 2, z) = radialJet F k r z

theorem NavierStokes.BoundaryAxisJets.radialJet_contDiff {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : ℝ × P → E} {z : P} (hf : ContDiff ℝ ↑⊤ fun (r : ℝ) => F (r, z)) (k : ℕ) : ContDiff ℝ ↑⊤ fun (r : ℝ) => radialJet F k r z

theorem NavierStokes.BoundaryAxisJets.axisJet_eq_iteratedDerivWithin {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {F : ℝ × P → E} {z : P} (hf : ContDiff ℝ ↑⊤ fun (r : ℝ) => F (r, z)) (he : Function.Even fun (r : ℝ) => F (r, z)) (k : ℕ) {X : ℝ} (hX : 0 ≤ X) : axisJet F k (X, z) = iteratedDerivWithin k (fun (Y : ℝ) => F (√Y, z)) (Set.Ici 0) X

theorem NavierStokes.BoundaryAxisJets.axisJet_hasDerivWithinAt {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {F : ℝ × P → E} {z : P} (hf : ContDiff ℝ ↑⊤ fun (r : ℝ) => F (r, z)) (he : Function.Even fun (r : ℝ) => F (r, z)) (k : ℕ) {X : ℝ} (hX : 0 ≤ X) : HasDerivWithinAt (fun (Y : ℝ) => axisJet F k (Y, z)) (axisJet F (k + 1) (X, z)) (Set.Ici 0) X

theorem NavierStokes.BoundaryAxisJets.axisJet_hasDerivAt_pos {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {F : ℝ × P → E} {z : P} (hf : ContDiff ℝ ↑⊤ fun (r : ℝ) => F (r, z)) (he : Function.Even fun (r : ℝ) => F (r, z)) (k : ℕ) {X : ℝ} (hX : 0 < X) : HasDerivAt (fun (Y : ℝ) => axisJet F k (Y, z)) (axisJet F (k + 1) (X, z)) X

theorem NavierStokes.BoundaryAxisJets.axisJet_eq_iteratedDeriv_pos {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {F : ℝ × P → E} {z : P} (hf : ContDiff ℝ ↑⊤ fun (r : ℝ) => F (r, z)) (he : Function.Even fun (r : ℝ) => F (r, z)) (k : ℕ) {X : ℝ} (hX : 0 < X) : axisJet F k (X, z) = iteratedDeriv k (fun (Y : ℝ) => F (√Y, z)) X

theorem NavierStokes.BoundaryAxisJets.axisJet_zero {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {F : ℝ × P → E} {z : P} (hf : ContDiff ℝ ↑⊤ fun (r : ℝ) => F (r, z)) (k : ℕ) : axisJet F k (0, z) = (↑k.factorial / ↑(2 * k).factorial) • iteratedDeriv (2 * k) (fun (r : ℝ) => F (r, z)) 0

Locality of the genuine Hadamard iterates

theorem NavierStokes.BoundaryAxisJets.scaled_mem_Ioo {R r t : ℝ} (hr : r ∈ Set.Ioo (-R) R) (ht : t ∈ Set.Icc 0 1) : t * r ∈ Set.Ioo (-R) R

theorem NavierStokes.BoundaryAxisJets.radialDerivative_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {R : ℝ} {f g : ℝ → E} (hfg : Set.EqOn f g (Set.Ioo (-R) R)) {r : ℝ} (hr : r ∈ Set.Ioo (-R) R) : EvenSmoothDescent.radialDerivative f r = EvenSmoothDescent.radialDerivative g r

theorem NavierStokes.BoundaryAxisJets.radialJet_congr {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {R : ℝ} {F G : ℝ × P → E} {z : P} (hfg : ∀ r ∈ Set.Ioo (-R) R, F (r, z) = G (r, z)) (k : ℕ) (r : ℝ) : r ∈ Set.Ioo (-R) R → radialJet F k r z = radialJet G k r z

noncomputable def NavierStokes.BoundaryAxisJets.localized {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : ℝ) (F : ℝ × P → E) (p : ℝ × P) : E

Localized, given by EvenSmoothDescent.localized R (fun r => F (r, p.2)) p.1.

Equations

• NavierStokes.BoundaryAxisJets.localized R F p = NavierStokes.EvenSmoothDescent.localized R (fun (r : ℝ) => F (r, p.2)) p.1

theorem NavierStokes.BoundaryAxisJets.evenCutoff_one {R r : ℝ} (hR : 0 < R) (hr : |r| ≤ R / 4) : EvenSmoothDescent.evenCutoff R r = 1

theorem NavierStokes.BoundaryAxisJets.localized_eq {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {R r : ℝ} (hR : 0 < R) (hr : |r| ≤ R / 4) (F : ℝ × P → E) (z : P) : localized R F (r, z) = F (r, z)

theorem NavierStokes.BoundaryAxisJets.radialJet_localized_eq {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {R : ℝ} (hR : 0 < R) (F : ℝ × P → E) (z : P) (k : ℕ) {r : ℝ} (hr : r ∈ Set.Ioo (-(R / 4)) (R / 4)) : radialJet (localized R F) k r z = radialJet F k r z

theorem NavierStokes.BoundaryAxisJets.localized_descent_eventuallyEq {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {R : ℝ} (hR : 0 < R) (F : ℝ × P → E) (z : P) {X : ℝ} (hX : X ∈ Set.Ico 0 ((R / 4) ^ 2)) : (fun (Y : ℝ) => localized R F (√Y, z)) =ᶠ[nhds X] fun (Y : ℝ) => F (√Y, z)

theorem NavierStokes.BoundaryAxisJets.axisJet_eq_iteratedDerivWithin_local {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {R : ℝ} (hR : 0 < R) {F : ℝ × P → E} {z : P} (hf : ContDiffOn ℝ (↑⊤) (fun (r : ℝ) => F (r, z)) (Set.Ioo (-R) R)) (he : ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) (k : ℕ) {X : ℝ} (hX : X ∈ Set.Ico 0 ((R / 4) ^ 2)) : axisJet F k (X, z) = iteratedDerivWithin k (fun (Y : ℝ) => F (√Y, z)) (Set.Ici 0) X

theorem NavierStokes.BoundaryAxisJets.axisJet_eq_iteratedDeriv_local_pos {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {R : ℝ} (hR : 0 < R) {F : ℝ × P → E} {z : P} (hf : ContDiffOn ℝ (↑⊤) (fun (r : ℝ) => F (r, z)) (Set.Ioo (-R) R)) (he : ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) (k : ℕ) {X : ℝ} (hX : X ∈ Set.Ioo 0 ((R / 4) ^ 2)) : axisJet F k (X, z) = iteratedDeriv k (fun (Y : ℝ) => F (√Y, z)) X

Genuine joint smoothness of the signed radial pullbacks

noncomputable def NavierStokes.BoundaryAxisJets.radialPartial {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : ℝ × P → E) (p : ℝ × P) : E

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

Equations

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

noncomputable def NavierStokes.BoundaryAxisJets.reduceFamily {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : ℝ × P → E) (p : ℝ × P) : E

Reduce family, given by EvenSmoothDescent.radialDerivative (fun r => F (r, p.2)) p.1.

Equations

• NavierStokes.BoundaryAxisJets.reduceFamily F p = NavierStokes.EvenSmoothDescent.radialDerivative (fun (r : ℝ) => F (r, p.2)) p.1

theorem NavierStokes.BoundaryAxisJets.radialPartial_contDiffOn {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup P] [NormedSpace ℝ P] {U : Set P} (hU : IsOpen U) {F : ℝ × P → E} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ U)) : ContDiffOn ℝ (↑⊤) (radialPartial F) (Set.univ ×ˢ U)

theorem NavierStokes.BoundaryAxisJets.reduceFamily_integral {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : ℝ × P → E) (p : ℝ × P) : reduceFamily F p = (1 / 2) • ∫ (t : ℝ) in 0..1, radialPartial (radialPartial F) (t * p.1, p.2)

theorem NavierStokes.BoundaryAxisJets.reduceFamily_contDiffOn {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup P] [NormedSpace ℝ P] [ProperSpace P] {U : Set P} (hU : IsOpen U) {F : ℝ × P → E} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ U)) : ContDiffOn ℝ (↑⊤) (reduceFamily F) (Set.univ ×ˢ U)

theorem NavierStokes.BoundaryAxisJets.radialJet_joint_contDiffOn {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup P] [NormedSpace ℝ P] [ProperSpace P] {U : Set P} (hU : IsOpen U) {F : ℝ × P → E} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ U)) (k : ℕ) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × P) => radialJet F k p.1 p.2) (Set.univ ×ˢ U)

theorem NavierStokes.BoundaryAxisJets.localized_joint_contDiffOn {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup P] [NormedSpace ℝ P] {R : ℝ} (hR : 0 < R) {U : Set P} (hU : IsOpen U) {F : ℝ × P → E} (hF : ContDiffOn ℝ (↑⊤) F (Set.Ioo (-R) R ×ˢ U)) : ContDiffOn ℝ (↑⊤) (localized R F) (Set.univ ×ˢ U)

theorem NavierStokes.BoundaryAxisJets.radialJet_joint_contDiffOn_local {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup P] [NormedSpace ℝ P] [ProperSpace P] {R : ℝ} (hR : 0 < R) {U : Set P} (hU : IsOpen U) {F : ℝ × P → E} (hF : ContDiffOn ℝ (↑⊤) F (Set.Ioo (-R) R ×ˢ U)) (k : ℕ) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × P) => radialJet F k p.1 p.2) (Set.Ioo (-(R / 4)) (R / 4) ×ˢ U)

theorem NavierStokes.BoundaryAxisJets.radialJet_even_local {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {R : ℝ} (hR : 0 < R) {F : ℝ × P → E} {z : P} (he : ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) (k : ℕ) {r : ℝ} (hr : r ∈ Set.Ioo (-(R / 4)) (R / 4)) : radialJet F k (-r) z = radialJet F k r z

theorem NavierStokes.BoundaryAxisJets.axisJet_square_local {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {R : ℝ} (hR : 0 < R) {F : ℝ × P → E} {z : P} (he : ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) (k : ℕ) {r : ℝ} (hr : r ∈ Set.Ioo (-(R / 4)) (R / 4)) : axisJet F k (r ^ 2, z) = radialJet F k r z

theorem NavierStokes.BoundaryAxisJets.axisJet_pullback_contDiffOn_local {E : Type u_1} {P : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup P] [NormedSpace ℝ P] [ProperSpace P] {R : ℝ} (hR : 0 < R) {U : Set P} (hU : IsOpen U) {F : ℝ × P → E} (hF : ContDiffOn ℝ (↑⊤) F (Set.Ioo (-R) R ×ˢ U)) (he : ∀ z ∈ U, ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) (k : ℕ) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × P) => axisJet F k (p.1 ^ 2, p.2)) (Set.Ioo (-(R / 4)) (R / 4) ×ˢ U)

The input needed by positive-order lower sources: every canonical squared-radius jet has a genuinely smooth, even signed radial pullback.

Holomorphy is preserved by the actual radial derivative

theorem NavierStokes.BoundaryAxisJets.radialPartial_holomorphic {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] [CompleteSpace B] {U : Set ℂ} (hU : IsOpen U) {F : ℝ × ℂ → B} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ U)) (hhol : ∀ (r : ℝ), DifferentiableOn ℂ (fun (z : ℂ) => F (r, z)) U) (r : ℝ) : DifferentiableOn ℂ (fun (z : ℂ) => radialPartial F (r, z)) U

The radial difference quotients converge in the supremum norm on every compact parameter disk. The holomorphic limit theorem therefore applies to the genuine radial derivative.

@[reducible, inline]

abbrev NavierStokes.BoundaryAxisJets.Segment : Type

Segment: an abbreviation for ↥(Icc (0 : ℝ) 1).

Equations

• NavierStokes.BoundaryAxisJets.Segment = ↑(Set.Icc 0 1)

noncomputable def NavierStokes.BoundaryAxisJets.segmentExtend {B : Type} [NormedAddCommGroup B] (f : C(Segment, B)) (t : ℝ) : B

Segment extend, given by f (projIcc 0 1 zero_le_one t).

Equations

• NavierStokes.BoundaryAxisJets.segmentExtend f t = f (Set.projIcc 0 1 NavierStokes.BoundaryAxisJets.segmentExtend._proof_1 t)

theorem NavierStokes.BoundaryAxisJets.segmentExtend_continuous {B : Type} [NormedAddCommGroup B] (f : C(Segment, B)) : Continuous (segmentExtend f)

theorem NavierStokes.BoundaryAxisJets.segmentIntegral_norm {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] (f : C(Segment, B)) : ‖∫ (t : ℝ) in 0..1, segmentExtend f t‖ ≤ 1 * ‖f‖

noncomputable def NavierStokes.BoundaryAxisJets.segmentIntegral {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] : C(Segment, B) →L[ℂ] B

Integration of a compact continuous family is complex linear.

Equations

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

theorem NavierStokes.BoundaryAxisJets.intervalIntegral_holomorphic {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] {U : Set ℂ} (hU : IsOpen U) {G : ℂ × ℝ → B} (hG : ContDiffOn ℝ (↑⊤) G (U ×ˢ Set.univ)) (hhol : ∀ (t : ℝ), DifferentiableOn ℂ (fun (z : ℂ) => G (z, t)) U) : DifferentiableOn ℂ (fun (z : ℂ) => ∫ (t : ℝ) in 0..1, G (z, t)) U

theorem NavierStokes.BoundaryAxisJets.reduceFamily_holomorphic {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] [CompleteSpace B] {U : Set ℂ} (hU : IsOpen U) {F : ℝ × ℂ → B} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ U)) (hhol : ∀ (r : ℝ), DifferentiableOn ℂ (fun (z : ℂ) => F (r, z)) U) (r : ℝ) : DifferentiableOn ℂ (fun (z : ℂ) => reduceFamily F (r, z)) U

theorem NavierStokes.BoundaryAxisJets.radialJet_holomorphic {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] [CompleteSpace B] {U : Set ℂ} (hU : IsOpen U) {F : ℝ × ℂ → B} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ U)) (hhol : ∀ (r : ℝ), DifferentiableOn ℂ (fun (z : ℂ) => F (r, z)) U) (k : ℕ) (r : ℝ) : DifferentiableOn ℂ (fun (z : ℂ) => radialJet F k r z) U

theorem NavierStokes.BoundaryAxisJets.localized_holomorphic {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] {R : ℝ} (hR : 0 < R) {U : Set ℂ} {F : ℝ × ℂ → B} (hhol : ∀ r ∈ Set.Ioo (-R) R, DifferentiableOn ℂ (fun (z : ℂ) => F (r, z)) U) (r : ℝ) : DifferentiableOn ℂ (fun (z : ℂ) => localized R F (r, z)) U

theorem NavierStokes.BoundaryAxisJets.radialJet_holomorphic_local {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] [CompleteSpace B] {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) {F : ℝ × ℂ → B} (hF : ContDiffOn ℝ (↑⊤) F (Set.Ioo (-R) R ×ˢ U)) (hhol : ∀ r ∈ Set.Ioo (-R) R, DifferentiableOn ℂ (fun (z : ℂ) => F (r, z)) U) (k : ℕ) {r : ℝ} (hr : r ∈ Set.Ioo (-(R / 4)) (R / 4)) : DifferentiableOn ℂ (fun (z : ℂ) => radialJet F k r z) U

theorem NavierStokes.BoundaryAxisJets.axisJet_pullback_holomorphic_local {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] [CompleteSpace B] {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) {F : ℝ × ℂ → B} (hF : ContDiffOn ℝ (↑⊤) F (Set.Ioo (-R) R ×ˢ U)) (hhol : ∀ r ∈ Set.Ioo (-R) R, DifferentiableOn ℂ (fun (z : ℂ) => F (r, z)) U) (he : ∀ z ∈ U, ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) (k : ℕ) {r : ℝ} (hr : r ∈ Set.Ioo (-(R / 4)) (R / 4)) : DifferentiableOn ℂ (fun (z : ℂ) => axisJet F k (r ^ 2, z)) U

Every canonical right jet has holomorphic parameter slices, including at the axis, under the actual joint-smooth and holomorphic input hypotheses.

Actual mixed parameter jets

noncomputable def NavierStokes.BoundaryAxisJets.complexPartial {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] (F : ℝ × ℂ → B) (p : ℝ × ℂ) : B

Complex partial, given by deriv (fun z => F (p.1, z)) p.2.

Equations

• NavierStokes.BoundaryAxisJets.complexPartial F p = deriv (fun (z : ℂ) => F (p.1, z)) p.2

noncomputable def NavierStokes.BoundaryAxisJets.complexJet {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] (F : ℝ × ℂ → B) (m : ℕ) (p : ℝ × ℂ) : B

Complex jet, given by iteratedDeriv m (fun z => F (p.1, z)) p.2.

Equations

• NavierStokes.BoundaryAxisJets.complexJet F m p = iteratedDeriv m (fun (z : ℂ) => F (p.1, z)) p.2

theorem NavierStokes.BoundaryAxisJets.complexPartial_eq_real_fderiv {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] {U : Set ℂ} (hU : IsOpen U) {F : ℝ × ℂ → B} {r : ℝ} (hhol : DifferentiableOn ℂ (fun (z : ℂ) => F (r, z)) U) {z : ℂ} (hz : z ∈ U) : complexPartial F (r, z) = (fderiv ℝ (fun (z : ℂ) => F (r, z)) z) 1

theorem NavierStokes.BoundaryAxisJets.complexPartial_contDiffOn {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] {S : Set ℝ} {U : Set ℂ} (hS : IsOpen S) (hU : IsOpen U) {F : ℝ × ℂ → B} (hF : ContDiffOn ℝ (↑⊤) F (S ×ˢ U)) (hhol : ∀ r ∈ S, DifferentiableOn ℂ (fun (z : ℂ) => F (r, z)) U) : ContDiffOn ℝ (↑⊤) (complexPartial F) (S ×ˢ U)

theorem NavierStokes.BoundaryAxisJets.complexJet_contDiffOn {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] [CompleteSpace B] {S : Set ℝ} {U : Set ℂ} (hS : IsOpen S) (hU : IsOpen U) {F : ℝ × ℂ → B} (hF : ContDiffOn ℝ (↑⊤) F (S ×ˢ U)) (hhol : ∀ r ∈ S, DifferentiableOn ℂ (fun (z : ℂ) => F (r, z)) U) (m : ℕ) : ContDiffOn ℝ (↑⊤) (complexJet F m) (S ×ˢ U)

noncomputable def NavierStokes.BoundaryAxisJets.mixedAxisJet {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] (F : ℝ × ℂ → B) (k m : ℕ) (p : ℝ × ℂ) : B

Mixed axis jet, given by iteratedDeriv m (fun z => axisJet F k (p.1, z)) p.2.

Equations

• NavierStokes.BoundaryAxisJets.mixedAxisJet F k m p = iteratedDeriv m (fun (z : ℂ) => NavierStokes.BoundaryAxisJets.axisJet F k (p.1, z)) p.2

theorem NavierStokes.BoundaryAxisJets.mixedAxisJet_square_local {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) {F : ℝ × ℂ → B} (he : ∀ z ∈ U, ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) (k m : ℕ) {r : ℝ} (hr : r ∈ Set.Ioo (-(R / 4)) (R / 4)) {z : ℂ} (hz : z ∈ U) : mixedAxisJet F k m (r ^ 2, z) = complexJet (fun (p : ℝ × ℂ) => radialJet F k p.1 p.2) m (r, z)

theorem NavierStokes.BoundaryAxisJets.mixedAxisJet_pullback_contDiffOn_local {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] [CompleteSpace B] {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) {F : ℝ × ℂ → B} (hF : ContDiffOn ℝ (↑⊤) F (Set.Ioo (-R) R ×ˢ U)) (hhol : ∀ r ∈ Set.Ioo (-R) R, DifferentiableOn ℂ (fun (z : ℂ) => F (r, z)) U) (he : ∀ z ∈ U, ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) (k m : ℕ) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => mixedAxisJet F k m (p.1 ^ 2, p.2)) (Set.Ioo (-(R / 4)) (R / 4) ×ˢ U)

Every fixed mixed jet has the genuine joint regularity required of a lower-order source, without any negative-X extension.

theorem NavierStokes.BoundaryAxisJets.mixedAxisJet_pullback_holomorphic_local {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] [CompleteSpace B] {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) {F : ℝ × ℂ → B} (hF : ContDiffOn ℝ (↑⊤) F (Set.Ioo (-R) R ×ˢ U)) (hhol : ∀ r ∈ Set.Ioo (-R) R, DifferentiableOn ℂ (fun (z : ℂ) => F (r, z)) U) (he : ∀ z ∈ U, ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) (k m : ℕ) {r : ℝ} (hr : r ∈ Set.Ioo (-(R / 4)) (R / 4)) : DifferentiableOn ℂ (fun (z : ℂ) => mixedAxisJet F k m (r ^ 2, z)) U

theorem NavierStokes.BoundaryAxisJets.mixedAxisJet_eq_within_local {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] [CompleteSpace B] {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) {F : ℝ × ℂ → B} (hF : ContDiffOn ℝ (↑⊤) F (Set.Ioo (-R) R ×ˢ U)) (he : ∀ z ∈ U, ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) (k m : ℕ) {X : ℝ} (hX : X ∈ Set.Ico 0 ((R / 4) ^ 2)) {z : ℂ} (hz : z ∈ U) : mixedAxisJet F k m (X, z) = iteratedDeriv m (fun (w : ℂ) => iteratedDerivWithin k (fun (Y : ℝ) => F (√Y, w)) (Set.Ici 0) X) z

theorem NavierStokes.BoundaryAxisJets.mixedAxisJet_eq_ordinary_local {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] [CompleteSpace B] {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) {F : ℝ × ℂ → B} (hF : ContDiffOn ℝ (↑⊤) F (Set.Ioo (-R) R ×ˢ U)) (he : ∀ z ∈ U, ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) (k m : ℕ) {X : ℝ} (hX : X ∈ Set.Ioo 0 ((R / 4) ^ 2)) {z : ℂ} (hz : z ∈ U) : mixedAxisJet F k m (X, z) = iteratedDeriv m (fun (w : ℂ) => iteratedDeriv k (fun (Y : ℝ) => F (√Y, w)) X) z

Interior localization retaining the full radial domain

noncomputable def NavierStokes.BoundaryAxisJets.interiorBump {R S : ℝ} (hS : 0 < S) (hSR : S < R) : ContDiffBump 0

Interior bump, bundling rIn, rOut, rIn_pos, rIn_lt_rOut.

Equations

• NavierStokes.BoundaryAxisJets.interiorBump hS hSR = { rIn := S, rOut := (S + R) / 2, rIn_pos := hS, rIn_lt_rOut := ⋯ }

noncomputable def NavierStokes.BoundaryAxisJets.interiorCutoff {R S : ℝ} (hS : 0 < S) (hSR : S < R) (r : ℝ) : ℝ

Interior cutoff, given by interiorBump hS hSR r * interiorBump hS hSR (-r).

Equations

• NavierStokes.BoundaryAxisJets.interiorCutoff hS hSR r = ↑(NavierStokes.BoundaryAxisJets.interiorBump hS hSR) r * ↑(NavierStokes.BoundaryAxisJets.interiorBump hS hSR) (-r)

theorem NavierStokes.BoundaryAxisJets.interiorCutoff_contDiff {R S : ℝ} (hS : 0 < S) (hSR : S < R) : ContDiff ℝ (↑⊤) (interiorCutoff hS hSR)

theorem NavierStokes.BoundaryAxisJets.interiorCutoff_even {R S : ℝ} (hS : 0 < S) (hSR : S < R) : Function.Even (interiorCutoff hS hSR)

theorem NavierStokes.BoundaryAxisJets.interiorCutoff_one {R S r : ℝ} (hS : 0 < S) (hSR : S < R) (hr : |r| ≤ S) : interiorCutoff hS hSR r = 1

theorem NavierStokes.BoundaryAxisJets.interiorCutoff_eventually_zero {R S r : ℝ} (hS : 0 < S) (hSR : S < R) (hr : R ≤ |r|) : interiorCutoff hS hSR =ᶠ[nhds r] fun (x : ℝ) => 0

noncomputable def NavierStokes.BoundaryAxisJets.interiorLocalized {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] {R S : ℝ} (hS : 0 < S) (hSR : S < R) (F : ℝ × ℂ → B) (p : ℝ × ℂ) : B

Interior localized, given by interiorCutoff hS hSR p.1 • F p.

Equations

• NavierStokes.BoundaryAxisJets.interiorLocalized hS hSR F p = NavierStokes.BoundaryAxisJets.interiorCutoff hS hSR p.1 • F p

theorem NavierStokes.BoundaryAxisJets.interiorLocalized_eq {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] {R S r : ℝ} (hS : 0 < S) (hSR : S < R) (hr : |r| ≤ S) (F : ℝ × ℂ → B) (z : ℂ) : interiorLocalized hS hSR F (r, z) = F (r, z)

theorem NavierStokes.BoundaryAxisJets.interiorLocalized_contDiffOn {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] {R S : ℝ} (hS : 0 < S) (hSR : S < R) {U : Set ℂ} (hU : IsOpen U) {F : ℝ × ℂ → B} (hF : ContDiffOn ℝ (↑⊤) F (Set.Ioo (-R) R ×ˢ U)) : ContDiffOn ℝ (↑⊤) (interiorLocalized hS hSR F) (Set.univ ×ˢ U)

theorem NavierStokes.BoundaryAxisJets.interiorLocalized_even {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] {R S : ℝ} (hS : 0 < S) (hSR : S < R) {F : ℝ × ℂ → B} {z : ℂ} (he : ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) : Function.Even fun (r : ℝ) => interiorLocalized hS hSR F (r, z)

theorem NavierStokes.BoundaryAxisJets.interiorLocalized_holomorphic {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] {R S : ℝ} (hS : 0 < S) (hSR : S < R) {U : Set ℂ} {F : ℝ × ℂ → B} (hhol : ∀ r ∈ Set.Ioo (-R) R, DifferentiableOn ℂ (fun (z : ℂ) => F (r, z)) U) (r : ℝ) : DifferentiableOn ℂ (fun (z : ℂ) => interiorLocalized hS hSR F (r, z)) U

theorem NavierStokes.BoundaryAxisJets.radialJet_interiorLocalized_eq {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] {R S : ℝ} (hS : 0 < S) (hSR : S < R) (F : ℝ × ℂ → B) (z : ℂ) (k : ℕ) {r : ℝ} (hr : r ∈ Set.Ioo (-S) S) : radialJet (interiorLocalized hS hSR F) k r z = radialJet F k r z

theorem NavierStokes.BoundaryAxisJets.radialJet_joint_contDiffOn_full {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) {F : ℝ × ℂ → B} (hF : ContDiffOn ℝ (↑⊤) F (Set.Ioo (-R) R ×ˢ U)) (k : ℕ) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => radialJet F k p.1 p.2) (Set.Ioo (-R) R ×ˢ U)

No radial radius is lost: localization is chosen around each interior point while the canonical jet itself remains unchanged.

theorem NavierStokes.BoundaryAxisJets.radialJet_holomorphic_full {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] [CompleteSpace B] {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) {F : ℝ × ℂ → B} (hF : ContDiffOn ℝ (↑⊤) F (Set.Ioo (-R) R ×ˢ U)) (hhol : ∀ r ∈ Set.Ioo (-R) R, DifferentiableOn ℂ (fun (z : ℂ) => F (r, z)) U) (k : ℕ) {r : ℝ} (hr : r ∈ Set.Ioo (-R) R) : DifferentiableOn ℂ (fun (z : ℂ) => radialJet F k r z) U

theorem NavierStokes.BoundaryAxisJets.radialJet_even_full {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] {R : ℝ} (hR : 0 < R) {F : ℝ × ℂ → B} {z : ℂ} (he : ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) (k : ℕ) {r : ℝ} (hr : r ∈ Set.Ioo (-R) R) : radialJet F k (-r) z = radialJet F k r z

theorem NavierStokes.BoundaryAxisJets.axisJet_square_full {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] {R : ℝ} (hR : 0 < R) {F : ℝ × ℂ → B} {z : ℂ} (he : ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) (k : ℕ) {r : ℝ} (hr : r ∈ Set.Ioo (-R) R) : axisJet F k (r ^ 2, z) = radialJet F k r z

theorem NavierStokes.BoundaryAxisJets.axisJet_pullback_contDiffOn_full {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) {F : ℝ × ℂ → B} (hF : ContDiffOn ℝ (↑⊤) F (Set.Ioo (-R) R ×ˢ U)) (he : ∀ z ∈ U, ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) (k : ℕ) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => axisJet F k (p.1 ^ 2, p.2)) (Set.Ioo (-R) R ×ˢ U)

theorem NavierStokes.BoundaryAxisJets.axisJet_pullback_holomorphic_full {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] [CompleteSpace B] {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) {F : ℝ × ℂ → B} (hF : ContDiffOn ℝ (↑⊤) F (Set.Ioo (-R) R ×ˢ U)) (hhol : ∀ r ∈ Set.Ioo (-R) R, DifferentiableOn ℂ (fun (z : ℂ) => F (r, z)) U) (he : ∀ z ∈ U, ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) (k : ℕ) {r : ℝ} (hr : r ∈ Set.Ioo (-R) R) : DifferentiableOn ℂ (fun (z : ℂ) => axisJet F k (r ^ 2, z)) U

theorem NavierStokes.BoundaryAxisJets.axisJet_derivatives_full {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] [CompleteSpace B] {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) {F : ℝ × ℂ → B} (hF : ContDiffOn ℝ (↑⊤) F (Set.Ioo (-R) R ×ˢ U)) (he : ∀ z ∈ U, ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) (k : ℕ) {X : ℝ} (hX : X ∈ Set.Ico 0 (R ^ 2)) {z : ℂ} (hz : z ∈ U) : axisJet F k (X, z) = iteratedDerivWithin k (fun (Y : ℝ) => F (√Y, z)) (Set.Ici 0) X ∧ (0 < X → axisJet F k (X, z) = iteratedDeriv k (fun (Y : ℝ) => F (√Y, z)) X)

theorem NavierStokes.BoundaryAxisJets.axisJet_eq_within_full {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] [CompleteSpace B] {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) {F : ℝ × ℂ → B} (hF : ContDiffOn ℝ (↑⊤) F (Set.Ioo (-R) R ×ˢ U)) (he : ∀ z ∈ U, ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) (k : ℕ) {X : ℝ} (hX : X ∈ Set.Ico 0 (R ^ 2)) {z : ℂ} (hz : z ∈ U) : axisJet F k (X, z) = iteratedDerivWithin k (fun (Y : ℝ) => F (√Y, z)) (Set.Ici 0) X

theorem NavierStokes.BoundaryAxisJets.axisJet_eq_ordinary_full {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] [CompleteSpace B] {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) {F : ℝ × ℂ → B} (hF : ContDiffOn ℝ (↑⊤) F (Set.Ioo (-R) R ×ˢ U)) (he : ∀ z ∈ U, ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) (k : ℕ) {X : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) {z : ℂ} (hz : z ∈ U) : axisJet F k (X, z) = iteratedDeriv k (fun (Y : ℝ) => F (√Y, z)) X

theorem NavierStokes.BoundaryAxisJets.axisJet_zero_full {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] [CompleteSpace B] {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) {F : ℝ × ℂ → B} (hF : ContDiffOn ℝ (↑⊤) F (Set.Ioo (-R) R ×ˢ U)) (he : ∀ z ∈ U, ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) (k : ℕ) {z : ℂ} (hz : z ∈ U) : axisJet F k (0, z) = (↑k.factorial / ↑(2 * k).factorial) • iteratedDeriv (2 * k) (fun (r : ℝ) => F (r, z)) 0

theorem NavierStokes.BoundaryAxisJets.mixedAxisJet_square_full {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) {F : ℝ × ℂ → B} (he : ∀ z ∈ U, ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) (k m : ℕ) {r : ℝ} (hr : r ∈ Set.Ioo (-R) R) {z : ℂ} (hz : z ∈ U) : mixedAxisJet F k m (r ^ 2, z) = complexJet (fun (p : ℝ × ℂ) => radialJet F k p.1 p.2) m (r, z)

theorem NavierStokes.BoundaryAxisJets.mixedAxisJet_pullback_contDiffOn_full {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] [CompleteSpace B] {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) {F : ℝ × ℂ → B} (hF : ContDiffOn ℝ (↑⊤) F (Set.Ioo (-R) R ×ˢ U)) (hhol : ∀ r ∈ Set.Ioo (-R) R, DifferentiableOn ℂ (fun (z : ℂ) => F (r, z)) U) (he : ∀ z ∈ U, ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) (k m : ℕ) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × ℂ) => mixedAxisJet F k m (p.1 ^ 2, p.2)) (Set.Ioo (-R) R ×ˢ U)

theorem NavierStokes.BoundaryAxisJets.mixedAxisJet_pullback_holomorphic_full {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] [CompleteSpace B] {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) {F : ℝ × ℂ → B} (hF : ContDiffOn ℝ (↑⊤) F (Set.Ioo (-R) R ×ˢ U)) (hhol : ∀ r ∈ Set.Ioo (-R) R, DifferentiableOn ℂ (fun (z : ℂ) => F (r, z)) U) (he : ∀ z ∈ U, ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) (k m : ℕ) {r : ℝ} (hr : r ∈ Set.Ioo (-R) R) : DifferentiableOn ℂ (fun (z : ℂ) => mixedAxisJet F k m (r ^ 2, z)) U

theorem NavierStokes.BoundaryAxisJets.mixedAxisJet_eq_within_full {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] [CompleteSpace B] {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) {F : ℝ × ℂ → B} (hF : ContDiffOn ℝ (↑⊤) F (Set.Ioo (-R) R ×ˢ U)) (he : ∀ z ∈ U, ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) (k m : ℕ) {X : ℝ} (hX : X ∈ Set.Ico 0 (R ^ 2)) {z : ℂ} (hz : z ∈ U) : mixedAxisJet F k m (X, z) = iteratedDeriv m (fun (w : ℂ) => iteratedDerivWithin k (fun (Y : ℝ) => F (√Y, w)) (Set.Ici 0) X) z

theorem NavierStokes.BoundaryAxisJets.mixedAxisJet_eq_ordinary_full {B : Type} [NormedAddCommGroup B] [NormedSpace ℂ B] [CompleteSpace B] {R : ℝ} (hR : 0 < R) {U : Set ℂ} (hU : IsOpen U) {F : ℝ × ℂ → B} (hF : ContDiffOn ℝ (↑⊤) F (Set.Ioo (-R) R ×ˢ U)) (he : ∀ z ∈ U, ∀ r ∈ Set.Ioo (-R) R, F (-r, z) = F (r, z)) (k m : ℕ) {X : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) {z : ℂ} (hz : z ∈ U) : mixedAxisJet F k m (X, z) = iteratedDeriv m (fun (w : ℂ) => iteratedDeriv k (fun (Y : ℝ) => F (√Y, w)) X) z