Finite harmonic extraction of the actual cylindrical residual

The coefficient operations below reconstruct genuine differential fields. Excluded errors remain explicit inputs with field-evaluation witnesses.

@[reducible, inline]

abbrev NavierStokes.HarmonicResidual.Coefficients (D : Type) : Type

Coefficients: an abbreviation for HarmonicFields.Coefficients D.

Equations

• NavierStokes.HarmonicResidual.Coefficients D = NavierStokes.HarmonicFields.Coefficients D

@[reducible, inline]

abbrev NavierStokes.HarmonicResidual.VectorCoefficients (D : Type) : Type

Vector coefficients: an abbreviation for Fin 3 → Coefficients D.

Equations

• NavierStokes.HarmonicResidual.VectorCoefficients D = (Fin 3 → NavierStokes.HarmonicResidual.Coefficients D)

noncomputable def NavierStokes.HarmonicResidual.liftDomain {D : Type} (U : Set D) : Set (D × ℝ)

Lift domain, given by U ×ˢ univ.

Equations

• NavierStokes.HarmonicResidual.liftDomain U = U ×ˢ Set.univ

theorem NavierStokes.HarmonicResidual.liftDomain_open {D : Type} [NormedAddCommGroup D] {U : Set D} (hU : IsOpen U) : IsOpen (liftDomain U)

noncomputable def NavierStokes.HarmonicResidual.liftDirection {D : Type} (V : D → D) (p : D × ℝ) : D × ℝ

Lift direction, given by (V p.1, 0).

Equations

• NavierStokes.HarmonicResidual.liftDirection V p = (V p.1, 0)

noncomputable def NavierStokes.HarmonicResidual.angularDirection {D : Type} [NormedAddCommGroup D] (_p : D × ℝ) : D × ℝ

Angular direction, given by (0, 1).

Equations

• NavierStokes.HarmonicResidual.angularDirection _p = (0, 1)

def NavierStokes.HarmonicResidual.SmoothCoefficients {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (U : Set D) (c : Coefficients D) : Prop

Smoothness is required of actual coefficient functions.

Equations

• NavierStokes.HarmonicResidual.SmoothCoefficients U c = ∀ (j : ℤ), ContDiffOn ℝ (↑⊤) (c.coeff j) U

theorem NavierStokes.HarmonicResidual.smoothCoefficients_zero {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (U : Set D) : SmoothCoefficients U 0

theorem NavierStokes.HarmonicResidual.SmoothCoefficients.add {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c d : Coefficients D} (hc : SmoothCoefficients U c) (hd : SmoothCoefficients U d) : SmoothCoefficients U (c + d)

theorem NavierStokes.HarmonicResidual.SmoothCoefficients.neg {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : Coefficients D} (hc : SmoothCoefficients U c) : SmoothCoefficients U (-c)

theorem NavierStokes.HarmonicResidual.SmoothCoefficients.sub {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c d : Coefficients D} (hc : SmoothCoefficients U c) (hd : SmoothCoefficients U d) : SmoothCoefficients U (c - d)

theorem NavierStokes.HarmonicResidual.SmoothCoefficients.mul {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c d : Coefficients D} (hc : SmoothCoefficients U c) (hd : SmoothCoefficients U d) : SmoothCoefficients U (c * d)

theorem NavierStokes.HarmonicResidual.smoothCoefficients_constant {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {f : D → ℂ} (hf : ContDiffOn ℝ (↑⊤) f U) : SmoothCoefficients U (HarmonicFields.constantCoefficient f)

theorem NavierStokes.HarmonicResidual.SmoothCoefficients.differentiate {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) {V : D → D} {Φ : D → ℝ} (hV : ContDiffOn ℝ (↑⊤) V U) (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (k : ℝ) {c : Coefficients D} (hc : SmoothCoefficients U c) : SmoothCoefficients U (HarmonicFields.differentiate V k Φ c)

theorem NavierStokes.HarmonicResidual.SmoothCoefficients.angular {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : Coefficients D} (hc : SmoothCoefficients U c) (kp : ℤ) : SmoothCoefficients U (HarmonicFields.angularDifferentiate kp c)

@[simp]

theorem NavierStokes.HarmonicResidual.field_add {D : Type} (c d : Coefficients D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (p : D × ℝ) : HarmonicFields.field (c + d) k Φ kp p = HarmonicFields.field c k Φ kp p + HarmonicFields.field d k Φ kp p

@[simp]

theorem NavierStokes.HarmonicResidual.field_zero {D : Type} (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (p : D × ℝ) : HarmonicFields.field 0 k Φ kp p = 0

@[simp]

theorem NavierStokes.HarmonicResidual.field_neg {D : Type} (c : Coefficients D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (p : D × ℝ) : HarmonicFields.field (-c) k Φ kp p = -HarmonicFields.field c k Φ kp p

@[simp]

theorem NavierStokes.HarmonicResidual.field_sub {D : Type} (c d : Coefficients D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (p : D × ℝ) : HarmonicFields.field (c - d) k Φ kp p = HarmonicFields.field c k Φ kp p - HarmonicFields.field d k Φ kp p

@[simp]

theorem NavierStokes.HarmonicResidual.field_constant {D : Type} (f : D → ℂ) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (p : D × ℝ) : HarmonicFields.field (HarmonicFields.constantCoefficient f) k Φ kp p = f p.1

theorem NavierStokes.HarmonicResidual.field_smoothOn {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : Coefficients D} (hc : SmoothCoefficients U c) {Φ : D → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (k : ℝ) (kp : ℤ) : ContDiffOn ℝ (↑⊤) (HarmonicFields.field c k Φ kp) (liftDomain U)

theorem NavierStokes.HarmonicResidual.along_liftDirection {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {f : D × ℝ → ℂ} {x : D} {θ : ℝ} (hf : DifferentiableAt ℝ f (x, θ)) (V : D → D) : HarmonicCalculus.along (liftDirection V) f (x, θ) = HarmonicCalculus.along V (fun (y : D) => f (y, θ)) x

theorem NavierStokes.HarmonicResidual.along_angularDirection {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {f : D × ℝ → ℂ} {x : D} {θ : ℝ} (hf : DifferentiableAt ℝ f (x, θ)) : HarmonicCalculus.along angularDirection f (x, θ) = deriv (fun (t : ℝ) => f (x, t)) θ

theorem NavierStokes.HarmonicResidual.field_differentiate {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) {c : Coefficients D} (hc : SmoothCoefficients U c) {Φ : D → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (V : D → D) (k : ℝ) (kp : ℤ) {p : D × ℝ} (hp : p ∈ liftDomain U) : HarmonicFields.field (HarmonicFields.differentiate V k Φ c) k Φ kp p = HarmonicCalculus.along (liftDirection V) (HarmonicFields.field c k Φ kp) p

theorem NavierStokes.HarmonicResidual.field_angularDifferentiate {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) {c : Coefficients D} (hc : SmoothCoefficients U c) {Φ : D → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (k : ℝ) (kp : ℤ) {p : D × ℝ} (hp : p ∈ liftDomain U) : HarmonicFields.field (HarmonicFields.angularDifferentiate kp c) k Φ kp p = HarmonicCalculus.along angularDirection (HarmonicFields.field c k Φ kp) p

structure NavierStokes.HarmonicResidual.Frame (D : Type) : Type

The directions and the cylindrical radius of one normalized graph.

• radius : D → ℝ

  Radius of Frame, of type D → ℝ.

• radial : D → D

  Radial of Frame, of type D → D.

• axial : D → D

  Axial of Frame, of type D → D.

• time : D → D

  Time of Frame, of type D → D.

• viscosity : ℝ

  Viscosity of Frame, of type ℝ.

noncomputable def NavierStokes.HarmonicResidual.vectorField {D : Type} (a : VectorCoefficients D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (p : D × ℝ) : HarmonicCalculus.ComplexVector

Vector field, defined pointwise by field (a i) k Φ kp p.

Equations

• NavierStokes.HarmonicResidual.vectorField a k Φ kp p i = NavierStokes.HarmonicFields.field (a i) k Φ kp p

noncomputable def NavierStokes.HarmonicResidual.rotate {D : Type} (a : VectorCoefficients D) : VectorCoefficients D

Rotate, given by ![-a 1, a 0, 0].

Equations

• NavierStokes.HarmonicResidual.rotate a = ![-a 1, a 0, 0]

@[simp]

theorem NavierStokes.HarmonicResidual.vectorField_rotate {D : Type} (a : VectorCoefficients D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (p : D × ℝ) : vectorField (rotate a) k Φ kp p = HarmonicCalculus.angularGenerator (vectorField a k Φ kp p)

noncomputable def NavierStokes.HarmonicResidual.scalarLaplacian {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (c : Coefficients D) : Coefficients D

Scalar laplacian, constructed using differentiate.

Equations

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

noncomputable def NavierStokes.HarmonicResidual.vectorLaplacian {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (a : VectorCoefficients D) : VectorCoefficients D

Vector laplacian as an element of VectorCoefficients D.

Equations

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

noncomputable def NavierStokes.HarmonicResidual.transport {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (a b : VectorCoefficients D) : VectorCoefficients D

Transport as an element of VectorCoefficients D.

Equations

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

noncomputable def NavierStokes.HarmonicResidual.gradient {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (p : Coefficients D) : VectorCoefficients D

Gradient as an element of VectorCoefficients D.

Equations

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

noncomputable def NavierStokes.HarmonicResidual.linearResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (B a : VectorCoefficients D) (p : Coefficients D) : VectorCoefficients D

Literal coefficient formula for the differentiated linearized PDE.

Equations

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

noncomputable def NavierStokes.HarmonicResidual.nonlinearResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (B a : VectorCoefficients D) (p : Coefficients D) : VectorCoefficients D

Nonlinear residual, defined pointwise by linearResidual g k Φ kp B a p i + transport g k Φ kp a a i.

Equations

• NavierStokes.HarmonicResidual.nonlinearResidual g k Φ kp B a p i = NavierStokes.HarmonicResidual.linearResidual g k Φ kp B a p i + NavierStokes.HarmonicResidual.transport g k Φ kp a a i

theorem NavierStokes.HarmonicResidual.field_secondDerivative {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) {c : Coefficients D} (hc : SmoothCoefficients U c) {Φ : D → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) {V : D → D} (hV : ContDiffOn ℝ (↑⊤) V U) (k : ℝ) (kp : ℤ) {p : D × ℝ} (hp : p ∈ liftDomain U) : HarmonicFields.field (HarmonicFields.differentiate V k Φ (HarmonicFields.differentiate V k Φ c)) k Φ kp p = HarmonicCalculus.along (liftDirection V) (HarmonicCalculus.along (liftDirection V) (HarmonicFields.field c k Φ kp)) p

theorem NavierStokes.HarmonicResidual.field_secondAngular {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) {c : Coefficients D} (hc : SmoothCoefficients U c) {Φ : D → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (k : ℝ) (kp : ℤ) {p : D × ℝ} (hp : p ∈ liftDomain U) : HarmonicFields.field (HarmonicFields.angularDifferentiate kp (HarmonicFields.angularDifferentiate kp c)) k Φ kp p = HarmonicCalculus.along angularDirection (HarmonicCalculus.along angularDirection (HarmonicFields.field c k Φ kp)) p

theorem NavierStokes.HarmonicResidual.field_scalarLaplacian {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (g : Frame D) (hr : ContDiffOn ℝ (↑⊤) g.radial U) (hz : ContDiffOn ℝ (↑⊤) g.axial U) {c : Coefficients D} (hc : SmoothCoefficients U c) {Φ : D → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (k : ℝ) (kp : ℤ) {p : D × ℝ} (hp : p ∈ liftDomain U) : HarmonicFields.field (scalarLaplacian g k Φ kp c) k Φ kp p = HarmonicCalculus.cylindricalLaplacian (fun (q : D × ℝ) => g.radius q.1) (liftDirection g.radial) angularDirection (liftDirection g.axial) (HarmonicFields.field c k Φ kp) p

theorem NavierStokes.HarmonicResidual.field_vectorLaplacian {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (g : Frame D) (hr : ContDiffOn ℝ (↑⊤) g.radial U) (hz : ContDiffOn ℝ (↑⊤) g.axial U) {a : VectorCoefficients D} (ha : ∀ (i : Fin 3), SmoothCoefficients U (a i)) {Φ : D → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (k : ℝ) (kp : ℤ) {p : D × ℝ} (hp : p ∈ liftDomain U) : vectorField (vectorLaplacian g k Φ kp a) k Φ kp p = HarmonicCalculus.cylindricalVectorLaplacian (fun (q : D × ℝ) => g.radius q.1) (liftDirection g.radial) angularDirection (liftDirection g.axial) (vectorField a k Φ kp) p

theorem NavierStokes.HarmonicResidual.field_transport {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (g : Frame D) (a : VectorCoefficients D) {b : VectorCoefficients D} (hb : ∀ (i : Fin 3), SmoothCoefficients U (b i)) {Φ : D → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (k : ℝ) (kp : ℤ) {p : D × ℝ} (hp : p ∈ liftDomain U) : vectorField (transport g k Φ kp a b) k Φ kp p = LinearWaveResidual.transport (fun (q : D × ℝ) => g.radius q.1) (liftDirection g.radial) angularDirection (liftDirection g.axial) (vectorField a k Φ kp) (vectorField b k Φ kp) p

theorem NavierStokes.HarmonicResidual.field_gradient {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (g : Frame D) {c : Coefficients D} (hc : SmoothCoefficients U c) {Φ : D → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (k : ℝ) (kp : ℤ) {p : D × ℝ} (hp : p ∈ liftDomain U) : vectorField (gradient g k Φ kp c) k Φ kp p = LinearWaveResidual.gradient (fun (q : D × ℝ) => g.radius q.1) (liftDirection g.radial) angularDirection (liftDirection g.axial) (HarmonicFields.field c k Φ kp) p

theorem NavierStokes.HarmonicResidual.field_linearResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (g : Frame D) (hr : ContDiffOn ℝ (↑⊤) g.radial U) (hz : ContDiffOn ℝ (↑⊤) g.axial U) {B a : VectorCoefficients D} (hB : ∀ (i : Fin 3), SmoothCoefficients U (B i)) (ha : ∀ (i : Fin 3), SmoothCoefficients U (a i)) {c : Coefficients D} (hc : SmoothCoefficients U c) {Φ : D → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (k : ℝ) (kp : ℤ) {p : D × ℝ} (hp : p ∈ liftDomain U) : vectorField (linearResidual g k Φ kp B a c) k Φ kp p = LinearWaveResidual.linearResidual g.viscosity (fun (q : D × ℝ) => g.radius q.1) (liftDirection g.radial) angularDirection (liftDirection g.axial) (liftDirection g.time) (vectorField B k Φ kp) (vectorField a k Φ kp) (HarmonicFields.field c k Φ kp) p

theorem NavierStokes.HarmonicResidual.field_nonlinearResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (g : Frame D) (hr : ContDiffOn ℝ (↑⊤) g.radial U) (hz : ContDiffOn ℝ (↑⊤) g.axial U) {B a : VectorCoefficients D} (hB : ∀ (i : Fin 3), SmoothCoefficients U (B i)) (ha : ∀ (i : Fin 3), SmoothCoefficients U (a i)) {c : Coefficients D} (hc : SmoothCoefficients U c) {Φ : D → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (k : ℝ) (kp : ℤ) {p : D × ℝ} (hp : p ∈ liftDomain U) : vectorField (nonlinearResidual g k Φ kp B a c) k Φ kp p = LinearWaveResidual.linearResidual g.viscosity (fun (q : D × ℝ) => g.radius q.1) (liftDirection g.radial) angularDirection (liftDirection g.axial) (liftDirection g.time) (vectorField B k Φ kp) (vectorField a k Φ kp) (HarmonicFields.field c k Φ kp) p + LinearWaveResidual.transport (fun (q : D × ℝ) => g.radius q.1) (liftDirection g.radial) angularDirection (liftDirection g.axial) (vectorField a k Φ kp) (vectorField a k Φ kp) p

Reality, actual extraction, and harmonic values

theorem NavierStokes.HarmonicResidual.band_zero {D : Type} (N : ℕ) : HarmonicFields.BandLimited 0 N

theorem NavierStokes.HarmonicResidual.band_neg {D : Type} {c : Coefficients D} {N : ℕ} (hc : HarmonicFields.BandLimited c N) : HarmonicFields.BandLimited (-c) N

theorem NavierStokes.HarmonicResidual.band_sub {D : Type} {c d : Coefficients D} {N : ℕ} (hc : HarmonicFields.BandLimited c N) (hd : HarmonicFields.BandLimited d N) : HarmonicFields.BandLimited (c - d) N

theorem NavierStokes.HarmonicResidual.band_constant_mul {D : Type} (f : D → ℂ) {c : Coefficients D} {N : ℕ} (hc : HarmonicFields.BandLimited c N) : HarmonicFields.BandLimited (HarmonicFields.constantCoefficient f * c) N

theorem NavierStokes.HarmonicResidual.band_mul_constant {D : Type} {c : Coefficients D} {N : ℕ} (hc : HarmonicFields.BandLimited c N) (f : D → ℂ) : HarmonicFields.BandLimited (c * HarmonicFields.constantCoefficient f) N

theorem NavierStokes.HarmonicResidual.band_rotate {D : Type} {a : VectorCoefficients D} {N : ℕ} (ha : ∀ (i : Fin 3), HarmonicFields.BandLimited (a i) N) (i : Fin 3) : HarmonicFields.BandLimited (rotate a i) N

theorem NavierStokes.HarmonicResidual.band_scalarLaplacian {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) {c : Coefficients D} {N : ℕ} (hc : HarmonicFields.BandLimited c N) : HarmonicFields.BandLimited (scalarLaplacian g k Φ kp c) N

theorem NavierStokes.HarmonicResidual.band_vectorLaplacian {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) {a : VectorCoefficients D} {N : ℕ} (ha : ∀ (i : Fin 3), HarmonicFields.BandLimited (a i) N) (i : Fin 3) : HarmonicFields.BandLimited (vectorLaplacian g k Φ kp a i) N

theorem NavierStokes.HarmonicResidual.band_transport {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) {a b : VectorCoefficients D} {M N : ℕ} (ha : ∀ (i : Fin 3), HarmonicFields.BandLimited (a i) M) (hb : ∀ (i : Fin 3), HarmonicFields.BandLimited (b i) N) (i : Fin 3) : HarmonicFields.BandLimited (transport g k Φ kp a b i) (M + N)

theorem NavierStokes.HarmonicResidual.band_gradient {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) {c : Coefficients D} {N : ℕ} (hc : HarmonicFields.BandLimited c N) (i : Fin 3) : HarmonicFields.BandLimited (gradient g k Φ kp c i) N

theorem NavierStokes.HarmonicResidual.band_linearResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) {B a : VectorCoefficients D} {c : Coefficients D} {N : ℕ} (hB : ∀ (i : Fin 3), HarmonicFields.BandLimited (B i) 0) (ha : ∀ (i : Fin 3), HarmonicFields.BandLimited (a i) N) (hc : HarmonicFields.BandLimited c N) (i : Fin 3) : HarmonicFields.BandLimited (linearResidual g k Φ kp B a c i) N

theorem NavierStokes.HarmonicResidual.band_nonlinearResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) {B a : VectorCoefficients D} {c : Coefficients D} {N : ℕ} (hB : ∀ (i : Fin 3), HarmonicFields.BandLimited (B i) 0) (ha : ∀ (i : Fin 3), HarmonicFields.BandLimited (a i) N) (hc : HarmonicFields.BandLimited c N) (i : Fin 3) : HarmonicFields.BandLimited (nonlinearResidual g k Φ kp B a c i) (N + N)

The bound concerns harmonic values |j|, not the number of terms.

theorem NavierStokes.HarmonicResidual.band_conjugateReverse {D : Type} {c : Coefficients D} {N : ℕ} (hc : HarmonicFields.BandLimited c N) : HarmonicFields.BandLimited (HarmonicFields.conjugateReverse c) N

noncomputable def NavierStokes.HarmonicResidual.realCoefficients {D : Type} (c : Coefficients D) : Coefficients D

Canonical real projection, with exactly the conjugate negative harmonics.

Equations

• NavierStokes.HarmonicResidual.realCoefficients c = (NavierStokes.HarmonicFields.constantCoefficient fun (x : D) => 2⁻¹) * (c + NavierStokes.HarmonicFields.conjugateReverse c)

@[simp]

theorem NavierStokes.HarmonicResidual.realCoefficients_apply {D : Type} (c : Coefficients D) (j : ℤ) (x : D) : (realCoefficients c).coeff j x = 2⁻¹ * (c.coeff j x + (starRingEnd ℂ) (c.coeff (-j) x))

theorem NavierStokes.HarmonicResidual.realCoefficients_conjugate {D : Type} (c : Coefficients D) : HarmonicFields.ConjugateSymmetric (realCoefficients c)

theorem NavierStokes.HarmonicResidual.realCoefficients_eq_self {D : Type} {c : Coefficients D} (hc : HarmonicFields.ConjugateSymmetric c) : realCoefficients c = c

theorem NavierStokes.HarmonicResidual.field_realCoefficients {D : Type} (c : Coefficients D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (p : D × ℝ) : HarmonicFields.field (realCoefficients c) k Φ kp p = ↑(HarmonicFields.field c k Φ kp p).re

theorem NavierStokes.HarmonicResidual.band_realCoefficients {D : Type} {c : Coefficients D} {N : ℕ} (hc : HarmonicFields.BandLimited c N) : HarmonicFields.BandLimited (realCoefficients c) N

theorem NavierStokes.HarmonicResidual.SmoothCoefficients.conjugateReverse {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : Coefficients D} (hc : SmoothCoefficients U c) : SmoothCoefficients U (HarmonicFields.conjugateReverse c)

theorem NavierStokes.HarmonicResidual.SmoothCoefficients.realCoefficients {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : Coefficients D} (hc : SmoothCoefficients U c) : SmoothCoefficients U (HarmonicResidual.realCoefficients c)

noncomputable def NavierStokes.HarmonicResidual.extract {D : Type} (f : D × ℝ → ℂ) (k : ℝ) (Φ : D → ℝ) (kp j : ℤ) (x : D) : ℂ

Extraction is integration against the conjugate carrier, including its slow phase.

Equations

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

theorem NavierStokes.HarmonicResidual.extract_field {D : Type} (c : Coefficients D) (k : ℝ) (Φ : D → ℝ) {kp : ℤ} (hkp : kp ≠ 0) (j : ℤ) (x : D) : extract (HarmonicFields.field c k Φ kp) k Φ kp j x = c.coeff j x

theorem NavierStokes.HarmonicResidual.coefficients_unique {D : Type} {c d : Coefficients D} (k : ℝ) (Φ : D → ℝ) {kp : ℤ} (hkp : kp ≠ 0) (he : HarmonicFields.field c k Φ kp = HarmonicFields.field d k Φ kp) : c = d

For a nonzero angular frequency the coefficients are uniquely determined by the field.

noncomputable def NavierStokes.HarmonicResidual.nonconstant {D : Type} (c : Coefficients D) : Coefficients D

Nonconstant, given by c.erase 0.

Equations

• NavierStokes.HarmonicResidual.nonconstant c = AddMonoidAlgebra.erase 0 c

theorem NavierStokes.HarmonicResidual.nonconstant_eq_sub {D : Type} (c : Coefficients D) : nonconstant c = c - HarmonicFields.constantCoefficient (c.coeff 0)

theorem NavierStokes.HarmonicResidual.field_nonconstant {D : Type} (c : Coefficients D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (p : D × ℝ) : HarmonicFields.field (nonconstant c) k Φ kp p = HarmonicFields.field c k Φ kp p - c.coeff 0 p.1

theorem NavierStokes.HarmonicResidual.angularMean_nonconstant {D : Type} (c : Coefficients D) (k : ℝ) (Φ : D → ℝ) {kp : ℤ} (hkp : kp ≠ 0) (x : D) : (HarmonicFields.angularMean fun (θ : ℝ) => HarmonicFields.field (nonconstant c) k Φ kp (x, θ)) = 0

theorem NavierStokes.HarmonicResidual.nonconstant_conjugate {D : Type} {c : Coefficients D} (hc : HarmonicFields.ConjugateSymmetric c) : HarmonicFields.ConjugateSymmetric (nonconstant c)

theorem NavierStokes.HarmonicResidual.band_nonconstant {D : Type} {c : Coefficients D} {N : ℕ} (hc : HarmonicFields.BandLimited c N) : HarmonicFields.BandLimited (nonconstant c) N

theorem NavierStokes.HarmonicResidual.nonconstant_support {D : Type} {c : Coefficients D} {j : ℤ} (hj : j ∈ HarmonicFields.Coefficients.support (nonconstant c)) : j ≠ 0

theorem NavierStokes.HarmonicResidual.SmoothCoefficients.nonconstant {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {c : Coefficients D} (hc : SmoothCoefficients U c) : SmoothCoefficients U (HarmonicResidual.nonconstant c)

theorem NavierStokes.HarmonicResidual.Actual.angularGenerator_add (a b : HarmonicCalculus.ComplexVector) : HarmonicCalculus.angularGenerator (a + b) = HarmonicCalculus.angularGenerator a + HarmonicCalculus.angularGenerator b

theorem NavierStokes.HarmonicResidual.Actual.transport_add_left {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) (Vr Vθ Vz : D → D) (a b v : D → HarmonicCalculus.ComplexVector) (x : D) : LinearWaveResidual.transport R Vr Vθ Vz (a + b) v x = LinearWaveResidual.transport R Vr Vθ Vz a v x + LinearWaveResidual.transport R Vr Vθ Vz b v x

theorem NavierStokes.HarmonicResidual.Actual.transport_add_right {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) (Vr Vθ Vz : D → D) (u a b : D → HarmonicCalculus.ComplexVector) {x : D} (ha : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => a y i) x) (hb : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => b y i) x) : LinearWaveResidual.transport R Vr Vθ Vz u (a + b) x = LinearWaveResidual.transport R Vr Vθ Vz u a x + LinearWaveResidual.transport R Vr Vθ Vz u b x

theorem NavierStokes.HarmonicResidual.Actual.twiceAlong_add {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) {V : D → D} (hV : ContDiffOn ℝ (↑⊤) V U) {f g : D → ℂ} (hf : ContDiffOn ℝ (↑⊤) f U) (hg : ContDiffOn ℝ (↑⊤) g U) {x : D} (hx : x ∈ U) : HarmonicCalculus.along V (HarmonicCalculus.along V (f + g)) x = HarmonicCalculus.along V (HarmonicCalculus.along V f) x + HarmonicCalculus.along V (HarmonicCalculus.along V g) x

theorem NavierStokes.HarmonicResidual.Actual.cylindricalLaplacian_add {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (R : D → ℝ) {Vr Vθ Vz : D → D} (hr : ContDiffOn ℝ (↑⊤) Vr U) (hθ : ContDiffOn ℝ (↑⊤) Vθ U) (hz : ContDiffOn ℝ (↑⊤) Vz U) {f g : D → ℂ} (hf : ContDiffOn ℝ (↑⊤) f U) (hg : ContDiffOn ℝ (↑⊤) g U) {x : D} (hx : x ∈ U) : HarmonicCalculus.cylindricalLaplacian R Vr Vθ Vz (f + g) x = HarmonicCalculus.cylindricalLaplacian R Vr Vθ Vz f x + HarmonicCalculus.cylindricalLaplacian R Vr Vθ Vz g x

theorem NavierStokes.HarmonicResidual.Actual.cylindricalVectorLaplacian_add {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (R : D → ℝ) {Vr Vθ Vz : D → D} (hr : ContDiffOn ℝ (↑⊤) Vr U) (hθ : ContDiffOn ℝ (↑⊤) Vθ U) (hz : ContDiffOn ℝ (↑⊤) Vz U) {a b : D → HarmonicCalculus.ComplexVector} (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => a y i) U) (hb : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => b y i) U) {x : D} (hx : x ∈ U) : HarmonicCalculus.cylindricalVectorLaplacian R Vr Vθ Vz (a + b) x = HarmonicCalculus.cylindricalVectorLaplacian R Vr Vθ Vz a x + HarmonicCalculus.cylindricalVectorLaplacian R Vr Vθ Vz b x

theorem NavierStokes.HarmonicResidual.Actual.gradient_add {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) (Vr Vθ Vz : D → D) {p q : D → ℂ} {x : D} (hp : DifferentiableAt ℝ p x) (hq : DifferentiableAt ℝ q x) : LinearWaveResidual.gradient R Vr Vθ Vz (p + q) x = LinearWaveResidual.gradient R Vr Vθ Vz p x + LinearWaveResidual.gradient R Vr Vθ Vz q x

theorem NavierStokes.HarmonicResidual.Actual.linearResidual_add {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (ε : ℝ) (R : D → ℝ) {Vr Vθ Vz : D → D} (Vt : D → D) (hr : ContDiffOn ℝ (↑⊤) Vr U) (hθ : ContDiffOn ℝ (↑⊤) Vθ U) (hz : ContDiffOn ℝ (↑⊤) Vz U) (B a b : D → HarmonicCalculus.ComplexVector) (p q : D → ℂ) (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => a y i) U) (hb : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => b y i) U) (hp : ContDiffOn ℝ (↑⊤) p U) (hq : ContDiffOn ℝ (↑⊤) q U) {x : D} (hx : x ∈ U) : LinearWaveResidual.linearResidual ε R Vr Vθ Vz Vt B (a + b) (p + q) x = LinearWaveResidual.linearResidual ε R Vr Vθ Vz Vt B a p x + LinearWaveResidual.linearResidual ε R Vr Vθ Vz Vt B b q x

noncomputable def NavierStokes.HarmonicResidual.Actual.nonlinearResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (ε : ℝ) (R : D → ℝ) (Vr Vθ Vz Vt : D → D) (B a : D → HarmonicCalculus.ComplexVector) (p : D → ℂ) (x : D) : HarmonicCalculus.ComplexVector

Exact residual of a perturbation of a fixed base, before the virtual stress and the separately retained base residual are added.

Equations

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

theorem NavierStokes.HarmonicResidual.Actual.nonlinearResidual_add_sub {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (ε : ℝ) (R : D → ℝ) {Vr Vθ Vz : D → D} (Vt : D → D) (hr : ContDiffOn ℝ (↑⊤) Vr U) (hθ : ContDiffOn ℝ (↑⊤) Vθ U) (hz : ContDiffOn ℝ (↑⊤) Vz U) (B a b : D → HarmonicCalculus.ComplexVector) (p q : D → ℂ) (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => a y i) U) (hb : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => b y i) U) (hp : ContDiffOn ℝ (↑⊤) p U) (hq : ContDiffOn ℝ (↑⊤) q U) {x : D} (hx : x ∈ U) : nonlinearResidual ε R Vr Vθ Vz Vt B (a + b) (p + q) x - nonlinearResidual ε R Vr Vθ Vz Vt B a p x = LinearWaveResidual.linearResidual ε R Vr Vθ Vz Vt B b q x + LinearWaveResidual.transport R Vr Vθ Vz a b x + LinearWaveResidual.transport R Vr Vθ Vz b a x + LinearWaveResidual.transport R Vr Vθ Vz b b x

theorem NavierStokes.HarmonicResidual.Actual.transport_zero_of_disjoint {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) (Vr Vθ Vz : D → D) {u v : D → HarmonicCalculus.ComplexVector} (hd : Disjoint (tsupport u) (tsupport v)) (x : D) : LinearWaveResidual.transport R Vr Vθ Vz u v x = 0

theorem NavierStokes.HarmonicResidual.Actual.transport_sum_left {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_1} (s : Finset ι) (R : D → ℝ) (Vr Vθ Vz : D → D) (u : ι → D → HarmonicCalculus.ComplexVector) (v : D → HarmonicCalculus.ComplexVector) (x : D) : LinearWaveResidual.transport R Vr Vθ Vz (∑ l ∈ s, u l) v x = ∑ l ∈ s, LinearWaveResidual.transport R Vr Vθ Vz (u l) v x

theorem NavierStokes.HarmonicResidual.Actual.transport_sum_right {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_1} (s : Finset ι) (R : D → ℝ) (Vr Vθ Vz : D → D) (u : D → HarmonicCalculus.ComplexVector) (v : ι → D → HarmonicCalculus.ComplexVector) {x : D} (hv : ∀ l ∈ s, ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => v l y i) x) : LinearWaveResidual.transport R Vr Vθ Vz u (∑ l ∈ s, v l) x = ∑ l ∈ s, LinearWaveResidual.transport R Vr Vθ Vz u (v l) x

theorem NavierStokes.HarmonicResidual.Actual.transport_sum_self {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_1} (s : Finset ι) (R : D → ℝ) (Vr Vθ Vz : D → D) (u : ι → D → HarmonicCalculus.ComplexVector) {x : D} (hu : ∀ l ∈ s, ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => u l y i) x) (hdisj : ∀ l ∈ s, ∀ j ∈ s, l ≠ j → Disjoint (tsupport (u l)) (tsupport (u j))) : LinearWaveResidual.transport R Vr Vθ Vz (∑ l ∈ s, u l) (∑ l ∈ s, u l) x = ∑ l ∈ s, LinearWaveResidual.transport R Vr Vθ Vz (u l) (u l) x

theorem NavierStokes.HarmonicResidual.Actual.linearResidual_sum {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_1} (s : Finset ι) {U : Set D} (hU : IsOpen U) (ε : ℝ) (R : D → ℝ) {Vr Vθ Vz : D → D} (Vt : D → D) (hr : ContDiffOn ℝ (↑⊤) Vr U) (hθ : ContDiffOn ℝ (↑⊤) Vθ U) (hz : ContDiffOn ℝ (↑⊤) Vz U) (B : D → HarmonicCalculus.ComplexVector) (u : ι → D → HarmonicCalculus.ComplexVector) (p : ι → D → ℂ) (hu : ∀ l ∈ s, ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => u l y i) U) (hp : ∀ l ∈ s, ContDiffOn ℝ (↑⊤) (p l) U) {x : D} (hx : x ∈ U) : LinearWaveResidual.linearResidual ε R Vr Vθ Vz Vt B (∑ l ∈ s, u l) (∑ l ∈ s, p l) x = ∑ l ∈ s, LinearWaveResidual.linearResidual ε R Vr Vθ Vz Vt B (u l) (p l) x

theorem NavierStokes.HarmonicResidual.Actual.nonlinearResidual_sum {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_1} (s : Finset ι) {U : Set D} (hU : IsOpen U) (ε : ℝ) (R : D → ℝ) {Vr Vθ Vz : D → D} (Vt : D → D) (hr : ContDiffOn ℝ (↑⊤) Vr U) (hθ : ContDiffOn ℝ (↑⊤) Vθ U) (hz : ContDiffOn ℝ (↑⊤) Vz U) (B : D → HarmonicCalculus.ComplexVector) (u : ι → D → HarmonicCalculus.ComplexVector) (p : ι → D → ℂ) (hu : ∀ l ∈ s, ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => u l y i) U) (hp : ∀ l ∈ s, ContDiffOn ℝ (↑⊤) (p l) U) (hdisj : ∀ l ∈ s, ∀ j ∈ s, l ≠ j → Disjoint (tsupport (u l)) (tsupport (u j))) {x : D} (hx : x ∈ U) : nonlinearResidual ε R Vr Vθ Vz Vt B (∑ l ∈ s, u l) (∑ l ∈ s, p l) x = ∑ l ∈ s, nonlinearResidual ε R Vr Vθ Vz Vt B (u l) (p l) x

theorem NavierStokes.HarmonicResidual.Actual.linearResidual_base_add {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (ε : ℝ) (R : D → ℝ) (Vr Vθ Vz Vt : D → D) (B M a : D → HarmonicCalculus.ComplexVector) (p : D → ℂ) {x : D} (hB : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => B y i) x) (hM : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => M y i) x) : LinearWaveResidual.linearResidual ε R Vr Vθ Vz Vt (B + M) a p x = LinearWaveResidual.linearResidual ε R Vr Vθ Vz Vt B a p x + LinearWaveResidual.transport R Vr Vθ Vz M a x + LinearWaveResidual.transport R Vr Vθ Vz a M x

theorem NavierStokes.HarmonicResidual.Actual.nonlinearResidual_mean_add {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (ε : ℝ) (R : D → ℝ) {Vr Vθ Vz : D → D} (Vt : D → D) (hr : ContDiffOn ℝ (↑⊤) Vr U) (hθ : ContDiffOn ℝ (↑⊤) Vθ U) (hz : ContDiffOn ℝ (↑⊤) Vz U) (B M a : D → HarmonicCalculus.ComplexVector) (p q : D → ℂ) (hB : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => B y i) U) (hM : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => M y i) U) (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => a y i) U) (hp : ContDiffOn ℝ (↑⊤) p U) (hq : ContDiffOn ℝ (↑⊤) q U) {x : D} (hx : x ∈ U) : nonlinearResidual ε R Vr Vθ Vz Vt B (M + a) (p + q) x = nonlinearResidual ε R Vr Vθ Vz Vt B M p x + nonlinearResidual ε R Vr Vθ Vz Vt (B + M) a q x

structure NavierStokes.HarmonicResidual.Frame.Regular {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : Frame D) (U : Set D) : Prop

Regularity of the actual graph directions, with the cylindrical radius nonzero.

• radius : ContDiffOn ℝ (↑⊤) g.radius U
• radius_ne (x : D) : x ∈ U → g.radius x ≠ 0
• radial : ContDiffOn ℝ (↑⊤) g.radial U
• axial : ContDiffOn ℝ (↑⊤) g.axial U
• time : ContDiffOn ℝ (↑⊤) g.time U

theorem NavierStokes.HarmonicResidual.liftDirection_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {V : D → D} (hV : ContDiffOn ℝ (↑⊤) V U) : ContDiffOn ℝ (↑⊤) (liftDirection V) (liftDomain U)

theorem NavierStokes.HarmonicResidual.smooth_rotate {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {a : VectorCoefficients D} (ha : ∀ (i : Fin 3), SmoothCoefficients U (a i)) (i : Fin 3) : SmoothCoefficients U (rotate a i)

theorem NavierStokes.HarmonicResidual.Frame.Regular.invRadius {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {g : Frame D} {U : Set D} (hg : g.Regular U) : SmoothCoefficients U (HarmonicFields.constantCoefficient fun (x : D) => ↑(g.radius x)⁻¹)

theorem NavierStokes.HarmonicResidual.Frame.Regular.invSquare {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {g : Frame D} {U : Set D} (hg : g.Regular U) : SmoothCoefficients U (HarmonicFields.constantCoefficient fun (x : D) => ↑(g.radius x ^ 2)⁻¹)

theorem NavierStokes.HarmonicResidual.smooth_scalarLaplacian {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) {g : Frame D} (hg : g.Regular U) {Φ : D → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (k : ℝ) (kp : ℤ) {c : Coefficients D} (hc : SmoothCoefficients U c) : SmoothCoefficients U (scalarLaplacian g k Φ kp c)

theorem NavierStokes.HarmonicResidual.smooth_vectorLaplacian {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) {g : Frame D} (hg : g.Regular U) {Φ : D → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (k : ℝ) (kp : ℤ) {a : VectorCoefficients D} (ha : ∀ (i : Fin 3), SmoothCoefficients U (a i)) (i : Fin 3) : SmoothCoefficients U (vectorLaplacian g k Φ kp a i)

theorem NavierStokes.HarmonicResidual.smooth_transport {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) {g : Frame D} (hg : g.Regular U) {Φ : D → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (k : ℝ) (kp : ℤ) {a b : VectorCoefficients D} (ha : ∀ (i : Fin 3), SmoothCoefficients U (a i)) (hb : ∀ (i : Fin 3), SmoothCoefficients U (b i)) (i : Fin 3) : SmoothCoefficients U (transport g k Φ kp a b i)

theorem NavierStokes.HarmonicResidual.smooth_gradient {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) {g : Frame D} (hg : g.Regular U) {Φ : D → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (k : ℝ) (kp : ℤ) {c : Coefficients D} (hc : SmoothCoefficients U c) (i : Fin 3) : SmoothCoefficients U (gradient g k Φ kp c i)

theorem NavierStokes.HarmonicResidual.smooth_nonlinearResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) {g : Frame D} (hg : g.Regular U) {Φ : D → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (k : ℝ) (kp : ℤ) {B a : VectorCoefficients D} (hB : ∀ (i : Fin 3), SmoothCoefficients U (B i)) (ha : ∀ (i : Fin 3), SmoothCoefficients U (a i)) {c : Coefficients D} (hc : SmoothCoefficients U c) (i : Fin 3) : SmoothCoefficients U (nonlinearResidual g k Φ kp B a c i)

noncomputable def NavierStokes.HarmonicResidual.constantVector {D : Type} (a : D → HarmonicCalculus.ComplexVector) : VectorCoefficients D

Constant vector, defined pointwise by constantCoefficient (fun x => a x i).

Equations

• NavierStokes.HarmonicResidual.constantVector a i = NavierStokes.HarmonicFields.constantCoefficient fun (x : D) => a x i

@[simp]

theorem NavierStokes.HarmonicResidual.vectorField_constantVector {D : Type} (a : D → HarmonicCalculus.ComplexVector) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (p : D × ℝ) : vectorField (constantVector a) k Φ kp p = a p.1

theorem NavierStokes.HarmonicResidual.band_zero_eq_constant {D : Type} {c : Coefficients D} (hc : HarmonicFields.BandLimited c 0) : c = HarmonicFields.constantCoefficient (c.coeff 0)

theorem NavierStokes.HarmonicResidual.field_band_zero {D : Type} {c : Coefficients D} (hc : HarmonicFields.BandLimited c 0) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (p : D × ℝ) : HarmonicFields.field c k Φ kp p = c.coeff 0 p.1

structure NavierStokes.HarmonicResidual.LabelData (D : Type) : Type

A label retains its own slow phase and native angular frequency.

• frequency : ℝ

  Frequency of LabelData, of type ℝ.

• phase : D → ℝ

  Phase of LabelData, of type D → ℝ.

• angularFrequency : ℤ

  Angular frequency of LabelData, of type ℤ.

• velocity : VectorCoefficients D

  Velocity field of LabelData, of type VectorCoefficients D.

• pressure : Coefficients D

  Pressure field of LabelData, of type Coefficients D.

• gaussian : VectorCoefficients D

  Gaussian of LabelData, of type VectorCoefficients D.

• aliasError : VectorCoefficients D

  Alias error of LabelData, of type VectorCoefficients D.

noncomputable def NavierStokes.HarmonicResidual.LabelData.wave {D : Type} (d : LabelData D) : D × ℝ → HarmonicCalculus.ComplexVector

Wave, given by vectorField d.velocity d.frequency d.phase d.angularFrequency.

Equations

• d.wave = NavierStokes.HarmonicResidual.vectorField d.velocity d.frequency d.phase d.angularFrequency

noncomputable def NavierStokes.HarmonicResidual.LabelData.pressureField {D : Type} (d : LabelData D) : D × ℝ → ℂ

Pressure field, given by field d.pressure d.frequency d.phase d.angularFrequency.

Equations

• d.pressureField = NavierStokes.HarmonicFields.field d.pressure d.frequency d.phase d.angularFrequency

noncomputable def NavierStokes.HarmonicResidual.LabelData.gaussianField {D : Type} (d : LabelData D) : D × ℝ → HarmonicCalculus.ComplexVector

Gaussian field, given by vectorField d.gaussian d.frequency d.phase d.angularFrequency.

Equations

• d.gaussianField = NavierStokes.HarmonicResidual.vectorField d.gaussian d.frequency d.phase d.angularFrequency

noncomputable def NavierStokes.HarmonicResidual.LabelData.aliasField {D : Type} (d : LabelData D) : D × ℝ → HarmonicCalculus.ComplexVector

Alias field, given by vectorField d.aliasError d.frequency d.phase d.angularFrequency.

Equations

• d.aliasField = NavierStokes.HarmonicResidual.vectorField d.aliasError d.frequency d.phase d.angularFrequency

structure NavierStokes.HarmonicResidual.LabelData.Regular {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (d : LabelData D) (U : Set D) : Prop

Regular data, collecting phase, velocity, pressure.

• phase : ContDiffOn ℝ (↑⊤) d.phase U
• velocity (i : Fin 3) : SmoothCoefficients U (d.velocity i)
• pressure : SmoothCoefficients U d.pressure

noncomputable def NavierStokes.HarmonicResidual.meanCoefficients {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : Frame D) (B M : D → HarmonicCalculus.ComplexVector) (p : D → ℂ) : VectorCoefficients D

Mean coefficients, given by nonlinearResidual g 0 (fun _ => 0) 1 (constantVector B) (constantVector M) (constantCoefficient p).

Equations

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

noncomputable def NavierStokes.HarmonicResidual.LabelData.residualCoefficients {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (d : LabelData D) (g : Frame D) (B M : D → HarmonicCalculus.ComplexVector) : VectorCoefficients D

Gaussian and alias fields are subtracted after the actual nonlinear differential residual.

Equations

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

noncomputable def NavierStokes.HarmonicResidual.LabelData.waveResidualCoefficients {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (d : LabelData D) (g : Frame D) (B M : D → HarmonicCalculus.ComplexVector) : VectorCoefficients D

Wave residual coefficients, defined pointwise by nonconstant (d.residualCoefficients g B M i).

Equations

• d.waveResidualCoefficients g B M i = NavierStokes.HarmonicResidual.nonconstant (d.residualCoefficients g B M i)

noncomputable def NavierStokes.HarmonicResidual.goodResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_1} (labels : Finset ι) (data : ι → LabelData D) (g : Frame D) (B M : D → HarmonicCalculus.ComplexVector) (p : D → ℂ) (virtual : D → Fin 3 → ℝ) (x : D × ℝ) (i : Fin 3) : ℝ

Good residual as an element of ℝ.

Equations

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

theorem NavierStokes.HarmonicResidual.meanCoefficients_band {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (g : Frame D) (B M : D → HarmonicCalculus.ComplexVector) (p : D → ℂ) (i : Fin 3) : HarmonicFields.BandLimited (meanCoefficients g B M p i) 0

theorem NavierStokes.HarmonicResidual.meanCoefficients_field {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (g : Frame D) (hr : ContDiffOn ℝ (↑⊤) g.radial U) (hz : ContDiffOn ℝ (↑⊤) g.axial U) (B M : D → HarmonicCalculus.ComplexVector) (p : D → ℂ) (hB : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => B y i) U) (hM : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => M y i) U) (hp : ContDiffOn ℝ (↑⊤) p U) {x : D × ℝ} (hx : x ∈ liftDomain U) : Actual.nonlinearResidual g.viscosity (fun (y : D × ℝ) => g.radius y.1) (liftDirection g.radial) angularDirection (liftDirection g.axial) (liftDirection g.time) (fun (y : D × ℝ) => B y.1) (fun (y : D × ℝ) => M y.1) (fun (y : D × ℝ) => p y.1) x = fun (i : Fin 3) => (meanCoefficients g B M p i).coeff 0 x.1

theorem NavierStokes.HarmonicResidual.LabelData.residualCoefficients_field {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (g : Frame D) (hr : ContDiffOn ℝ (↑⊤) g.radial U) (hz : ContDiffOn ℝ (↑⊤) g.axial U) (B M : D → HarmonicCalculus.ComplexVector) (hB : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => B y i) U) (hM : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => M y i) U) (d : LabelData D) (hd : d.Regular U) {x : D × ℝ} (hx : x ∈ liftDomain U) (i : Fin 3) : (HarmonicFields.field (d.residualCoefficients g B M i) d.frequency d.phase d.angularFrequency x).re = (Actual.nonlinearResidual g.viscosity (fun (y : D × ℝ) => g.radius y.1) (liftDirection g.radial) angularDirection (liftDirection g.axial) (liftDirection g.time) ((fun (y : D × ℝ) => B y.1) + fun (y : D × ℝ) => M y.1) d.wave d.pressureField x i).re - (d.gaussianField x i).re - (d.aliasField x i).re

theorem NavierStokes.HarmonicResidual.goodResidual_grouped {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_1} (labels : Finset ι) (data : ι → LabelData D) {U : Set D} (hU : IsOpen U) {g : Frame D} (hg : g.Regular U) (B M : D → HarmonicCalculus.ComplexVector) (p : D → ℂ) (virtual : D → Fin 3 → ℝ) (hB : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => B y i) U) (hM : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => M y i) U) (hp : ContDiffOn ℝ (↑⊤) p U) (hd : ∀ l ∈ labels, (data l).Regular U) (hdisj : ∀ l ∈ labels, ∀ j ∈ labels, l ≠ j → Disjoint (tsupport (data l).wave) (tsupport (data j).wave)) {x : D × ℝ} (hx : x ∈ liftDomain U) (i : Fin 3) : goodResidual labels data g B M p virtual x i = ((meanCoefficients g B M p i).coeff 0 x.1).re + virtual x.1 i + ∑ l ∈ labels, (HarmonicFields.field ((data l).residualCoefficients g B M i) (data l).frequency (data l).phase (data l).angularFrequency x).re

theorem NavierStokes.HarmonicResidual.LabelData.residualCoefficients_band {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (d : LabelData D) (g : Frame D) (B M : D → HarmonicCalculus.ComplexVector) {N E : ℕ} (hu : ∀ (i : Fin 3), HarmonicFields.BandLimited (d.velocity i) N) (hp : HarmonicFields.BandLimited d.pressure N) (hg : ∀ (i : Fin 3), HarmonicFields.BandLimited (d.gaussian i) E) (ha : ∀ (i : Fin 3), HarmonicFields.BandLimited (d.aliasError i) E) (i : Fin 3) : HarmonicFields.BandLimited (d.residualCoefficients g B M i) (max (N + N) E)

theorem NavierStokes.HarmonicResidual.LabelData.waveResidualCoefficients_band {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (d : LabelData D) (g : Frame D) (B M : D → HarmonicCalculus.ComplexVector) {N E : ℕ} (hu : ∀ (i : Fin 3), HarmonicFields.BandLimited (d.velocity i) N) (hp : HarmonicFields.BandLimited d.pressure N) (hg : ∀ (i : Fin 3), HarmonicFields.BandLimited (d.gaussian i) E) (ha : ∀ (i : Fin 3), HarmonicFields.BandLimited (d.aliasError i) E) (i : Fin 3) : HarmonicFields.BandLimited (d.waveResidualCoefficients g B M i) (max (N + N) E)

theorem NavierStokes.HarmonicResidual.LabelData.waveResidualCoefficients_values {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (d : LabelData D) (g : Frame D) (B M : D → HarmonicCalculus.ComplexVector) {N E : ℕ} (hu : ∀ (i : Fin 3), HarmonicFields.BandLimited (d.velocity i) N) (hp : HarmonicFields.BandLimited d.pressure N) (hg : ∀ (i : Fin 3), HarmonicFields.BandLimited (d.gaussian i) E) (ha : ∀ (i : Fin 3), HarmonicFields.BandLimited (d.aliasError i) E) (i : Fin 3) (j : ℤ) (hj : j ∈ HarmonicFields.Coefficients.support (d.waveResidualCoefficients g B M i)) : j ≠ 0 ∧ j.natAbs ≤ max (N + N) E

theorem NavierStokes.HarmonicResidual.LabelData.residualCoefficients_conjugate {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (d : LabelData D) (g : Frame D) (B M : D → HarmonicCalculus.ComplexVector) (i : Fin 3) : HarmonicFields.ConjugateSymmetric (d.residualCoefficients g B M i)

theorem NavierStokes.HarmonicResidual.LabelData.waveResidualCoefficients_conjugate {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (d : LabelData D) (g : Frame D) (B M : D → HarmonicCalculus.ComplexVector) (i : Fin 3) : HarmonicFields.ConjugateSymmetric (d.waveResidualCoefficients g B M i)

theorem NavierStokes.HarmonicResidual.LabelData.waveResidualCoefficients_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) {g : Frame D} (hg : g.Regular U) (B M : D → HarmonicCalculus.ComplexVector) (hB : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => B y i) U) (hM : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => M y i) U) (d : LabelData D) (hd : d.Regular U) (hgaussian : ∀ (i : Fin 3), SmoothCoefficients U (d.gaussian i)) (halias : ∀ (i : Fin 3), SmoothCoefficients U (d.aliasError i)) (i : Fin 3) : SmoothCoefficients U (d.waveResidualCoefficients g B M i)

theorem NavierStokes.HarmonicResidual.LabelData.extract_residual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (d : LabelData D) (g : Frame D) (B M : D → HarmonicCalculus.ComplexVector) (hkp : d.angularFrequency ≠ 0) (i : Fin 3) (j : ℤ) (x : D) : extract (HarmonicFields.field (d.residualCoefficients g B M i) d.frequency d.phase d.angularFrequency) d.frequency d.phase d.angularFrequency j x = (d.residualCoefficients g B M i).coeff j x

noncomputable def NavierStokes.HarmonicResidual.realAngularMean (f : ℝ → ℝ) : ℝ

Real angular mean, given by (∫ θ in (0 : ℝ)..period, f θ) / period.

Equations

• NavierStokes.HarmonicResidual.realAngularMean f = (∫ (θ : ℝ) in 0..NavierStokes.HarmonicFields.period, f θ) / NavierStokes.HarmonicFields.period

theorem NavierStokes.HarmonicResidual.realAngularMean_const (a : ℝ) : (realAngularMean fun (x : ℝ) => a) = a

theorem NavierStokes.HarmonicResidual.realAngularMean_add {f g : ℝ → ℝ} (hf : Continuous f) (hg : Continuous g) : (realAngularMean fun (θ : ℝ) => f θ + g θ) = realAngularMean f + realAngularMean g

theorem NavierStokes.HarmonicResidual.realAngularMean_sum {ι : Type u_1} (s : Finset ι) (f : ι → ℝ → ℝ) (hf : ∀ l ∈ s, Continuous (f l)) : (realAngularMean fun (θ : ℝ) => ∑ l ∈ s, f l θ) = ∑ l ∈ s, realAngularMean (f l)

theorem NavierStokes.HarmonicResidual.realAngularMean_field {D : Type} (c : Coefficients D) (k : ℝ) (Φ : D → ℝ) {kp : ℤ} (hkp : kp ≠ 0) (x : D) : (realAngularMean fun (θ : ℝ) => (HarmonicFields.field c k Φ kp (x, θ)).re) = (c.coeff 0 x).re

noncomputable def NavierStokes.HarmonicResidual.meanResidualValue {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_1} (labels : Finset ι) (data : ι → LabelData D) (g : Frame D) (B M : D → HarmonicCalculus.ComplexVector) (p : D → ℂ) (virtual : D → Fin 3 → ℝ) (x : D) (i : Fin 3) : ℝ

Mean residual value, given by (meanCoefficients g B M p i 0 x).re + virtual x i + ∑ l ∈ labels, (data l |>.residualCoefficients g B M i 0 x).re.

Equations

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

theorem NavierStokes.HarmonicResidual.goodResidual_angularMean {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_1} (labels : Finset ι) (data : ι → LabelData D) {U : Set D} (hU : IsOpen U) {g : Frame D} (hg : g.Regular U) (B M : D → HarmonicCalculus.ComplexVector) (p : D → ℂ) (virtual : D → Fin 3 → ℝ) (hB : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => B y i) U) (hM : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => M y i) U) (hp : ContDiffOn ℝ (↑⊤) p U) (hd : ∀ l ∈ labels, (data l).Regular U) (hdisj : ∀ l ∈ labels, ∀ j ∈ labels, l ≠ j → Disjoint (tsupport (data l).wave) (tsupport (data j).wave)) (hkp : ∀ l ∈ labels, (data l).angularFrequency ≠ 0) {x : D} (hx : x ∈ U) (i : Fin 3) : (realAngularMean fun (θ : ℝ) => goodResidual labels data g B M p virtual (x, θ) i) = meanResidualValue labels data g B M p virtual x i

noncomputable def NavierStokes.HarmonicResidual.goodWaveResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_1} (labels : Finset ι) (data : ι → LabelData D) (g : Frame D) (B M : D → HarmonicCalculus.ComplexVector) (p : D → ℂ) (virtual : D → Fin 3 → ℝ) (x : D × ℝ) (i : Fin 3) : ℝ

Good wave residual, given by goodResidual labels data g B M p virtual x i - realAngularMean (fun θ => goodResidual labels data g B M p virtual (x.1, θ) i).

Equations

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

theorem NavierStokes.HarmonicResidual.goodWaveResidual_grouped {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_1} (labels : Finset ι) (data : ι → LabelData D) {U : Set D} (hU : IsOpen U) {g : Frame D} (hg : g.Regular U) (B M : D → HarmonicCalculus.ComplexVector) (p : D → ℂ) (virtual : D → Fin 3 → ℝ) (hB : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => B y i) U) (hM : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => M y i) U) (hp : ContDiffOn ℝ (↑⊤) p U) (hd : ∀ l ∈ labels, (data l).Regular U) (hdisj : ∀ l ∈ labels, ∀ j ∈ labels, l ≠ j → Disjoint (tsupport (data l).wave) (tsupport (data j).wave)) (hkp : ∀ l ∈ labels, (data l).angularFrequency ≠ 0) {x : D × ℝ} (hx : x ∈ liftDomain U) (i : Fin 3) : goodWaveResidual labels data g B M p virtual x i = ∑ l ∈ labels, (HarmonicFields.field ((data l).waveResidualCoefficients g B M i) (data l).frequency (data l).phase (data l).angularFrequency x).re

Exact reconstruction of the good nonconstant PDE residual by native-label blocks.

The stored correction state and its actual grouped residual

noncomputable def NavierStokes.HarmonicResidual.contextFrame {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (n : ℕ) : Frame D

Context frame, bundling radius, radial, axial, time and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.HarmonicResidual.contextBase {D : Type} (c : CorrectionState.Context D) (n : ℕ) (x : D) : HarmonicCalculus.ComplexVector

Context base, given by ![(c.base.radial n x : ℂ), (c.base.angular n x : ℂ), (c.base.axial n x : ℂ)].

Equations

• NavierStokes.HarmonicResidual.contextBase c n x = ![↑(c.base.radial n x), ↑(c.base.angular n x), ↑(c.base.axial n x)]

noncomputable def NavierStokes.HarmonicResidual.stateMean {D : Type} (s : CorrectionState.State D) (n : ℕ) (x : D) : HarmonicCalculus.ComplexVector

State mean, given by ![(s.mean.radial n x : ℂ), (s.mean.angular n x : ℂ), (s.mean.axial n x : ℂ)].

Equations

• NavierStokes.HarmonicResidual.stateMean s n x = ![↑(s.mean.radial n x), ↑(s.mean.angular n x), ↑(s.mean.axial n x)]

noncomputable def NavierStokes.HarmonicResidual.statePerturbation {D : Type} (s : CorrectionState.State D) (n : ℕ) (x : D × ℝ) : HarmonicCalculus.ComplexVector

State perturbation as an element of ComplexVector.

Equations

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

noncomputable def NavierStokes.HarmonicResidual.statePressure {D : Type} (s : CorrectionState.State D) (n : ℕ) (x : D × ℝ) : ℂ

State pressure, given by (s.totalPressureIncrement n x : ℝ).

Equations

• NavierStokes.HarmonicResidual.statePressure s n x = ↑(s.totalPressureIncrement n x)

noncomputable def NavierStokes.HarmonicResidual.contextVirtual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (n : ℕ) (x : D) : Fin 3 → ℝ

Context virtual, given by ![0, -(c.operators.radialDiv 2 c.virtualTheta n x), -(c.operators.radialDiv 1 c.virtualAxial n x)].

Equations

• NavierStokes.HarmonicResidual.contextVirtual c n x = ![0, -c.operators.radialDiv 2 c.virtualTheta n x, -c.operators.radialDiv 1 c.virtualAxial n x]

noncomputable def NavierStokes.HarmonicResidual.stateFullResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (s : CorrectionState.State D) (n : ℕ) (x : D × ℝ) (i : Fin 3) : ℝ

The same full normalized differential field used by the correction cycle.

Equations

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

noncomputable def NavierStokes.HarmonicResidual.stateGoodResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (s : CorrectionState.State D) : CorrectionState.Oscillation D

State good residual, given by stateFullResidual c s - s.errors.total.

Equations

• NavierStokes.HarmonicResidual.stateGoodResidual c s = NavierStokes.HarmonicResidual.stateFullResidual c s - s.errors.total

noncomputable def NavierStokes.HarmonicResidual.stateGoodWaveResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (s : CorrectionState.State D) (n : ℕ) (x : D × ℝ) (i : Fin 3) : ℝ

State good wave residual, given by stateGoodResidual c s n x i - CorrectionState.angularAverage (fun m y => stateGoodResidual c s m y i) n x.1.

Equations

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

@[reducible, inline]

abbrev NavierStokes.HarmonicResidual.BlockCoefficients (D : Type) : Type

Block coefficients: an abbreviation for ℕ → VectorCoefficients D.

Equations

• NavierStokes.HarmonicResidual.BlockCoefficients D = (ℕ → NavierStokes.HarmonicResidual.VectorCoefficients D)

noncomputable def NavierStokes.HarmonicResidual.ofBlock {D : Type} (b : CorrectionState.HarmonicBlock D) (gaussian aliasError : BlockCoefficients D) (n : ℕ) : LabelData D

Input blocks are interpreted as their actual real fields. The real projection does not enlarge the largest harmonic value and is the identity for conjugate data.

Equations

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

theorem NavierStokes.HarmonicResidual.ofBlock_wave {D : Type} (b : CorrectionState.HarmonicBlock D) (gaussian aliasError : BlockCoefficients D) (n : ℕ) (x : D × ℝ) (i : Fin 3) : (ofBlock b gaussian aliasError n).wave x i = ↑(b.oscillation n x i)

theorem NavierStokes.HarmonicResidual.ofBlock_pressure {D : Type} (b : CorrectionState.HarmonicBlock D) (gaussian aliasError : BlockCoefficients D) (n : ℕ) (x : D × ℝ) : (ofBlock b gaussian aliasError n).pressureField x = ↑(b.oscillatoryPressure n x)

theorem NavierStokes.HarmonicResidual.ofBlock_tsupport_wave {D : Type} [NormedAddCommGroup D] (b : CorrectionState.HarmonicBlock D) (gaussian aliasError : BlockCoefficients D) (n : ℕ) : tsupport (ofBlock b gaussian aliasError n).wave = tsupport (b.oscillation n)

theorem NavierStokes.HarmonicResidual.ofBlock_regular {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (b : CorrectionState.HarmonicBlock D) (gaussian aliasError : BlockCoefficients D) (n : ℕ) (hΦ : ContDiffOn ℝ (↑⊤) (b.phase n) U) (hv : ∀ (i : Fin 3), SmoothCoefficients U (b.velocity n i)) (hp : SmoothCoefficients U (b.pressure n)) : (ofBlock b gaussian aliasError n).Regular U

structure NavierStokes.HarmonicResidual.BlockRepresentation {D : Type} {ι : Type u_1} (labels : ℕ → Finset ι) (blocks : ι → CorrectionState.HarmonicBlock D) (gaussianCoeffs aliasCoeffs : ι → BlockCoefficients D) (s : CorrectionState.State D) : Prop

Only representations of the stored fields are inputs; no residual identity is assumed. The finite label set may vary with the band.

• velocity (n : ℕ) (x : D × ℝ) (i : Fin 3) : s.oscillation n x i = ∑ l ∈ labels n, (blocks l).oscillation n x i
• pressure (n : ℕ) (x : D × ℝ) : s.oscillatoryPressure n x = ∑ l ∈ labels n, (blocks l).oscillatoryPressure n x
• gaussian (n : ℕ) (x : D × ℝ) (i : Fin 3) : s.errors.gaussian n x i = ∑ l ∈ labels n, ((ofBlock (blocks l) (gaussianCoeffs l) (aliasCoeffs l) n).gaussianField x i).re
• aliasError (n : ℕ) (x : D × ℝ) (i : Fin 3) : s.errors.aliasError n x i = ∑ l ∈ labels n, ((ofBlock (blocks l) (gaussianCoeffs l) (aliasCoeffs l) n).aliasField x i).re

theorem NavierStokes.HarmonicResidual.BlockRepresentation.perturbation {D : Type} {ι : Type u_1} {labels : ℕ → Finset ι} {blocks : ι → CorrectionState.HarmonicBlock D} {gaussian aliasError : ι → BlockCoefficients D} {s : CorrectionState.State D} (hrep : BlockRepresentation labels blocks gaussian aliasError s) (n : ℕ) : statePerturbation s n = (fun (x : D × ℝ) => stateMean s n x.1) + ∑ l ∈ labels n, (ofBlock (blocks l) (gaussian l) (aliasError l) n).wave

theorem NavierStokes.HarmonicResidual.BlockRepresentation.pressureField {D : Type} {ι : Type u_1} {labels : ℕ → Finset ι} {blocks : ι → CorrectionState.HarmonicBlock D} {gaussian aliasError : ι → BlockCoefficients D} {s : CorrectionState.State D} (hrep : BlockRepresentation labels blocks gaussian aliasError s) (n : ℕ) : statePressure s n = (fun (x : D × ℝ) => ↑(s.pressure n x.1)) + ∑ l ∈ labels n, (ofBlock (blocks l) (gaussian l) (aliasError l) n).pressureField

theorem NavierStokes.HarmonicResidual.BlockRepresentation.goodResidual_eq {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_1} {labels : ℕ → Finset ι} {blocks : ι → CorrectionState.HarmonicBlock D} {gaussian aliasError : ι → BlockCoefficients D} {s : CorrectionState.State D} (hrep : BlockRepresentation labels blocks gaussian aliasError s) (c : CorrectionState.Context D) (n : ℕ) (x : D × ℝ) (i : Fin 3) : stateGoodResidual c s n x i = goodResidual (labels n) (fun (l : ι) => ofBlock (blocks l) (gaussian l) (aliasError l) n) (contextFrame c n) (contextBase c n) (stateMean s n) (fun (y : D) => ↑(s.pressure n y)) (contextVirtual c n) x i

The fixed base error cancels literally; Gaussian and alias errors stay additive.

noncomputable def NavierStokes.HarmonicResidual.residualBlock {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (s : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (gaussian aliasError : BlockCoefficients D) : CorrectionState.HarmonicBlock D

Residual block, bundling velocity, pressure, frequency, phase and the required compatibility proofs.

Equations

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

theorem NavierStokes.HarmonicResidual.BlockRepresentation.goodWaveResidual_eq {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_1} {labels : ℕ → Finset ι} {blocks : ι → CorrectionState.HarmonicBlock D} {gaussian aliasError : ι → BlockCoefficients D} {s : CorrectionState.State D} (hrep : BlockRepresentation labels blocks gaussian aliasError s) (c : CorrectionState.Context D) (n : ℕ) (x : D × ℝ) (i : Fin 3) : stateGoodWaveResidual c s n x i = goodWaveResidual (labels n) (fun (l : ι) => ofBlock (blocks l) (gaussian l) (aliasError l) n) (contextFrame c n) (contextBase c n) (stateMean s n) (fun (y : D) => ↑(s.pressure n y)) (contextVirtual c n) x i

structure NavierStokes.HarmonicResidual.ExtractionRegular {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_1} (U : Set D) (c : CorrectionState.Context D) (s : CorrectionState.State D) (labels : ℕ → Finset ι) (blockFamily : ι → CorrectionState.HarmonicBlock D) (gaussianCoeffs aliasCoeffs : ι → BlockCoefficients D) (n : ℕ) : Prop

Conditions on the actual graph, represented fields, and actual closed supports.

• frame : (contextFrame c n).Regular U
• base (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (x : D) => contextBase c n x i) U
• mean (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (x : D) => stateMean s n x i) U
• pressure : ContDiffOn ℝ (↑⊤) (s.pressure n) U
• blocks (l : ι) : l ∈ labels n → (ofBlock (blockFamily l) (gaussianCoeffs l) (aliasCoeffs l) n).Regular U
• gaussian (l : ι) : l ∈ labels n → ∀ (i : Fin 3), SmoothCoefficients U (gaussianCoeffs l n i)
• aliasError (l : ι) : l ∈ labels n → ∀ (i : Fin 3), SmoothCoefficients U (aliasCoeffs l n i)
• disjoint (l : ι) : l ∈ labels n → ∀ j ∈ labels n, l ≠ j → Disjoint (tsupport ((blockFamily l).oscillation n)) (tsupport ((blockFamily j).oscillation n))
• angular_nonzero (l : ι) : l ∈ labels n → (blockFamily l).angularFrequency n ≠ 0

theorem NavierStokes.HarmonicResidual.ExtractionRegular.dataDisjoint {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_1} {U : Set D} {c : CorrectionState.Context D} {s : CorrectionState.State D} {labels : ℕ → Finset ι} {blocks : ι → CorrectionState.HarmonicBlock D} {gaussian aliasError : ι → BlockCoefficients D} {n : ℕ} (h : ExtractionRegular U c s labels blocks gaussian aliasError n) (l : ι) : l ∈ labels n → ∀ j ∈ labels n, l ≠ j → Disjoint (tsupport (ofBlock (blocks l) (gaussian l) (aliasError l) n).wave) (tsupport (ofBlock (blocks j) (gaussian j) (aliasError j) n).wave)

theorem NavierStokes.HarmonicResidual.stateGoodWaveResidual_grouped {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_1} {U : Set D} (hU : IsOpen U) {c : CorrectionState.Context D} {s : CorrectionState.State D} {labels : ℕ → Finset ι} {blocks : ι → CorrectionState.HarmonicBlock D} {gaussian aliasError : ι → BlockCoefficients D} (hrep : BlockRepresentation labels blocks gaussian aliasError s) {n : ℕ} (h : ExtractionRegular U c s labels blocks gaussian aliasError n) {x : D × ℝ} (hx : x ∈ liftDomain U) (i : Fin 3) : stateGoodWaveResidual c s n x i = ∑ l ∈ labels n, (residualBlock c s (blocks l) (gaussian l) (aliasError l)).oscillation n x i

The forcing supplied to each copy solve consists of the actual nonconstant PDE coefficients. Finite active sets can change with n.

noncomputable def NavierStokes.HarmonicResidual.stateMeanCoefficientValue {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_1} (labels : ℕ → Finset ι) (blocks : ι → CorrectionState.HarmonicBlock D) (gaussian aliasError : ι → BlockCoefficients D) (c : CorrectionState.Context D) (s : CorrectionState.State D) (n : ℕ) (x : D) (i : Fin 3) : ℝ

State mean coefficient value, constructed using meanResidualValue.

Equations

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

theorem NavierStokes.HarmonicResidual.stateMeanCoefficientValue_eq_average {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_1} {U : Set D} (hU : IsOpen U) {c : CorrectionState.Context D} {s : CorrectionState.State D} {labels : ℕ → Finset ι} {blocks : ι → CorrectionState.HarmonicBlock D} {gaussian aliasError : ι → BlockCoefficients D} (hrep : BlockRepresentation labels blocks gaussian aliasError s) {n : ℕ} (h : ExtractionRegular U c s labels blocks gaussian aliasError n) {x : D} (hx : x ∈ U) (i : Fin 3) : stateMeanCoefficientValue labels blocks gaussian aliasError c s n x i = CorrectionState.angularAverage (fun (m : ℕ) (y : D × ℝ) => stateGoodResidual c s m y i) n x

The selected zero mode is the actual angular mean of the stored good residual.

theorem NavierStokes.HarmonicResidual.residualBlock_band {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (s : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (gaussian aliasError : BlockCoefficients D) {N E : ℕ} (hb : b.BandLimited N) (hg : ∀ (n : ℕ) (i : Fin 3), HarmonicFields.BandLimited (gaussian n i) E) (ha : ∀ (n : ℕ) (i : Fin 3), HarmonicFields.BandLimited (aliasError n i) E) : (residualBlock c s b gaussian aliasError).BandLimited (max (N + N) E)

theorem NavierStokes.HarmonicResidual.residualBlock_conjugate {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (s : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (gaussian aliasError : BlockCoefficients D) (n : ℕ) (i : Fin 3) : HarmonicFields.ConjugateSymmetric ((residualBlock c s b gaussian aliasError).velocity n i)

theorem NavierStokes.HarmonicResidual.residualBlock_zero_mode {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (s : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (gaussian aliasError : BlockCoefficients D) (n : ℕ) (i : Fin 3) : ((residualBlock c s b gaussian aliasError).velocity n i).coeff 0 = 0

theorem NavierStokes.HarmonicResidual.residualBlock_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_1} {U : Set D} (hU : IsOpen U) {c : CorrectionState.Context D} {s : CorrectionState.State D} {labels : ℕ → Finset ι} {blocks : ι → CorrectionState.HarmonicBlock D} {gaussian aliasError : ι → BlockCoefficients D} {n : ℕ} (h : ExtractionRegular U c s labels blocks gaussian aliasError n) {l : ι} (hl : l ∈ labels n) (i : Fin 3) : SmoothCoefficients U ((residualBlock c s (blocks l) (gaussian l) (aliasError l)).velocity n i)

theorem NavierStokes.HarmonicResidual.residualBlock_values {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (s : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (gaussian aliasError : BlockCoefficients D) {N E : ℕ} (hb : b.BandLimited N) (hg : ∀ (n : ℕ) (i : Fin 3), HarmonicFields.BandLimited (gaussian n i) E) (ha : ∀ (n : ℕ) (i : Fin 3), HarmonicFields.BandLimited (aliasError n i) E) (n : ℕ) (i : Fin 3) (j : ℤ) (hj : j ∈ ((residualBlock c s b gaussian aliasError).velocity n i).support) : j ≠ 0 ∧ j.natAbs ≤ max (N + N) E

theorem NavierStokes.HarmonicResidual.residualBlock_stage_band {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (s : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (gaussian aliasError : BlockCoefficients D) (stage : ℕ) (hb : b.BandLimited (2 ^ stage)) (hg : ∀ (n : ℕ) (i : Fin 3), HarmonicFields.BandLimited (gaussian n i) (2 ^ (stage + 1))) (ha : ∀ (n : ℕ) (i : Fin 3), HarmonicFields.BandLimited (aliasError n i) (2 ^ (stage + 1))) : (residualBlock c s b gaussian aliasError).BandLimited (2 ^ (stage + 1))

A fixed stage can have large harmonic values, but the next quadratic stage has an explicit bound independent of band and label count.

theorem NavierStokes.HarmonicResidual.residualBlock_extract {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (s : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (gaussian aliasError : BlockCoefficients D) (n : ℕ) (hkp : b.angularFrequency n ≠ 0) (i : Fin 3) (j : ℤ) (x : D) : extract (fun (y : D × ℝ) => ↑((residualBlock c s b gaussian aliasError).oscillation n y i)) (b.frequency n) (b.phase n) (b.angularFrequency n) j x = ((residualBlock c s b gaussian aliasError).velocity n i).coeff j x

theorem NavierStokes.HarmonicResidual.residualBlock_mean_zero {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (s : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (gaussian aliasError : BlockCoefficients D) (n : ℕ) (hkp : b.angularFrequency n ≠ 0) (i : Fin 3) (x : D) : CorrectionState.angularAverage (fun (m : ℕ) (y : D × ℝ) => (residualBlock c s b gaussian aliasError).oscillation m y i) n x = 0

theorem NavierStokes.HarmonicResidual.stateFullResidual_reconstructed {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_1} {U : Set D} (hU : IsOpen U) {c : CorrectionState.Context D} {s : CorrectionState.State D} {labels : ℕ → Finset ι} {blocks : ι → CorrectionState.HarmonicBlock D} {gaussian aliasError : ι → BlockCoefficients D} (hrep : BlockRepresentation labels blocks gaussian aliasError s) {n : ℕ} (h : ExtractionRegular U c s labels blocks gaussian aliasError n) {x : D × ℝ} (hx : x ∈ liftDomain U) (i : Fin 3) : stateFullResidual c s n x i = ∑ l ∈ labels n, (residualBlock c s (blocks l) (gaussian l) (aliasError l)).oscillation n x i + stateMeanCoefficientValue labels blocks gaussian aliasError c s n x.1 i + s.errors.total n x i

Reconstruction of the full differentiated residual, with every excluded error restored once.

theorem NavierStokes.HarmonicResidual.contextFrame_regular {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (c : CorrectionState.Context D) (n : ℕ) (hR : ContDiffOn ℝ (↑⊤) c.operators.radius U) (hRn : ∀ x ∈ U, c.operators.radius x ≠ 0) (hprofile : ContDiffOn ℝ (↑⊤) c.operators.radialProfile U) : (contextFrame c n).Regular U

The actual graph formula gives smooth directions whenever its primitive radius and radial profile are smooth on the annular domain.