Actual wave identities at closed native-cell points

All derivatives below are ambient derivatives at the selected point. No openness of a quantitative control cell, nor a zero germ at its flat boundary, is required.

theorem NavierStokes.ClosedNativeWaveIdentities.along_germ {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : D → D) {f g : D → E} {x : D} (h : f =ᶠ[nhds x] g) : HarmonicCalculus.along V f x = HarmonicCalculus.along V g x

theorem NavierStokes.ClosedNativeWaveIdentities.contDiffAt_along {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : D → D} {f : D → E} {x : D} (hV : ContDiffAt ℝ (↑⊤) V x) (hf : ContDiffAt ℝ (↑⊤) f x) : ContDiffAt ℝ (↑⊤) (HarmonicCalculus.along V f) x

theorem NavierStokes.ClosedNativeWaveIdentities.eventually_differentiableAt {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : D → E} {x : D} (hf : ContDiffAt ℝ (↑⊤) f x) : ∀ᶠ (y : D) in nhds x, DifferentiableAt ℝ f y

theorem NavierStokes.ClosedNativeWaveIdentities.along_along_mode_at {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {V : D → D} (κ : ℝ) {Φ : D → ℝ} {a : D → ℂ} {x : D} (hV : ContDiffAt ℝ (↑⊤) V x) (hΦ : ContDiffAt ℝ (↑⊤) Φ x) (ha : ContDiffAt ℝ (↑⊤) a x) : HarmonicCalculus.along V (HarmonicCalculus.along V (HarmonicCalculus.mode κ Φ a)) x = (HarmonicCalculus.along V (HarmonicCalculus.along V a) x + 2 * HarmonicCalculus.phaseFactor κ * ↑(HarmonicCalculus.along V Φ x) * HarmonicCalculus.along V a x + (HarmonicCalculus.phaseFactor κ * ↑(HarmonicCalculus.along V (HarmonicCalculus.along V Φ) x) - ↑κ ^ 2 * ↑(HarmonicCalculus.along V Φ x) ^ 2) * a x) * HarmonicCalculus.carrier κ Φ x

theorem NavierStokes.ClosedNativeWaveIdentities.cylindricalLaplacian_mode_at {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) {Vr Vθ Vz : D → D} (κ : ℝ) {Φ : D → ℝ} {a : D → ℂ} {x : D} (hr : ContDiffAt ℝ (↑⊤) Vr x) (hθ : ContDiffAt ℝ (↑⊤) Vθ x) (hz : ContDiffAt ℝ (↑⊤) Vz x) (hΦ : ContDiffAt ℝ (↑⊤) Φ x) (ha : ContDiffAt ℝ (↑⊤) a x) : HarmonicCalculus.cylindricalLaplacian R Vr Vθ Vz (HarmonicCalculus.mode κ Φ a) x = (HarmonicCalculus.cylindricalLaplacian R Vr Vθ Vz a x + 2 * HarmonicCalculus.phaseFactor κ * HarmonicCalculus.phaseCross R Vr Vθ Vz Φ a x + (HarmonicCalculus.phaseFactor κ * ↑(HarmonicCalculus.cylindricalLaplacian R Vr Vθ Vz Φ x) - ↑κ ^ 2 * ↑(‖HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x‖ ^ 2)) * a x) * HarmonicCalculus.carrier κ Φ x

theorem NavierStokes.ClosedNativeWaveIdentities.along_along_const_germ {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : D → D} {f : D → E} {c : E} {x : D} (hf : HarmonicCalculus.along V f =ᶠ[nhds x] fun (x : D) => c) : HarmonicCalculus.along V (HarmonicCalculus.along V f) x = 0

theorem NavierStokes.ClosedNativeWaveIdentities.cylindricalLaplacian_angular_independent_at {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : D → ℝ) (Vr Vθ Vz : D → D) {f : D → E} {x : D} (hf : HarmonicCalculus.along Vθ f =ᶠ[nhds x] fun (x : D) => 0) : HarmonicCalculus.cylindricalLaplacian R Vr Vθ Vz f x = HarmonicCalculus.along Vr (HarmonicCalculus.along Vr f) x + (R x)⁻¹ • HarmonicCalculus.along Vr f x + HarmonicCalculus.along Vz (HarmonicCalculus.along Vz f) x

theorem NavierStokes.ClosedNativeWaveIdentities.cylindricalLaplacian_phase_at {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) (Vr Vθ Vz : D → D) {Φ : D → ℝ} {p : ℝ} {x : D} (hΦθ : HarmonicCalculus.along Vθ Φ =ᶠ[nhds x] fun (x : D) => p) : HarmonicCalculus.cylindricalLaplacian R Vr Vθ Vz Φ x = HarmonicCalculus.along Vr (fun (y : D) => (HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ y).ofLp 0) x + (HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x).ofLp 0 / R x + HarmonicCalculus.along Vz (fun (y : D) => (HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ y).ofLp 2) x

theorem NavierStokes.ClosedNativeWaveIdentities.cylindricalVectorLaplacian_mode_at {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) {Vr Vθ Vz : D → D} (κ : ℝ) {Φ : D → ℝ} {a : D → HarmonicCalculus.ComplexVector} {x : D} (hr : ContDiffAt ℝ (↑⊤) Vr x) (hθ : ContDiffAt ℝ (↑⊤) Vθ x) (hz : ContDiffAt ℝ (↑⊤) Vz x) (hΦ : ContDiffAt ℝ (↑⊤) Φ x) (ha : ∀ (i : Fin 3), ContDiffAt ℝ (↑⊤) (fun (y : D) => a y i) x) : HarmonicCalculus.cylindricalVectorLaplacian R Vr Vθ Vz (HarmonicCalculus.vectorMode κ Φ a) x = fun (i : Fin 3) => (HarmonicCalculus.cylindricalVectorLaplacian R Vr Vθ Vz a x i + 2 * HarmonicCalculus.phaseFactor κ * HarmonicCalculus.phaseCross R Vr Vθ Vz Φ (fun (y : D) => a y i) x + (HarmonicCalculus.phaseFactor κ * ↑(HarmonicCalculus.cylindricalLaplacian R Vr Vθ Vz Φ x) - ↑κ ^ 2 * ↑(‖HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x‖ ^ 2)) * a x i + 2 * HarmonicCalculus.phaseFactor κ * ↑((HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x).ofLp 1 / R x) * HarmonicCalculus.angularGenerator (a x) i) * HarmonicCalculus.carrier κ Φ x

theorem NavierStokes.ClosedNativeWaveIdentities.cylindricalVectorLaplacian_angular_independent_at {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) (Vr Vθ Vz : D → D) {a : D → HarmonicCalculus.ComplexVector} {x : D} (haθ : ∀ (i : Fin 3), (HarmonicCalculus.along Vθ fun (y : D) => a y i) =ᶠ[nhds x] fun (x : D) => 0) : HarmonicCalculus.cylindricalVectorLaplacian R Vr Vθ Vz a x = fun (i : Fin 3) => HarmonicCalculus.along Vr (HarmonicCalculus.along Vr fun (y : D) => a y i) x + (R x)⁻¹ • HarmonicCalculus.along Vr (fun (y : D) => a y i) x + HarmonicCalculus.along Vz (HarmonicCalculus.along Vz fun (y : D) => a y i) x + (R x ^ 2)⁻¹ • HarmonicCalculus.angularGenerator (HarmonicCalculus.angularGenerator (a x)) i

theorem NavierStokes.ClosedNativeWaveIdentities.vectorLaplacian_mode_split_at {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) {Vr Vθ Vz : D → D} (κ : ℝ) {Φ : D → ℝ} {a : D → HarmonicCalculus.ComplexVector} {pθ : ℝ} {x : D} (hr : ContDiffAt ℝ (↑⊤) Vr x) (hθ : ContDiffAt ℝ (↑⊤) Vθ x) (hz : ContDiffAt ℝ (↑⊤) Vz x) (hΦ : ContDiffAt ℝ (↑⊤) Φ x) (ha : ∀ (i : Fin 3), ContDiffAt ℝ (↑⊤) (fun (y : D) => a y i) x) (haθ : ∀ (i : Fin 3), (HarmonicCalculus.along Vθ fun (y : D) => a y i) =ᶠ[nhds x] fun (x : D) => 0) (hΦθ : HarmonicCalculus.along Vθ Φ =ᶠ[nhds x] fun (x : D) => pθ) : HarmonicCalculus.cylindricalVectorLaplacian R Vr Vθ Vz (HarmonicCalculus.vectorMode κ Φ a) x = fun (i : Fin 3) => (LinearWaveResidual.viscousRemainder R Vr Vθ Vz κ Φ a x i - ↑κ ^ 2 * ↑(‖HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x‖ ^ 2) * a x i) * HarmonicCalculus.carrier κ Φ x

theorem NavierStokes.ClosedNativeWaveIdentities.linearResidual_mode_split_at {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (ε κ : ℝ) (R b F G : D → ℝ) {Vr Vθ Vz : D → D} (Vf Vs : D → D) {Φ : D → ℝ} {a : D → HarmonicCalculus.ComplexVector} {p : D → ℂ} {pθ : ℝ} {x : D} (hr : ContDiffAt ℝ (↑⊤) Vr x) (hθ : ContDiffAt ℝ (↑⊤) Vθ x) (hz : ContDiffAt ℝ (↑⊤) Vz x) (hΦ : ContDiffAt ℝ (↑⊤) Φ x) (ha : ∀ (i : Fin 3), ContDiffAt ℝ (↑⊤) (fun (y : D) => a y i) x) (hR : DifferentiableAt ℝ R x) (hb : DifferentiableAt ℝ b x) (hF : DifferentiableAt ℝ F x) (hG : DifferentiableAt ℝ G x) (hRx : R x ≠ 0) (hDr : HarmonicCalculus.along Vr R x = 1) (hBθ : ∀ (i : Fin 3), HarmonicCalculus.along Vθ (fun (y : D) => LinearWaveResidual.base R b F G y i) x = 0) (haθ : ∀ (i : Fin 3), (HarmonicCalculus.along Vθ fun (y : D) => a y i) =ᶠ[nhds x] fun (x : D) => 0) (hΦθ : HarmonicCalculus.along Vθ Φ =ᶠ[nhds x] fun (x : D) => pθ) (hp : DifferentiableAt ℝ p x) (hpθ : HarmonicCalculus.along Vθ p x = 0) : LinearWaveResidual.linearResidual ε R Vr Vθ Vz (LinearWaveResidual.timeDirection ε Vf Vs) (LinearWaveResidual.complexBase R b F G) (HarmonicCalculus.vectorMode κ Φ a) (HarmonicCalculus.mode κ Φ p) x = fun (i : Fin 3) => (LinearWaveResidual.principal ε κ R F G Vr Vθ Vz Vf Φ a p x i + LinearWaveResidual.remainder ε κ R b F G Vr Vθ Vz Vf Vs Φ a p x i) * HarmonicCalculus.carrier κ Φ x

theorem NavierStokes.ClosedNativeWaveIdentities.phaseNormal_contDiffAt {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {R : D → ℝ} {Vr Vθ Vz : D → D} {Φ : D → ℝ} {x : D} (hR : ContDiffAt ℝ (↑⊤) R x) (hRn : R x ≠ 0) (hr : ContDiffAt ℝ (↑⊤) Vr x) (hθ : ContDiffAt ℝ (↑⊤) Vθ x) (hz : ContDiffAt ℝ (↑⊤) Vz x) (hΦ : ContDiffAt ℝ (↑⊤) Φ x) : ContDiffAt ℝ (↑⊤) (HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ) x

theorem NavierStokes.ClosedNativeWaveIdentities.normalCoefficient_contDiffAt {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {N : D → CurlClassBounds.RealVector} {a : D → HarmonicCalculus.ComplexVector} {x : D} (hN : ContDiffAt ℝ (↑⊤) N x) (ha : ContDiffAt ℝ (↑⊤) a x) (hne : N x ≠ 0) : ContDiffAt ℝ (↑⊤) (fun (y : D) => CurlClassBounds.normalCoefficient (N y) (a y)) x

theorem NavierStokes.ClosedNativeWaveIdentities.cylindricalCurl_contDiffAt {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {R : D → ℝ} {Vr Vθ Vz : D → D} {B : D → HarmonicCalculus.ComplexVector} {x : D} (hR : ContDiffAt ℝ (↑⊤) R x) (hRn : R x ≠ 0) (hr : ContDiffAt ℝ (↑⊤) Vr x) (hθ : ContDiffAt ℝ (↑⊤) Vθ x) (hz : ContDiffAt ℝ (↑⊤) Vz x) (hB : ContDiffAt ℝ (↑⊤) B x) : ContDiffAt ℝ (↑⊤) (CurlClassBounds.cylindricalCurl R Vr Vθ Vz B) x

theorem NavierStokes.ClosedNativeWaveIdentities.carrier_contDiffAt {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (K : ℝ) {Φ : D → ℝ} {x : D} (hΦ : ContDiffAt ℝ (↑⊤) Φ x) : ContDiffAt ℝ (↑⊤) (HarmonicCalculus.carrier K Φ) x

theorem NavierStokes.ClosedNativeWaveIdentities.vectorMode_contDiffAt {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (K : ℝ) {Φ : D → ℝ} {a : D → HarmonicCalculus.ComplexVector} {x : D} (hΦ : ContDiffAt ℝ (↑⊤) Φ x) (ha : ContDiffAt ℝ (↑⊤) a x) : ContDiffAt ℝ (↑⊤) (HarmonicCalculus.vectorMode K Φ a) x

theorem NavierStokes.ClosedNativeWaveIdentities.vectorPotential_contDiffAt {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (K : ℝ) {R : D → ℝ} {Vr Vθ Vz : D → D} {Φ : D → ℝ} {a : D → HarmonicCalculus.ComplexVector} {x : D} (hR : ContDiffAt ℝ (↑⊤) R x) (hRn : R x ≠ 0) (hr : ContDiffAt ℝ (↑⊤) Vr x) (hθ : ContDiffAt ℝ (↑⊤) Vθ x) (hz : ContDiffAt ℝ (↑⊤) Vz x) (hΦ : ContDiffAt ℝ (↑⊤) Φ x) (ha : ContDiffAt ℝ (↑⊤) a x) (hn : HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x ≠ 0) : ContDiffAt ℝ (↑⊤) (CurlClassBounds.vectorPotential K R Vr Vθ Vz Φ a) x

theorem NavierStokes.ClosedNativeWaveIdentities.curlRemainder_contDiffAt {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (K : ℝ) {R : D → ℝ} {Vr Vθ Vz : D → D} {B : D → HarmonicCalculus.ComplexVector} {x : D} (hR : ContDiffAt ℝ (↑⊤) R x) (hRn : R x ≠ 0) (hr : ContDiffAt ℝ (↑⊤) Vr x) (hθ : ContDiffAt ℝ (↑⊤) Vθ x) (hz : ContDiffAt ℝ (↑⊤) Vz x) (hB : ContDiffAt ℝ (↑⊤) B x) : ContDiffAt ℝ (↑⊤) (CurlClassBounds.curlRemainder K R Vr Vθ Vz B) x

theorem NavierStokes.ClosedNativeWaveIdentities.realizedCoefficient_contDiffAt {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (K : ℝ) {R : D → ℝ} {Vr Vθ Vz : D → D} {Φ : D → ℝ} {a : D → HarmonicCalculus.ComplexVector} {x : D} (hR : ContDiffAt ℝ (↑⊤) R x) (hRn : R x ≠ 0) (hr : ContDiffAt ℝ (↑⊤) Vr x) (hθ : ContDiffAt ℝ (↑⊤) Vθ x) (hz : ContDiffAt ℝ (↑⊤) Vz x) (hΦ : ContDiffAt ℝ (↑⊤) Φ x) (ha : ContDiffAt ℝ (↑⊤) a x) (hn : HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x ≠ 0) : ContDiffAt ℝ (↑⊤) (CurlClassBounds.realizedCoefficient K R Vr Vθ Vz Φ a) x

theorem NavierStokes.ClosedNativeWaveIdentities.cylindricalCurl_vectorPotential_of_differentiable {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) (Vr Vθ Vz : D → D) {K : ℝ} (hK : K ≠ 0) {Φ : D → ℝ} {a : D → HarmonicCalculus.ComplexVector} {x : D} (hΦ : DifferentiableAt ℝ Φ x) (hB : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => CurlClassBounds.coefficient R Vr Vθ Vz Φ a y i) x) (hn : HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x ≠ 0) (ht : HarmonicCalculus.normalDot (HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x) (a x) = 0) : CurlClassBounds.cylindricalCurl R Vr Vθ Vz (CurlClassBounds.vectorPotential K R Vr Vθ Vz Φ a) x = HarmonicCalculus.vectorMode K Φ (CurlClassBounds.realizedCoefficient K R Vr Vθ Vz Φ a) x

Curl realization itself uses the first coefficient derivatives and tangency at the selected point, with no surrounding geometric identities.

theorem NavierStokes.ClosedNativeWaveIdentities.cylindricalCurl_vectorPotential_at {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {K : ℝ} (hK : K ≠ 0) {R : D → ℝ} {Vr Vθ Vz : D → D} {Φ : D → ℝ} {a : D → HarmonicCalculus.ComplexVector} {x : D} (hR : ContDiffAt ℝ (↑⊤) R x) (hRn : R x ≠ 0) (hr : ContDiffAt ℝ (↑⊤) Vr x) (hθ : ContDiffAt ℝ (↑⊤) Vθ x) (hz : ContDiffAt ℝ (↑⊤) Vz x) (hΦ : ContDiffAt ℝ (↑⊤) Φ x) (ha : ContDiffAt ℝ (↑⊤) a x) (hn : HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x ≠ 0) (ht : HarmonicCalculus.normalDot (HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x) (a x) = 0) : CurlClassBounds.cylindricalCurl R Vr Vθ Vz (CurlClassBounds.vectorPotential K R Vr Vθ Vz Φ a) x = HarmonicCalculus.vectorMode K Φ (CurlClassBounds.realizedCoefficient K R Vr Vθ Vz Φ a) x

theorem NavierStokes.ClosedNativeWaveIdentities.cylindricalCurl_vectorPotential_germ {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {K : ℝ} (hK : K ≠ 0) {R : D → ℝ} {Vr Vθ Vz : D → D} {Φ : D → ℝ} {a : D → HarmonicCalculus.ComplexVector} {x : D} (hR : ContDiffAt ℝ (↑⊤) R x) (hRn : R x ≠ 0) (hr : ContDiffAt ℝ (↑⊤) Vr x) (hθ : ContDiffAt ℝ (↑⊤) Vθ x) (hz : ContDiffAt ℝ (↑⊤) Vz x) (hΦ : ContDiffAt ℝ (↑⊤) Φ x) (ha : ContDiffAt ℝ (↑⊤) a x) (hn : HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x ≠ 0) (ht : (fun (y : D) => HarmonicCalculus.normalDot (HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ y) (a y)) =ᶠ[nhds x] fun (x : D) => 0) : CurlClassBounds.cylindricalCurl R Vr Vθ Vz (CurlClassBounds.vectorPotential K R Vr Vθ Vz Φ a) =ᶠ[nhds x] HarmonicCalculus.vectorMode K Φ (CurlClassBounds.realizedCoefficient K R Vr Vθ Vz Φ a)

structure NavierStokes.ClosedNativeWaveIdentities.GeometryAt {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) (Vr Vθ Vz : D → D) (x : D) : Prop

The actual cylindrical frame identities at one ambient point.

• radius_smooth : ContDiffAt ℝ (↑⊤) R x
• radius_ne : R x ≠ 0
• radial_smooth : ContDiffAt ℝ (↑⊤) Vr x
• angular_smooth : ContDiffAt ℝ (↑⊤) Vθ x
• axial_smooth : ContDiffAt ℝ (↑⊤) Vz x
• radial_radius : HarmonicCalculus.along Vr R x = 1
• angular_radius : HarmonicCalculus.along Vθ R x = 0
• axial_radius : HarmonicCalculus.along Vz R x = 0
• radial_angular : (fderiv ℝ Vθ x) (Vr x) = (fderiv ℝ Vr x) (Vθ x)
• radial_axial : (fderiv ℝ Vz x) (Vr x) = (fderiv ℝ Vr x) (Vz x)
• angular_axial : (fderiv ℝ Vz x) (Vθ x) = (fderiv ℝ Vθ x) (Vz x)

theorem NavierStokes.ClosedNativeWaveIdentities.divergence_curl_zero_at {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {R : D → ℝ} {Vr Vθ Vz : D → D} {x : D} (G : GeometryAt R Vr Vθ Vz x) {B : D → HarmonicCalculus.ComplexVector} (hB : ContDiffAt ℝ (↑⊤) B x) : HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz (CurlClassBounds.cylindricalCurl R Vr Vθ Vz B) x = 0

theorem NavierStokes.ClosedNativeWaveIdentities.cylindricalDivergence_germ {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {R : D → ℝ} {Vr Vθ Vz : D → D} {a b : D → HarmonicCalculus.ComplexVector} {x : D} (h : a =ᶠ[nhds x] b) : HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz a x = HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz b x

theorem NavierStokes.ClosedNativeWaveIdentities.realizedCoefficient_divergence_at {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {K : ℝ} (hK : K ≠ 0) {R : D → ℝ} {Vr Vθ Vz : D → D} {Φ : D → ℝ} {a : D → HarmonicCalculus.ComplexVector} {x : D} (G : GeometryAt R Vr Vθ Vz x) (hΦ : ContDiffAt ℝ (↑⊤) Φ x) (ha : ContDiffAt ℝ (↑⊤) a x) (hn : HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x ≠ 0) (ht : (fun (y : D) => HarmonicCalculus.normalDot (HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ y) (a y)) =ᶠ[nhds x] fun (x : D) => 0) : HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz (HarmonicCalculus.vectorMode K Φ (CurlClassBounds.realizedCoefficient K R Vr Vθ Vz Φ a)) x = 0

theorem NavierStokes.ClosedNativeWaveIdentities.cylindricalDivergence_contDiffAt {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {R : D → ℝ} {Vr Vθ Vz : D → D} {a : D → HarmonicCalculus.ComplexVector} {x : D} (hR : ContDiffAt ℝ (↑⊤) R x) (hRn : R x ≠ 0) (hr : ContDiffAt ℝ (↑⊤) Vr x) (hθ : ContDiffAt ℝ (↑⊤) Vθ x) (hz : ContDiffAt ℝ (↑⊤) Vz x) (ha : ContDiffAt ℝ (↑⊤) a x) : ContDiffAt ℝ (↑⊤) (HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz a) x

theorem NavierStokes.ClosedNativeWaveIdentities.eq_zero_of_mem_closure {D : Type} [NormedAddCommGroup D] {E : Type u_1} [NormedAddCommGroup E] {f : D → E} {C : Set D} {x : D} (hf : ContinuousAt f x) (hx : x ∈ closure C) (hzero : Set.EqOn f (fun (x : D) => 0) C) : f x = 0

theorem NavierStokes.ClosedNativeWaveIdentities.realizedCoefficient_divergence_of_mem_closure_interior {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {K : ℝ} (hK : K ≠ 0) {R : D → ℝ} {Vr Vθ Vz : D → D} {Φ : D → ℝ} {a : D → HarmonicCalculus.ComplexVector} {C : Set D} {x : D} (hG : ∀ y ∈ C, GeometryAt R Vr Vθ Vz y) (hΦ : ∀ y ∈ C, ContDiffAt ℝ (↑⊤) Φ y) (ha : ∀ y ∈ C, ContDiffAt ℝ (↑⊤) a y) (hn : ∀ y ∈ C, HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ y ≠ 0) (ht : ∀ y ∈ C, HarmonicCalculus.normalDot (HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ y) (a y) = 0) (hx : x ∈ C) (hclosure : x ∈ closure (interior C)) : HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz (HarmonicCalculus.vectorMode K Φ (CurlClassBounds.realizedCoefficient K R Vr Vθ Vz Φ a)) x = 0

A second legitimate boundary interface: tangency on a set whose interior approaches the selected point. Continuity of the actual divergence is derived from the supplied ambient jets.

Literal cutoff/curl residual from primitive pointwise data

structure NavierStokes.ClosedNativeWaveIdentities.ExactAt {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : LinearWaveBounds.WaveCoefficients D) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (n : ℕ) (x : D) : Prop

Exact at data, collecting radial_profile, phase, amplitude, radius, radial_base, frequency_base and their compatibility conditions.

• radial_profile : ContDiffAt ℝ (↑⊤) d.radialProfile x
• phase : ContDiffAt ℝ (↑⊤) (a.phase n) x
• amplitude (j : Fin 3) : ContDiffAt ℝ (↑⊤) (fun (y : D) => a.amplitude n y j) x
• radius : DifferentiableAt ℝ (a.radius n) x
• radial_base : DifferentiableAt ℝ (a.radialBase n) x
• frequency_base : DifferentiableAt ℝ (a.frequencyBase n) x
• axial_base : DifferentiableAt ℝ (a.axialBase n) x
• pressure : DifferentiableAt ℝ (a.pressure n) x
• radius_nonzero : a.radius n x ≠ 0
• radial_radius : HarmonicCalculus.along (d.radialField n) (a.radius n) x = 1
• base_angular (j : Fin 3) : HarmonicCalculus.along (fun (x : D) => d.angular) (fun (y : D) => LinearWaveResidual.base (a.radius n) (a.radialBase n) (a.frequencyBase n) (a.axialBase n) y j) x = 0
• amplitude_angular (j : Fin 3) : (HarmonicCalculus.along (fun (x : D) => d.angular) fun (y : D) => a.amplitude n y j) =ᶠ[nhds x] fun (x : D) => 0
• phase_angular : ∃ (p : ℝ), HarmonicCalculus.along (fun (x : D) => d.angular) (a.phase n) =ᶠ[nhds x] fun (x : D) => p
• pressure_angular : HarmonicCalculus.along (fun (x : D) => d.angular) (a.pressure n) x = 0

theorem NavierStokes.ClosedNativeWaveIdentities.harmonicResidual_eq_at {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {a : LinearWaveBounds.WaveCoefficients D} {s : WeightedClasses.StripData D} {d : LinearWaveBounds.GraphDirections D} {n : ℕ} {x : D} (h : ExactAt a s d n x) : a.harmonicResidual s d n x = fun (j : Fin 3) => (a.principal s d n x j + a.remainder s d n x j) * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x

theorem NavierStokes.ClosedNativeWaveIdentities.harmonicResidual_eq_good_add_excluded_at {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : LinearWaveBounds.WaveCoefficients D) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (ψ : ℕ → D → ℝ) (f source : ℕ → D → HarmonicCalculus.ComplexVector) (n : ℕ) (x : D) (h : ExactAt ((a.withCutoff ψ).addAmplitude f) s d n x) (ha : ∀ (j : Fin 3), DifferentiableAt ℝ (fun (y : D) => a.amplitude n y j) x) (hψ : DifferentiableAt ℝ (ψ n) x) (hf : ∀ (j : Fin 3), DifferentiableAt ℝ (fun (y : D) => f n y j) x) (hsolve : a.principal s d n x = -source n x) : (((a.withCutoff ψ).addAmplitude f).harmonicResidual s d n x + fun (j : Fin 3) => source n x j * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x) = fun (j : Fin 3) => (a.goodCoefficient s d ψ f n x j + LinearWaveBounds.excludedSlotError d ψ a.amplitude source n x j) * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x

structure NavierStokes.ClosedNativeWaveIdentities.AngularData {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : LinearWaveBounds.WaveCoefficients D) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (ψ : ℕ → D → ℝ) (n : ℕ) : Prop

These are symmetries of the uncorrected input fields.

• radius : CopyAngularInvariance.Invariant d.angular (a.radius n)
• radial_base : CopyAngularInvariance.Invariant d.angular (a.radialBase n)
• frequency_base : CopyAngularInvariance.Invariant d.angular (a.frequencyBase n)
• axial_base : CopyAngularInvariance.Invariant d.angular (a.axialBase n)
• radial_field : CopyAngularInvariance.Invariant d.angular (d.radialField n)
• phase : ∃ (p : ℝ), CopyAngularInvariance.AffinePhase d.angular p (a.phase n)
• amplitude : CopyAngularInvariance.Invariant d.angular (a.amplitude n)
• pressure : CopyAngularInvariance.Invariant d.angular (a.pressure n)
• cutoff : CopyAngularInvariance.Invariant d.angular (ψ n)

structure NavierStokes.ClosedNativeWaveIdentities.RawJetsAt {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : LinearWaveBounds.WaveCoefficients D) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (ψ : ℕ → D → ℝ) (n : ℕ) (x : D) : Prop

Only actual input jets and pointwise nondegeneracy enter this record.

• radial_profile : ContDiffAt ℝ (↑⊤) d.radialProfile x
• phase : ContDiffAt ℝ (↑⊤) (a.phase n) x
• radius : ContDiffAt ℝ (↑⊤) (a.radius n) x
• radial_base : DifferentiableAt ℝ (a.radialBase n) x
• frequency_base : DifferentiableAt ℝ (a.frequencyBase n) x
• axial_base : DifferentiableAt ℝ (a.axialBase n) x
• amplitude : ContDiffAt ℝ (↑⊤) (a.amplitude n) x
• pressure : DifferentiableAt ℝ (a.pressure n) x
• cutoff : ContDiffAt ℝ (↑⊤) (ψ n) x
• radius_ne : a.radius n x ≠ 0
• normal_ne : a.normal s d n x ≠ 0

theorem NavierStokes.ClosedNativeWaveIdentities.RawJetsAt.radial_field {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {a : LinearWaveBounds.WaveCoefficients D} {s : WeightedClasses.StripData D} {d : LinearWaveBounds.GraphDirections D} {ψ : ℕ → D → ℝ} {n : ℕ} {x : D} (h : RawJetsAt a s d ψ n x) : ContDiffAt ℝ (↑⊤) (d.radialField n) x

theorem NavierStokes.ClosedNativeWaveIdentities.RawJetsAt.curlCorrection {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {a : LinearWaveBounds.WaveCoefficients D} {s : WeightedClasses.StripData D} {d : LinearWaveBounds.GraphDirections D} {ψ : ℕ → D → ℝ} {n : ℕ} {x : D} (h : RawJetsAt a s d ψ n x) : ContDiffAt ℝ (↑⊤) ((a.withCutoff ψ).curlCorrection s d n) x

theorem NavierStokes.ClosedNativeWaveIdentities.RawJetsAt.corrected_amplitude {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {a : LinearWaveBounds.WaveCoefficients D} {s : WeightedClasses.StripData D} {d : LinearWaveBounds.GraphDirections D} {ψ : ℕ → D → ℝ} {n : ℕ} {x : D} (h : RawJetsAt a s d ψ n x) : ContDiffAt ℝ (↑⊤) ((a.corrected s d ψ).amplitude n) x

theorem NavierStokes.ClosedNativeWaveIdentities.RawJetsAt.corrected_exact {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {a : LinearWaveBounds.WaveCoefficients D} {s : WeightedClasses.StripData D} {d : LinearWaveBounds.GraphDirections D} {ψ : ℕ → D → ℝ} {n : ℕ} {x : D} (h : RawJetsAt a s d ψ n x) (g : AngularData a s d ψ n) (hDr : HarmonicCalculus.along (d.radialField n) (a.radius n) x = 1) : ExactAt (a.corrected s d ψ) s d n x

theorem NavierStokes.ClosedNativeWaveIdentities.RawJetsAt.cancellation {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {a : LinearWaveBounds.WaveCoefficients D} {s : WeightedClasses.StripData D} {d : LinearWaveBounds.GraphDirections D} {ψ : ℕ → D → ℝ} {n : ℕ} {x : D} (h : RawJetsAt a s d ψ n x) (g : AngularData a s d ψ n) (hDr : HarmonicCalculus.along (d.radialField n) (a.radius n) x = 1) (source : ℕ → D → HarmonicCalculus.ComplexVector) (hsolve : a.principal s d n x = -source n x) : ((a.corrected s d ψ).harmonicResidual s d n x + fun (j : Fin 3) => source n x j * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x) = fun (j : Fin 3) => (a.constructedGood s d ψ n x j + LinearWaveBounds.excludedSlotError d ψ a.amplitude source n x j) * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x

theorem NavierStokes.ClosedNativeWaveIdentities.rawJets_of_localInput {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type} {a : PeriodizedWaveBounds.CopyData D I} {s : WeightedClasses.StripData D} {d : LinearWaveBounds.GraphDirections D} {C : ℕ → I → Set D} {P : ℕ → I → D → ℝ} {α κ : ℝ} (h : LocalizedWaveBounds.InputBounds s C P α κ d (LocalizedWaveBounds.rawFamily a)) (hψ : LocalizedWaveBounds.LocalUnweighted s C 0 a.cutoff) (n : ℕ) (i : I) {x : D} (hx : x ∈ s.domain) (hi : x ∈ C n i) (hΦ : ContDiffAt ℝ (↑⊤) (a.background.phase n) x) (hR : a.background.radius n x ≠ 0) (hN : a.background.normal s d n x ≠ 0) : RawJetsAt (a.raw i) s d (fun (n : ℕ) => a.cutoff n i) n x

theorem NavierStokes.ClosedNativeWaveIdentities.native_cancellation_of_principal {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type} {a : PeriodizedWaveBounds.CopyData D I} {s : WeightedClasses.StripData D} {d : LinearWaveBounds.GraphDirections D} {C : ℕ → I → Set D} {P : ℕ → I → D → ℝ} {α κ : ℝ} (h : LocalizedWaveBounds.InputBounds s C P α κ d (LocalizedWaveBounds.rawFamily a)) (hψ : LocalizedWaveBounds.LocalUnweighted s C 0 a.cutoff) (n : ℕ) (i : I) {x : D} (hx : x ∈ s.domain) (hi : x ∈ C n i) (hΦ : ContDiffAt ℝ (↑⊤) (a.background.phase n) x) (hR : a.background.radius n x ≠ 0) (hN : a.background.normal s d n x ≠ 0) (g : AngularData (a.raw i) s d (fun (n : ℕ) => a.cutoff n i) n) (hDr : HarmonicCalculus.along (d.radialField n) (a.background.radius n) x = 1) (hsolve : (a.raw i).principal s d n x = -a.source n x) : ((a.corrected s d i).harmonicResidual s d n x + fun (j : Fin 3) => a.source n x j * HarmonicCalculus.carrier (a.background.frequency n) (a.background.phase n) x) = fun (j : Fin 3) => (a.localGood s d n i x j + a.localGaussian d n i x j) * HarmonicCalculus.carrier (a.background.frequency n) (a.background.phase n) x

theorem NavierStokes.ClosedNativeWaveIdentities.native_realizes_curl_at {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type} {a : PeriodizedWaveBounds.CopyData D I} {s : WeightedClasses.StripData D} {d : LinearWaveBounds.GraphDirections D} (n : ℕ) (i : I) (x : D) (h : RawJetsAt (a.raw i) s d (fun (n : ℕ) => a.cutoff n i) n x) (hK : a.background.frequency n ≠ 0) (ht : HarmonicCalculus.normalDot (a.background.normal s d n x) (a.amplitude n i x) = 0) : CurlClassBounds.cylindricalCurl (a.background.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n) ((a.localized i).curlPotential s d n) x = HarmonicCalculus.vectorMode (a.background.frequency n) (a.background.phase n) ((a.corrected s d i).amplitude n) x

theorem NavierStokes.ClosedNativeWaveIdentities.native_divergence_zero_at {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type} {a : PeriodizedWaveBounds.CopyData D I} {s : WeightedClasses.StripData D} {d : LinearWaveBounds.GraphDirections D} (n : ℕ) (i : I) (x : D) (h : RawJetsAt (a.raw i) s d (fun (n : ℕ) => a.cutoff n i) n x) (G : GeometryAt (a.background.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n) x) (hK : a.background.frequency n ≠ 0) (ht : (fun (y : D) => HarmonicCalculus.normalDot (a.background.normal s d n y) (a.amplitude n i y)) =ᶠ[nhds x] fun (x : D) => 0) : HarmonicCalculus.cylindricalDivergence (a.background.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n) (HarmonicCalculus.vectorMode (a.background.frequency n) (a.background.phase n) ((a.corrected s d i).amplitude n)) x = 0