Actual particular-wave assembly

The residual source is the coefficient of HarmonicResidual.residualBlock. All signed nonzero harmonics are retained inside their original spatial label. A fixed reference solve supplies the compatible band views.

noncomputable def NavierStokes.ParticularWaveAssembly.modes (N : ℕ) : Finset ℤ

One finite signed harmonic range, without the mean coefficient.

Equations

• NavierStokes.ParticularWaveAssembly.modes N = (Finset.Icc (-↑N) ↑N).erase 0

@[simp]

theorem NavierStokes.ParticularWaveAssembly.mem_modes (N : ℕ) (j : ℤ) : j ∈ modes N ↔ j ≠ 0 ∧ j.natAbs ≤ N

theorem NavierStokes.ParticularWaveAssembly.neg_mem_modes (N : ℕ) (j : ℤ) : -j ∈ modes N ↔ j ∈ modes N

theorem NavierStokes.ParticularWaveAssembly.pair_apply {D : Type} (j m : ℤ) (a : D → ℂ) (x : D) : (ErrorHarmonics.conjugatePair j a).coeff m x = (if m = j then a x / 2 else 0) + (starRingEnd ℂ) (if -m = j then a x / 2 else 0)

theorem NavierStokes.ParticularWaveAssembly.signed_pairs_reconstruct {D : Type} (c : HarmonicFields.Coefficients D) (N : ℕ) (hc : HarmonicFields.ConjugateSymmetric c) (h0 : c.coeff 0 = 0) (hN : HarmonicFields.BandLimited c N) : ∑ j ∈ modes N, ErrorHarmonics.conjugatePair j (c.coeff j) = c

Pairing each signed Fourier source introduces no extra factor of two. Every coefficient is recovered exactly, including the absent mean.

noncomputable def NavierStokes.ParticularWaveAssembly.residualSource {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A : HarmonicResidual.BlockCoefficients D) (j : ℤ) (n : ℕ) (x : D) : HarmonicCalculus.ComplexVector

The actual source coefficient, with no convention-dependent scaling.

Equations

• NavierStokes.ParticularWaveAssembly.residualSource c u b G A j n x i = ((NavierStokes.HarmonicResidual.residualBlock c u b G A).velocity n i).coeff j x

theorem NavierStokes.ParticularWaveAssembly.residualSource_zero {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A : HarmonicResidual.BlockCoefficients D) (n : ℕ) (x : D) : residualSource c u b G A 0 n x = 0

theorem NavierStokes.ParticularWaveAssembly.residualSource_conjugate {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A : HarmonicResidual.BlockCoefficients D) (j : ℤ) (n : ℕ) (x : D) (i : Fin 3) : residualSource c u b G A (-j) n x i = (starRingEnd ℂ) (residualSource c u b G A j n x i)

noncomputable def NavierStokes.ParticularWaveAssembly.modeBlock {D : Type} (j : ℤ) (k : ℕ → ℝ) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (v : ℕ → D → HarmonicCalculus.ComplexVector) (p : ℕ → D → ℂ) : CorrectionState.HarmonicBlock D

A pair at the original label's carrier, for both velocity and pressure.

Equations

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

theorem NavierStokes.ParticularWaveAssembly.modeBlock_band {D : Type} (j : ℤ) (k : ℕ → ℝ) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (v : ℕ → D → HarmonicCalculus.ComplexVector) (p : ℕ → D → ℂ) : (modeBlock j k Φ kp v p).BandLimited j.natAbs

theorem NavierStokes.ParticularWaveAssembly.modeBlock_real {D : Type} (j : ℤ) (k : ℕ → ℝ) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (v : ℕ → D → HarmonicCalculus.ComplexVector) (p : ℕ → D → ℂ) : ErrorHarmonics.RealBlock (modeBlock j k Φ kp v p)

theorem NavierStokes.ParticularWaveAssembly.modeBlock_zero {D : Type} {j : ℤ} (hj : j ≠ 0) (k : ℕ → ℝ) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (v : ℕ → D → HarmonicCalculus.ComplexVector) (p : ℕ → D → ℂ) : (∀ (n : ℕ) (i : Fin 3), ((modeBlock j k Φ kp v p).velocity n i).coeff 0 = 0) ∧ ∀ (n : ℕ), ((modeBlock j k Φ kp v p).pressure n).coeff 0 = 0

theorem NavierStokes.ParticularWaveAssembly.pair_class {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {a : ℕ → D → ℂ} (ha : WeightedClasses.MemClass s w α a) (j m : ℤ) : WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => (ErrorHarmonics.conjugatePair j (a n)).coeff m x

theorem NavierStokes.ParticularWaveAssembly.modeBlock_classes {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {W : ℕ → D → ℝ} {α γ : ℝ} (j : ℤ) (k : ℕ → ℝ) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) {v : ℕ → D → HarmonicCalculus.ComplexVector} {p : ℕ → D → ℂ} (hv : WeightedClasses.WaveClass s W α v) (hp : WeightedClasses.WaveClass s W γ p) : CorrectionState.HarmonicBlock.WaveBounds s W α (modeBlock j k Φ kp v p) ∧ CorrectionState.HarmonicBlock.PressureBounds s W γ (modeBlock j k Φ kp v p)

noncomputable def NavierStokes.ParticularWaveAssembly.assembledBlock {D : Type} (N : ℕ) (k : ℕ → ℝ) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (v : ℤ → ℕ → D → HarmonicCalculus.ComplexVector) (p : ℤ → ℕ → D → ℂ) : CorrectionState.HarmonicBlock D

Assembled block, given by sumBlock (modes N) k Φ kp (fun j => modeBlock j k Φ kp (v j) (p j)).

Equations

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

theorem NavierStokes.ParticularWaveAssembly.assembledBlock_band {D : Type} (N : ℕ) (k : ℕ → ℝ) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (v : ℤ → ℕ → D → HarmonicCalculus.ComplexVector) (p : ℤ → ℕ → D → ℂ) : (assembledBlock N k Φ kp v p).BandLimited N

theorem NavierStokes.ParticularWaveAssembly.assembledBlock_real {D : Type} (N : ℕ) (k : ℕ → ℝ) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (v : ℤ → ℕ → D → HarmonicCalculus.ComplexVector) (p : ℤ → ℕ → D → ℂ) : ErrorHarmonics.RealBlock (assembledBlock N k Φ kp v p)

theorem NavierStokes.ParticularWaveAssembly.residualSource_reconstruct {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A : HarmonicResidual.BlockCoefficients D) (N : ℕ) (hN : (HarmonicResidual.residualBlock c u b G A).BandLimited N) (n : ℕ) (i : Fin 3) : (assembledBlock N b.frequency b.phase b.angularFrequency (residualSource c u b G A) fun (x : ℤ) (x_1 : ℕ) (x_2 : D) => 0).velocity n i = (HarmonicResidual.residualBlock c u b G A).velocity n i

Reassemble the actual signed residual sources, without changing label, phase, frequency, or normalization.

A fixed native clock and reference geometry

noncomputable def NavierStokes.ParticularWaveAssembly.transportTangent {P Q H : Type} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (t : CommonCoverSolve.TangentData P H) (φ : Q → P) (gap : ℕ) (amplitude : ℝ) : CommonCoverSolve.TangentData Q H

Transport only the input data. The physical native clock and anchor are retained, and the cover is refined by a specified integer power.

Equations

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

theorem NavierStokes.ParticularWaveAssembly.transportTangent_linearData {P Q H : Type} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (t : CommonCoverSolve.TangentData P H) (φ : Q → P) (gap : ℕ) (amplitude : ℝ) : (transportTangent t φ gap amplitude).linearData = CopySolveCompatibility.scaleSource (CopySolveCompatibility.transformData t.linearData φ gap) amplitude

theorem NavierStokes.ParticularWaveAssembly.copySolve_transport {P Q H : Type} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (t : CommonCoverSolve.TangentData P H) (φ : Q → P) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (gap : ℕ) (amplitude : ℝ) (copy : TorusInverse.Frequency) (q : Q) (Y : TorusInverse.Plane) : (transportTangent t φ gap amplitude).linearData.copySolve (CopySolveCompatibility.refineGeometry g gap) hab copy (q, Y) = amplitude • t.linearData.copySolve g hab copy (φ q, (CommonCoverSolve.coverPower gap) Y)

theorem NavierStokes.ParticularWaveAssembly.commonSolve_transport {P Q H : Type} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (t : CommonCoverSolve.TangentData P H) (φ : Q → P) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (gap : ℕ) (amplitude : ℝ) (κ : TorusInverse.Plane → ℝ) (q : Q) (Y : TorusInverse.Plane) : (transportTangent t φ gap amplitude).linearData.commonSolve (CopySolveCompatibility.refineGeometry g gap) hab κ (q, Y) = amplitude • t.linearData.commonSolve g hab κ (φ q, (CommonCoverSolve.coverPower gap) Y)

All transported views equal a pullback of one actual common-cover Volterra output; no chartwise output is supplied as a hypothesis.

theorem NavierStokes.ParticularWaveAssembly.copyPressureReal_transport {P Q H : Type} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (t : CommonCoverSolve.TangentData P H) (φ : Q → P) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (gap : ℕ) (amplitude : ℝ) (copy : TorusInverse.Frequency) (q : Q) (Y : TorusInverse.Plane) : ParticularWaveBounds.copyPressureReal (transportTangent t φ gap amplitude) (CopySolveCompatibility.refineGeometry g gap) hab copy (q, Y) = amplitude * ParticularWaveBounds.copyPressureReal t g hab copy (φ q, (CommonCoverSolve.coverPower gap) Y)

theorem NavierStokes.ParticularWaveAssembly.copyPressure_transport {P Q H : Type} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (t : CommonCoverSolve.TangentData P H) (φ : Q → P) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (gap : ℕ) (amplitude referenceFrequency frequency : ℝ) (hreference : referenceFrequency ≠ 0) (hfrequency : frequency ≠ 0) (copy : TorusInverse.Frequency) (q : Q) (Y : TorusInverse.Plane) : ParticularWaveBounds.copyPressure (transportTangent t φ gap amplitude) (CopySolveCompatibility.refineGeometry g gap) hab copy frequency (q, Y) = (amplitude * referenceFrequency / frequency) • ParticularWaveBounds.copyPressure t g hab copy referenceFrequency (φ q, (CommonCoverSolve.coverPower gap) Y)

Pressure transports with its own inverse carrier frequency.

Full angular fields and grouped coefficient classes

theorem NavierStokes.ParticularWaveAssembly.assembledBlock_zero {D : Type} (N : ℕ) (k : ℕ → ℝ) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (v : ℤ → ℕ → D → HarmonicCalculus.ComplexVector) (p : ℤ → ℕ → D → ℂ) : (∀ (n : ℕ) (i : Fin 3), ((assembledBlock N k Φ kp v p).velocity n i).coeff 0 = 0) ∧ ∀ (n : ℕ), ((assembledBlock N k Φ kp v p).pressure n).coeff 0 = 0

theorem NavierStokes.ParticularWaveAssembly.assembledBlock_classes {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {W : ℕ → D → ℝ} {α γ : ℝ} (N : ℕ) (k : ℕ → ℝ) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) {v : ℤ → ℕ → D → HarmonicCalculus.ComplexVector} {p : ℤ → ℕ → D → ℂ} (hW : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W n x) (hv : ∀ j ∈ modes N, WeightedClasses.WaveClass s W α (v j)) (hp : ∀ j ∈ modes N, WeightedClasses.WaveClass s W γ (p j)) : CorrectionState.HarmonicBlock.WaveBounds s W α (assembledBlock N k Φ kp v p) ∧ CorrectionState.HarmonicBlock.PressureBounds s W γ (assembledBlock N k Φ kp v p)

theorem NavierStokes.ParticularWaveAssembly.assembledBlock_mean_zero {D : Type} (N : ℕ) (k : ℕ → ℝ) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (v : ℤ → ℕ → D → HarmonicCalculus.ComplexVector) (p : ℤ → ℕ → D → ℂ) (hkp : ∀ (n : ℕ), kp n ≠ 0) : (∀ (i : Fin 3), (CorrectionState.angularAverage fun (n : ℕ) (x : D × ℝ) => (assembledBlock N k Φ kp v p).oscillation n x i) = 0) ∧ CorrectionState.angularAverage (assembledBlock N k Φ kp v p).oscillatoryPressure = 0

noncomputable def NavierStokes.ParticularWaveAssembly.fullModeBlock {D : Type} (j : ℤ) (k : ℕ → ℝ) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (a : LinearWaveBounds.WaveCoefficients (D × ℝ)) : CorrectionState.HarmonicBlock D

Full mode block, given by modeBlock j k Φ kp (fun n x => a.amplitude n (x,0)) (fun n x => a.pressure n (x,0)).

Equations

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

theorem NavierStokes.ParticularWaveAssembly.fullModeBlock_represents {D : Type} (j : ℤ) (k : ℕ → ℝ) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (a : LinearWaveBounds.WaveCoefficients (D × ℝ)) (ha : ErrorHarmonics.AngleIndependent a.amplitude) (hp : ErrorHarmonics.AngleIndependent a.pressure) (hphase : ∀ (n : ℕ) (x : D) (θ : ℝ), a.frequency n * a.phase n (x, θ) = ↑j * (k n * Φ n x + ↑(kp n) * θ)) : ((fullModeBlock j k Φ kp a).oscillation = fun (n : ℕ) (x : D × ℝ) (i : Fin 3) => (HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) (a.amplitude n) x i).re) ∧ (fullModeBlock j k Φ kp a).oscillatoryPressure = fun (n : ℕ) (x : D × ℝ) => (HarmonicCalculus.mode (a.frequency n) (a.phase n) (a.pressure n) x).re

theorem NavierStokes.ParticularWaveAssembly.fullModeBlock_classes {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData (D × ℝ)} {W : ℕ → D × ℝ → ℝ} {α γ : ℝ} (j : ℤ) (k : ℕ → ℝ) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (a : LinearWaveBounds.WaveCoefficients (D × ℝ)) (ha : WeightedClasses.WaveClass s W α a.amplitude) (hp : WeightedClasses.WaveClass s W γ a.pressure) : CorrectionState.HarmonicBlock.WaveBounds (SignedWaveUpdate.sectionStrip s) (fun (n : ℕ) (x : D) => W n (x, 0)) α (fullModeBlock j k Φ kp a) ∧ CorrectionState.HarmonicBlock.PressureBounds (SignedWaveUpdate.sectionStrip s) (fun (n : ℕ) (x : D) => W n (x, 0)) γ (fullModeBlock j k Φ kp a)

Complex reference transport, including pressure

noncomputable def NavierStokes.ParticularWaveAssembly.transportSource {P Q : Type} (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (φ : Q → P) (gap : ℕ) (amplitude : ℝ) : Q × TorusInverse.Plane → HarmonicCalculus.ComplexVector

Transport source, defined pointwise by amplitude • f (φ q.1, coverPower gap q.2).

Equations

• NavierStokes.ParticularWaveAssembly.transportSource f φ gap amplitude q = amplitude • f (φ q.1, (NavierStokes.CommonCoverSolve.coverPower gap) q.2)

theorem NavierStokes.ParticularWaveAssembly.realData_transport {P Q : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (φ : Q → P) (gap : ℕ) (amplitude : ℝ) : ParticularWaveBounds.realData (transportTangent t φ gap amplitude) (transportSource f φ gap amplitude) = transportTangent (ParticularWaveBounds.realData t f) φ gap amplitude

theorem NavierStokes.ParticularWaveAssembly.imagData_transport {P Q : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (φ : Q → P) (gap : ℕ) (amplitude : ℝ) : ParticularWaveBounds.imagData (transportTangent t φ gap amplitude) (transportSource f φ gap amplitude) = transportTangent (ParticularWaveBounds.imagData t f) φ gap amplitude

theorem NavierStokes.ParticularWaveAssembly.copyVelocity_transport {P Q : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (φ : Q → P) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (gap : ℕ) (amplitude : ℝ) (copy : TorusInverse.Frequency) (q : Q) (Y : TorusInverse.Plane) : ParticularWaveBounds.copyVelocity (transportTangent t φ gap amplitude) (CopySolveCompatibility.refineGeometry g gap) hab copy (q, Y) = amplitude • ParticularWaveBounds.copyVelocity t g hab copy (φ q, (CommonCoverSolve.coverPower gap) Y)

theorem NavierStokes.ParticularWaveAssembly.complexCopyVelocity_transport {P Q : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (φ : Q → P) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (gap : ℕ) (amplitude : ℝ) (copy : TorusInverse.Frequency) (q : Q) (Y : TorusInverse.Plane) : ParticularWaveBounds.complexCopyVelocity (transportTangent t φ gap amplitude) (transportSource f φ gap amplitude) (CopySolveCompatibility.refineGeometry g gap) hab copy (q, Y) = amplitude • ParticularWaveBounds.complexCopyVelocity t f g hab copy (φ q, (CommonCoverSolve.coverPower gap) Y)

theorem NavierStokes.ParticularWaveAssembly.complexCopyPressure_transport {P Q : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (φ : Q → P) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (gap : ℕ) (amplitude referenceFrequency frequency : ℝ) (hreference : referenceFrequency ≠ 0) (hfrequency : frequency ≠ 0) (copy : TorusInverse.Frequency) (q : Q) (Y : TorusInverse.Plane) : ParticularWaveBounds.complexCopyPressure (transportTangent t φ gap amplitude) (transportSource f φ gap amplitude) (CopySolveCompatibility.refineGeometry g gap) hab copy frequency (q, Y) = (amplitude * referenceFrequency / frequency) • ParticularWaveBounds.complexCopyPressure t f g hab copy referenceFrequency (φ q, (CommonCoverSolve.coverPower gap) Y)

theorem NavierStokes.ParticularWaveAssembly.periodizedCopies_transport {P Q H : Type} [NormedAddCommGroup H] [NormedSpace ℝ H] (g : CommonCoverSolve.Geometry) (κ : TorusInverse.Plane → ℝ) (F : TorusInverse.Frequency → P × TorusInverse.Plane → H) (φ : Q → P) (gap : ℕ) (amplitude : ℝ) (q : Q) (Y : TorusInverse.Plane) : ParticularWaveBounds.periodizedCopies (CopySolveCompatibility.refineGeometry g gap) κ (fun (k : TorusInverse.Frequency) (q : Q × TorusInverse.Plane) => amplitude • F k (φ q.1, (CommonCoverSolve.coverPower gap) q.2)) (q, Y) = amplitude • ParticularWaveBounds.periodizedCopies g κ F (φ q, (CommonCoverSolve.coverPower gap) Y)

theorem NavierStokes.ParticularWaveAssembly.commonVelocity_transport {P Q : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (φ : Q → P) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (gap : ℕ) (amplitude : ℝ) (κ : TorusInverse.Plane → ℝ) (q : Q) (Y : TorusInverse.Plane) : ParticularWaveBounds.commonVelocity (transportTangent t φ gap amplitude) (transportSource f φ gap amplitude) (CopySolveCompatibility.refineGeometry g gap) hab κ (q, Y) = amplitude • ParticularWaveBounds.commonVelocity t f g hab κ (φ q, (CommonCoverSolve.coverPower gap) Y)

theorem NavierStokes.ParticularWaveAssembly.commonPressure_transport {P Q : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (φ : Q → P) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (gap : ℕ) (amplitude referenceFrequency frequency : ℝ) (hreference : referenceFrequency ≠ 0) (hfrequency : frequency ≠ 0) (κ : TorusInverse.Plane → ℝ) (q : Q) (Y : TorusInverse.Plane) : ParticularWaveBounds.commonPressure (transportTangent t φ gap amplitude) (transportSource f φ gap amplitude) (CopySolveCompatibility.refineGeometry g gap) hab κ frequency (q, Y) = (amplitude * referenceFrequency / frequency) • ParticularWaveBounds.commonPressure t f g hab κ referenceFrequency (φ q, (CommonCoverSolve.coverPower gap) Y)

One physical reference for every band view

structure NavierStokes.ParticularWaveAssembly.Reference (P : Type) : Type

The choices are made once for a spatial label. The native interval, center, cover, and cutoff are shared by all its band views and harmonics.

• band : ℕ

  Band of Reference, of type ℕ.

• geometry : CommonCoverSolve.Geometry

  Geometry of Reference, of type Geometry.

• length : ℝ

  Length of Reference, of type ℝ.

• length_pos : 0 < self.length
• tangent : ℤ → CommonCoverSolve.TangentData P ProblemStatement.Space

  Tangent of Reference, of type ℤ → TangentData P ProblemStatement.Space.

• cutoff : TorusInverse.Plane → ℝ

  Cutoff of Reference, of type Plane → ℝ.

• cutoff_compact : HasCompactSupport self.cutoff

structure NavierStokes.ParticularWaveAssembly.BandCharts (P : Type) : Type

Only chart/source input data, never an independently chosen solution.

• parameter : ℕ → P → P

  Parameter of BandCharts, of type ℕ → P → P.

• gap : ℕ → ℕ

  Gap of BandCharts, of type ℕ → ℕ.

• amplitude : ℕ → ℝ

  Amplitude of BandCharts, of type ℕ → ℝ.

noncomputable def NavierStokes.ParticularWaveAssembly.referenceVelocity {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : Reference P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector

Reference velocity, given by commonVelocity (r.tangent j) (residualSource c u b G A j r.band) r.geometry r.length_pos.le r.cutoff.

Equations

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

noncomputable def NavierStokes.ParticularWaveAssembly.referencePressure {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : Reference P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) : P × TorusInverse.Plane → ℂ

Reference pressure, constructed using commonPressure.

Equations

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

noncomputable def NavierStokes.ParticularWaveAssembly.bandTangent {P : Type} (r : Reference P) (charts : BandCharts P) (j : ℤ) (n : ℕ) : CommonCoverSolve.TangentData P ProblemStatement.Space

Band tangent, given by transportTangent (r.tangent j) (charts.parameter n) (charts.gap n) (charts.amplitude n).

Equations

• NavierStokes.ParticularWaveAssembly.bandTangent r charts j n = NavierStokes.ParticularWaveAssembly.transportTangent (r.tangent j) (charts.parameter n) (charts.gap n) (charts.amplitude n)

noncomputable def NavierStokes.ParticularWaveAssembly.bandGeometry {P : Type} (r : Reference P) (charts : BandCharts P) (n : ℕ) : CommonCoverSolve.Geometry

Band geometry, given by CopySolveCompatibility.refineGeometry r.geometry (charts.gap n).

Equations

• NavierStokes.ParticularWaveAssembly.bandGeometry r charts n = NavierStokes.CopySolveCompatibility.refineGeometry r.geometry (charts.gap n)

noncomputable def NavierStokes.ParticularWaveAssembly.actualBandVelocity {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : Reference P) (charts : BandCharts P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (n : ℕ) : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector

Actual band velocity, given by commonVelocity (bandTangent r charts j n) (residualSource c u b G A j n) (bandGeometry r charts n) r.length_pos.le r.cutoff.

Equations

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

noncomputable def NavierStokes.ParticularWaveAssembly.actualBandPressure {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : Reference P) (charts : BandCharts P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (n : ℕ) : P × TorusInverse.Plane → ℂ

Actual band pressure, constructed using commonPressure.

Equations

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

theorem NavierStokes.ParticularWaveAssembly.actualBandVelocity_eq_reference {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : Reference P) (charts : BandCharts P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (n : ℕ) (hsource : residualSource c u b G A j n = transportSource (residualSource c u b G A j r.band) (charts.parameter n) (charts.gap n) (charts.amplitude n)) (p : P) (Y : TorusInverse.Plane) : actualBandVelocity r charts c u b G A j n (p, Y) = charts.amplitude n • referenceVelocity r c u b G A j (charts.parameter n p, (CommonCoverSolve.coverPower (charts.gap n)) Y)

Compatibility is required only of the actual residual source inputs. Uniqueness of the fixed-reference Volterra construction then gives the physical output identity.

theorem NavierStokes.ParticularWaveAssembly.actualBandPressure_eq_reference {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : Reference P) (charts : BandCharts P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) {j : ℤ} (hj : j ≠ 0) (n : ℕ) (hfrequency : ∀ (n : ℕ), b.frequency n ≠ 0) (hsource : residualSource c u b G A j n = transportSource (residualSource c u b G A j r.band) (charts.parameter n) (charts.gap n) (charts.amplitude n)) (p : P) (Y : TorusInverse.Plane) : actualBandPressure r charts c u b G A j n (p, Y) = (charts.amplitude n * b.frequency r.band / b.frequency n) • referencePressure r c u b G A j (charts.parameter n p, (CommonCoverSolve.coverPower (charts.gap n)) Y)

theorem NavierStokes.ParticularWaveAssembly.referenceVelocity_finite {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : Reference P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (p : P × TorusInverse.Plane) : ∃ (I : Finset TorusInverse.Frequency), referenceVelocity r c u b G A j p = ∑ k ∈ I, r.cutoff (r.geometry.coordinates k p.2) • ParticularWaveBounds.complexCopyVelocity (r.tangent j) (residualSource c u b G A j r.band) r.geometry ⋯ k p

theorem NavierStokes.ParticularWaveAssembly.referencePressure_finite {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : Reference P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (p : P × TorusInverse.Plane) : ∃ (I : Finset TorusInverse.Frequency), referencePressure r c u b G A j p = ∑ k ∈ I, r.cutoff (r.geometry.coordinates k p.2) • ParticularWaveBounds.complexCopyPressure (r.tangent j) (residualSource c u b G A j r.band) r.geometry ⋯ k (↑j * b.frequency r.band) p

Angular invariance is inherited by the actual complex solve

theorem NavierStokes.ParticularWaveAssembly.complexCopyVelocity_invariant {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {θ : P} {t : CommonCoverSolve.TangentData P ProblemStatement.Space} {source : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector} (ht : CopyAngularInvariance.TangentInvariant θ t) (hs : CopyAngularInvariance.Invariant (θ, 0) source) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (k : TorusInverse.Frequency) : CopyAngularInvariance.Invariant (θ, 0) (ParticularWaveBounds.complexCopyVelocity t source g hab k)

theorem NavierStokes.ParticularWaveAssembly.complexCopyPressure_invariant {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {θ : P} {t : CommonCoverSolve.TangentData P ProblemStatement.Space} {source : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector} (ht : CopyAngularInvariance.TangentInvariant θ t) (hs : CopyAngularInvariance.Invariant (θ, 0) source) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (k : TorusInverse.Frequency) (frequency : ℝ) : CopyAngularInvariance.Invariant (θ, 0) (ParticularWaveBounds.complexCopyPressure t source g hab k frequency)

theorem NavierStokes.ParticularWaveAssembly.commonVelocity_invariant {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {θ : P} {t : CommonCoverSolve.TangentData P ProblemStatement.Space} {source : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector} (ht : CopyAngularInvariance.TangentInvariant θ t) (hs : CopyAngularInvariance.Invariant (θ, 0) source) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) : CopyAngularInvariance.Invariant (θ, 0) (ParticularWaveBounds.commonVelocity t source g hab κ)

theorem NavierStokes.ParticularWaveAssembly.commonPressure_invariant {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {θ : P} {t : CommonCoverSolve.TangentData P ProblemStatement.Space} {source : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector} (ht : CopyAngularInvariance.TangentInvariant θ t) (hs : CopyAngularInvariance.Invariant (θ, 0) source) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) (frequency : ℝ) : CopyAngularInvariance.Invariant (θ, 0) (ParticularWaveBounds.commonPressure t source g hab κ frequency)

noncomputable def NavierStokes.ParticularWaveAssembly.angleLift {P E : Type} (f : P × TorusInverse.Plane → E) : (P × ℝ) × TorusInverse.Plane → E

Angle lift, defined pointwise by f (z.1.1, z.2).

Equations

• NavierStokes.ParticularWaveAssembly.angleLift f z = f (z.1.1, z.2)

theorem NavierStokes.ParticularWaveAssembly.angleLift_invariant {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {E : Type} (f : P × TorusInverse.Plane → E) : CopyAngularInvariance.Invariant ((0, 1), 0) (angleLift f)

noncomputable def NavierStokes.ParticularWaveAssembly.angleTangent {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) : CommonCoverSolve.TangentData (P × ℝ) ProblemStatement.Space

Angle tangent, bundling normal, normalDot, action, damping and the required compatibility proofs.

Equations

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

theorem NavierStokes.ParticularWaveAssembly.angleTangent_invariant {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (t : CommonCoverSolve.TangentData P ProblemStatement.Space) : CopyAngularInvariance.TangentInvariant (0, 1) (angleTangent t)

noncomputable def NavierStokes.ParticularWaveAssembly.angleShuffle {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] : (P × TorusInverse.Plane) × ℝ ≃ₗᵢ[ℝ] (P × ℝ) × TorusInverse.Plane

An isometry retaining the physical angular coordinate, while moving it into the slow-parameter product used by the Volterra construction.

Equations

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

theorem NavierStokes.ParticularWaveAssembly.angleShuffle_apply {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (x : P × TorusInverse.Plane) (θ : ℝ) : angleShuffle (x, θ) = ((x.1, θ), x.2)

theorem NavierStokes.ParticularWaveAssembly.invariant_angleShuffle {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {E : Type} {f : (P × ℝ) × TorusInverse.Plane → E} (hf : CopyAngularInvariance.Invariant ((0, 1), 0) f) (x : P × TorusInverse.Plane) (θ : ℝ) : f (angleShuffle (x, θ)) = f (angleShuffle (x, 0))

Angular invariance of the retained differential error

theorem NavierStokes.ParticularWaveAssembly.principal_invariant {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {θ : E} {R F G Φ : E → ℝ} {Vr Vθ Vz Vf : E → E} {a : E → HarmonicCalculus.ComplexVector} {p : E → ℂ} {m : ℝ} (ε K : ℝ) (hR : CopyAngularInvariance.Invariant θ R) (hF : CopyAngularInvariance.Invariant θ F) (hG : CopyAngularInvariance.Invariant θ G) (hr : CopyAngularInvariance.Invariant θ Vr) (hθ : CopyAngularInvariance.Invariant θ Vθ) (hz : CopyAngularInvariance.Invariant θ Vz) (hf : CopyAngularInvariance.Invariant θ Vf) (hΦ : CopyAngularInvariance.AffinePhase θ m Φ) (ha : CopyAngularInvariance.Invariant θ a) (hp : CopyAngularInvariance.Invariant θ p) : CopyAngularInvariance.Invariant θ (LinearWaveResidual.principal ε K R F G Vr Vθ Vz Vf Φ a p)

theorem NavierStokes.ParticularWaveAssembly.remainder_invariant {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {θ : E} {R b F G Φ : E → ℝ} {Vr Vθ Vz Vf Vs : E → E} {a : E → HarmonicCalculus.ComplexVector} {p : E → ℂ} {m : ℝ} (ε K : ℝ) (hR : CopyAngularInvariance.Invariant θ R) (hb : CopyAngularInvariance.Invariant θ b) (hF : CopyAngularInvariance.Invariant θ F) (hG : CopyAngularInvariance.Invariant θ G) (hr : CopyAngularInvariance.Invariant θ Vr) (hθ : CopyAngularInvariance.Invariant θ Vθ) (hz : CopyAngularInvariance.Invariant θ Vz) (hf : CopyAngularInvariance.Invariant θ Vf) (hs : CopyAngularInvariance.Invariant θ Vs) (hΦ : CopyAngularInvariance.AffinePhase θ m Φ) (ha : CopyAngularInvariance.Invariant θ a) (hp : CopyAngularInvariance.Invariant θ p) : CopyAngularInvariance.Invariant θ (LinearWaveResidual.remainder ε K R b F G Vr Vθ Vz Vf Vs Φ a p)

theorem NavierStokes.ParticularWaveAssembly.constructedGood_invariant {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData E} {d : LinearWaveBounds.GraphDirections E} {a : LinearWaveBounds.WaveCoefficients E} (ψ : ℕ → E → ℝ) (hR : ∀ (n : ℕ), CopyAngularInvariance.Invariant d.angular (a.radius n)) (hb : ∀ (n : ℕ), CopyAngularInvariance.Invariant d.angular (a.radialBase n)) (hF : ∀ (n : ℕ), CopyAngularInvariance.Invariant d.angular (a.frequencyBase n)) (hG : ∀ (n : ℕ), CopyAngularInvariance.Invariant d.angular (a.axialBase n)) (hr : ∀ (n : ℕ), CopyAngularInvariance.Invariant d.angular (d.radialField n)) (hz : ∀ (n : ℕ), CopyAngularInvariance.Invariant d.angular (d.axialField s n)) (hΦ : ∀ (n : ℕ), ∃ (m : ℝ), CopyAngularInvariance.AffinePhase d.angular m (a.phase n)) (ha : ∀ (n : ℕ), CopyAngularInvariance.Invariant d.angular (a.amplitude n)) (hp : ∀ (n : ℕ), CopyAngularInvariance.Invariant d.angular (a.pressure n)) (hψ : ∀ (n : ℕ), CopyAngularInvariance.Invariant d.angular (ψ n)) (n : ℕ) : CopyAngularInvariance.Invariant d.angular (a.constructedGood s d ψ n)

Actual copy localization from an injective padded native chart

theorem NavierStokes.ParticularWaveAssembly.native_coordinate_image (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) : g.center + g.basis (g.coordinates k Y) = TorusAverages.latticePoint (-k) + (CommonCoverSolve.coverPower g.gap) Y

theorem NavierStokes.ParticularWaveAssembly.native_copy_unique (g : CommonCoverSolve.Geometry) {Ω : Set TorusInverse.Plane} (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => g.center + g.basis z) '' Ω)) {k l : TorusInverse.Frequency} {Y : TorusInverse.Plane} (hk : g.coordinates k Y ∈ Ω) (hl : g.coordinates l Y ∈ Ω) : k = l

theorem NavierStokes.ParticularWaveAssembly.periodizedCopies_eq_weighted_single {P H : Type} [NormedAddCommGroup H] [NormedSpace ℝ H] (g : CommonCoverSolve.Geometry) (κ : TorusInverse.Plane → ℝ) (F : TorusInverse.Frequency → P × TorusInverse.Plane → H) {Ω : Set TorusInverse.Plane} (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => g.center + g.basis z) '' Ω)) (hsupp : Function.support κ ⊆ Ω) (k : TorusInverse.Frequency) (p : P × TorusInverse.Plane) (hp : g.coordinates k p.2 ∈ Ω) : ParticularWaveBounds.periodizedCopies g κ F p = κ (g.coordinates k p.2) • F k p

theorem NavierStokes.ParticularWaveAssembly.periodizedCopies_germ {P H : Type} [NormedAddCommGroup P] [NormedAddCommGroup H] [NormedSpace ℝ H] (g : CommonCoverSolve.Geometry) (κ : TorusInverse.Plane → ℝ) (F : TorusInverse.Frequency → P × TorusInverse.Plane → H) {Ω : Set TorusInverse.Plane} (hΩ : IsOpen Ω) (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => g.center + g.basis z) '' Ω)) (hsupp : Function.support κ ⊆ Ω) (k : TorusInverse.Frequency) (p : P × TorusInverse.Plane) (hp : g.coordinates k p.2 ∈ Ω) : ParticularWaveBounds.periodizedCopies g κ F =ᶠ[nhds p] fun (q : P × TorusInverse.Plane) => κ (g.coordinates k q.2) • F k q

The derivative of the native cutoff is preserved. No plateau is assumed for the active copy, so Gaussian edge derivatives are retained.

theorem NavierStokes.ParticularWaveAssembly.periodizedCopies_jets {P H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup H] [NormedSpace ℝ H] (g : CommonCoverSolve.Geometry) (κ : TorusInverse.Plane → ℝ) (F : TorusInverse.Frequency → P × TorusInverse.Plane → H) {Ω : Set TorusInverse.Plane} (hΩ : IsOpen Ω) (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => g.center + g.basis z) '' Ω)) (hsupp : Function.support κ ⊆ Ω) (k : TorusInverse.Frequency) (p : P × TorusInverse.Plane) (hp : g.coordinates k p.2 ∈ Ω) (m : ℕ) : iteratedFDeriv ℝ m (ParticularWaveBounds.periodizedCopies g κ F) p = iteratedFDeriv ℝ m (fun (q : P × TorusInverse.Plane) => κ (g.coordinates k q.2) • F k q) p

The forced coefficients from the literal residual source

theorem NavierStokes.ParticularWaveAssembly.angleTangent_eq_transport {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) : angleTangent t = transportTangent t Prod.fst 0 1

theorem NavierStokes.ParticularWaveAssembly.angleSource_eq_transport {P : Type} (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) : angleLift f = transportSource f Prod.fst 0 1

theorem NavierStokes.ParticularWaveAssembly.complexCopyVelocity_angle {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (source : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (copy : TorusInverse.Frequency) (p : P) (θ : ℝ) (Y : TorusInverse.Plane) : ParticularWaveBounds.complexCopyVelocity (angleTangent t) (angleLift source) g hab copy ((p, θ), Y) = ParticularWaveBounds.complexCopyVelocity t source g hab copy (p, Y)

theorem NavierStokes.ParticularWaveAssembly.complexCopyPressure_angle {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (source : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (copy : TorusInverse.Frequency) {K : ℝ} (hK : K ≠ 0) (p : P) (θ : ℝ) (Y : TorusInverse.Plane) : ParticularWaveBounds.complexCopyPressure (angleTangent t) (angleLift source) g hab copy K ((p, θ), Y) = ParticularWaveBounds.complexCopyPressure t source g hab copy K (p, Y)

noncomputable def NavierStokes.ParticularWaveAssembly.actualCarrier {P : Type} (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (j : ℤ) : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)

Frequency and phase are constructed from the original residual block. Only the background fields of base are retained.

Equations

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

theorem NavierStokes.ParticularWaveAssembly.actualCarrier_phase {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (j : ℤ) (hfrequency : ∀ (n : ℕ), b.frequency n ≠ 0) (n : ℕ) (x : P × TorusInverse.Plane) (θ : ℝ) : (actualCarrier base b j).frequency n * (actualCarrier base b j).phase n (angleShuffle (x, θ)) = ↑j * (b.frequency n * b.phase n x + ↑(b.angularFrequency n) * θ)

theorem NavierStokes.ParticularWaveAssembly.actualCarrier_affine {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (j : ℤ) (n : ℕ) : CopyAngularInvariance.AffinePhase ((0, 1), 0) (↑(b.angularFrequency n) / b.frequency n) ((actualCarrier base b j).phase n)

noncomputable def NavierStokes.ParticularWaveAssembly.actualCopyCoefficients {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : Reference P) (charts : BandCharts P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (copy : ℕ → TorusInverse.Frequency) : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)

Actual copy coefficients, constructed using complexCopyCoefficients.

Equations

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

noncomputable def NavierStokes.ParticularWaveAssembly.actualCommonCoefficients {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : Reference P) (charts : BandCharts P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)

Actual common coefficients as an element of WaveCoefficients ((P × ℝ) × Plane).

Equations

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

theorem NavierStokes.ParticularWaveAssembly.actualCopy_amplitude_invariant {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : Reference P) (charts : BandCharts P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (copy : ℕ → TorusInverse.Frequency) (n : ℕ) : CopyAngularInvariance.Invariant ((0, 1), 0) ((actualCopyCoefficients r charts c u b G A j base copy).amplitude n)

theorem NavierStokes.ParticularWaveAssembly.actualCopy_pressure_invariant {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : Reference P) (charts : BandCharts P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (copy : ℕ → TorusInverse.Frequency) (n : ℕ) : CopyAngularInvariance.Invariant ((0, 1), 0) ((actualCopyCoefficients r charts c u b G A j base copy).pressure n)

theorem NavierStokes.ParticularWaveAssembly.actualCommon_amplitude_periodization {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : Reference P) (charts : BandCharts P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (n : ℕ) : (actualCommonCoefficients r charts c u b G A j base).amplitude n = ParticularWaveBounds.periodizedCopies (bandGeometry r charts n) r.cutoff fun (k : TorusInverse.Frequency) => ParticularWaveBounds.complexCopyVelocity (angleTangent (bandTangent r charts j n)) (angleLift (residualSource c u b G A j n)) (bandGeometry r charts n) ⋯ k

theorem NavierStokes.ParticularWaveAssembly.actualCommon_pressure_periodization {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : Reference P) (charts : BandCharts P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) {j : ℤ} (hj : j ≠ 0) (hfrequency : ∀ (n : ℕ), b.frequency n ≠ 0) (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (n : ℕ) : (actualCommonCoefficients r charts c u b G A j base).pressure n = ParticularWaveBounds.periodizedCopies (bandGeometry r charts n) r.cutoff fun (k : TorusInverse.Frequency) => ParticularWaveBounds.complexCopyPressure (angleTangent (bandTangent r charts j n)) (angleLift (residualSource c u b G A j n)) (bandGeometry r charts n) ⋯ k (↑j * b.frequency n)

Germ transport through the actual differential operators

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

theorem NavierStokes.ParticularWaveAssembly.curl_germ {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : E → HarmonicCalculus.ComplexVector} {x : E} (h : a =ᶠ[nhds x] b) (R : E → ℝ) (Vr Vθ Vz : E → E) : CurlClassBounds.cylindricalCurl R Vr Vθ Vz a =ᶠ[nhds x] CurlClassBounds.cylindricalCurl R Vr Vθ Vz b

theorem NavierStokes.ParticularWaveAssembly.realizedCoefficient_germ {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : E → HarmonicCalculus.ComplexVector} {x : E} (h : a =ᶠ[nhds x] b) (K : ℝ) (R : E → ℝ) (Vr Vθ Vz : E → E) (Φ : E → ℝ) : CurlClassBounds.realizedCoefficient K R Vr Vθ Vz Φ a =ᶠ[nhds x] CurlClassBounds.realizedCoefficient K R Vr Vθ Vz Φ b

theorem NavierStokes.ParticularWaveAssembly.vectorMode_germ {E : Type} [NormedAddCommGroup E] {a b : E → HarmonicCalculus.ComplexVector} {x : E} (h : a =ᶠ[nhds x] b) (K : ℝ) (Φ : E → ℝ) : HarmonicCalculus.vectorMode K Φ a =ᶠ[nhds x] HarmonicCalculus.vectorMode K Φ b

theorem NavierStokes.ParticularWaveAssembly.mode_germ {E : Type} [NormedAddCommGroup E] {p q : E → ℂ} {x : E} (h : p =ᶠ[nhds x] q) (K : ℝ) (Φ : E → ℝ) : HarmonicCalculus.mode K Φ p =ᶠ[nhds x] HarmonicCalculus.mode K Φ q

theorem NavierStokes.ParticularWaveAssembly.laplacian_germ {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : E → ℂ} {x : E} (h : f =ᶠ[nhds x] g) (R : E → ℝ) (Vr Vθ Vz : E → E) : HarmonicCalculus.cylindricalLaplacian R Vr Vθ Vz f =ᶠ[nhds x] HarmonicCalculus.cylindricalLaplacian R Vr Vθ Vz g

theorem NavierStokes.ParticularWaveAssembly.vectorLaplacian_germ {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : E → HarmonicCalculus.ComplexVector} {x : E} (h : a =ᶠ[nhds x] b) (R : E → ℝ) (Vr Vθ Vz : E → E) : HarmonicCalculus.cylindricalVectorLaplacian R Vr Vθ Vz a =ᶠ[nhds x] HarmonicCalculus.cylindricalVectorLaplacian R Vr Vθ Vz b

theorem NavierStokes.ParticularWaveAssembly.linearResidual_germ {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : E → HarmonicCalculus.ComplexVector} {p q : E → ℂ} {x : E} (ha : a =ᶠ[nhds x] b) (hp : p =ᶠ[nhds x] q) (ε : ℝ) (R : E → ℝ) (Vr Vθ Vz Vt : E → E) (B : E → HarmonicCalculus.ComplexVector) : LinearWaveResidual.linearResidual ε R Vr Vθ Vz Vt B a p =ᶠ[nhds x] LinearWaveResidual.linearResidual ε R Vr Vθ Vz Vt B b q

Common physical coefficient and its exact local curl

noncomputable def NavierStokes.ParticularWaveAssembly.nativeCutoff {P : Type} (r : Reference P) (charts : BandCharts P) (copy : ℕ → TorusInverse.Frequency) : ℕ → (P × ℝ) × TorusInverse.Plane → ℝ

Native cutoff, defined pointwise by r.cutoff ((bandGeometry r charts n).coordinates (copy n) z.2).

Equations

• NavierStokes.ParticularWaveAssembly.nativeCutoff r charts copy n z = r.cutoff ((NavierStokes.ParticularWaveAssembly.bandGeometry r charts n).coordinates (copy n) z.2)

noncomputable def NavierStokes.ParticularWaveAssembly.actualCorrectedCommon {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : Reference P) (charts : BandCharts P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)) (dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)) : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)

The common coefficient already contains its single native cutoff. Its correction is the actual cylindrical curl correction of that coefficient.

Equations

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

theorem NavierStokes.ParticularWaveAssembly.actualCommon_raw_germ {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : Reference P) (charts : BandCharts P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) {j : ℤ} (hj : j ≠ 0) (hfrequency : ∀ (n : ℕ), b.frequency n ≠ 0) (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (copy : ℕ → TorusInverse.Frequency) (ψ : ℕ → (P × ℝ) × TorusInverse.Plane → ℝ) (n : ℕ) (x : (P × ℝ) × TorusInverse.Plane) {Ω : Set TorusInverse.Plane} (hΩ : IsOpen Ω) (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (bandGeometry r charts n).center + (bandGeometry r charts n).basis z) '' Ω)) (hsupp : Function.support r.cutoff ⊆ Ω) (hx : (bandGeometry r charts n).coordinates (copy n) x.2 ∈ Ω) (hψ : nativeCutoff r charts copy n =ᶠ[nhds x] ψ n) : (actualCommonCoefficients r charts c u b G A j base).amplitude n =ᶠ[nhds x] ((actualCopyCoefficients r charts c u b G A j base copy).withCutoff ψ).amplitude n ∧ (actualCommonCoefficients r charts c u b G A j base).pressure n =ᶠ[nhds x] ((actualCopyCoefficients r charts c u b G A j base copy).withCutoff ψ).pressure n

theorem NavierStokes.ParticularWaveAssembly.actualCommon_corrected_germ {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : Reference P) (charts : BandCharts P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) {j : ℤ} (hj : j ≠ 0) (hfrequency : ∀ (n : ℕ), b.frequency n ≠ 0) (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (copy : ℕ → TorusInverse.Frequency) (s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)) (dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)) (ψ : ℕ → (P × ℝ) × TorusInverse.Plane → ℝ) (n : ℕ) (x : (P × ℝ) × TorusInverse.Plane) {Ω : Set TorusInverse.Plane} (hΩ : IsOpen Ω) (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (bandGeometry r charts n).center + (bandGeometry r charts n).basis z) '' Ω)) (hsupp : Function.support r.cutoff ⊆ Ω) (hx : (bandGeometry r charts n).coordinates (copy n) x.2 ∈ Ω) (hψ : nativeCutoff r charts copy n =ᶠ[nhds x] ψ n) : (actualCorrectedCommon r charts c u b G A j base s dirs).amplitude n =ᶠ[nhds x] ((actualCopyCoefficients r charts c u b G A j base copy).corrected s dirs ψ).amplitude n ∧ (actualCorrectedCommon r charts c u b G A j base s dirs).pressure n =ᶠ[nhds x] ((actualCopyCoefficients r charts c u b G A j base copy).corrected s dirs ψ).pressure n

theorem NavierStokes.ParticularWaveAssembly.actualCommon_residual_germ {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : Reference P) (charts : BandCharts P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) {j : ℤ} (hj : j ≠ 0) (hfrequency : ∀ (n : ℕ), b.frequency n ≠ 0) (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (copy : ℕ → TorusInverse.Frequency) (s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)) (dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)) (ψ : ℕ → (P × ℝ) × TorusInverse.Plane → ℝ) (n : ℕ) (x : (P × ℝ) × TorusInverse.Plane) {Ω : Set TorusInverse.Plane} (hΩ : IsOpen Ω) (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (bandGeometry r charts n).center + (bandGeometry r charts n).basis z) '' Ω)) (hsupp : Function.support r.cutoff ⊆ Ω) (hx : (bandGeometry r charts n).coordinates (copy n) x.2 ∈ Ω) (hψ : nativeCutoff r charts copy n =ᶠ[nhds x] ψ n) : (actualCorrectedCommon r charts c u b G A j base s dirs).harmonicResidual s dirs n =ᶠ[nhds x] ((actualCopyCoefficients r charts c u b G A j base copy).corrected s dirs ψ).harmonicResidual s dirs n

Finite fields at the original residual carrier

theorem NavierStokes.ParticularWaveAssembly.modeBlock_value {D : Type} (j : ℤ) (k : ℕ → ℝ) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (v : ℕ → D → HarmonicCalculus.ComplexVector) (p : ℕ → D → ℂ) (n : ℕ) (x : D × ℝ) (i : Fin 3) : (modeBlock j k Φ kp v p).oscillation n x i = (v n x.1 i * HarmonicFields.character j (k n * Φ n x.1 + ↑(kp n) * x.2)).re

theorem NavierStokes.ParticularWaveAssembly.modeBlock_pressure_value {D : Type} (j : ℤ) (k : ℕ → ℝ) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (v : ℕ → D → HarmonicCalculus.ComplexVector) (p : ℕ → D → ℂ) (n : ℕ) (x : D × ℝ) : (modeBlock j k Φ kp v p).oscillatoryPressure n x = (p n x.1 * HarmonicFields.character j (k n * Φ n x.1 + ↑(kp n) * x.2)).re

theorem NavierStokes.ParticularWaveAssembly.assembledBlock_value {D : Type} (N : ℕ) (k : ℕ → ℝ) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (v : ℤ → ℕ → D → HarmonicCalculus.ComplexVector) (p : ℤ → ℕ → D → ℂ) (n : ℕ) (x : D × ℝ) (i : Fin 3) : (assembledBlock N k Φ kp v p).oscillation n x i = ∑ j ∈ modes N, (v j n x.1 i * HarmonicFields.character j (k n * Φ n x.1 + ↑(kp n) * x.2)).re

theorem NavierStokes.ParticularWaveAssembly.assembledBlock_pressure_value {D : Type} (N : ℕ) (k : ℕ → ℝ) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (v : ℤ → ℕ → D → HarmonicCalculus.ComplexVector) (p : ℤ → ℕ → D → ℂ) (n : ℕ) (x : D × ℝ) : (assembledBlock N k Φ kp v p).oscillatoryPressure n x = ∑ j ∈ modes N, (p j n x.1 * HarmonicFields.character j (k n * Φ n x.1 + ↑(kp n) * x.2)).re

theorem NavierStokes.ParticularWaveAssembly.residualSource_field {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A : HarmonicResidual.BlockCoefficients D) (N : ℕ) (hN : (HarmonicResidual.residualBlock c u b G A).BandLimited N) (n : ℕ) (x : D × ℝ) (i : Fin 3) : (HarmonicResidual.residualBlock c u b G A).oscillation n x i = ∑ j ∈ modes N, (residualSource c u b G A j n x.1 i * HarmonicFields.character j (b.frequency n * b.phase n x.1 + ↑(b.angularFrequency n) * x.2)).re

theorem NavierStokes.ParticularWaveAssembly.finite_cancellation {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A : HarmonicResidual.BlockCoefficients D) (N : ℕ) (hN : (HarmonicResidual.residualBlock c u b G A).BandLimited N) (res : ℤ → ℕ → D × ℝ → HarmonicCalculus.ComplexVector) (good gaussian : ℤ → ℕ → D → HarmonicCalculus.ComplexVector) (n : ℕ) (x : D × ℝ) (hcancel : ∀ j ∈ modes N, ∀ (i : Fin 3), res j n x i + residualSource c u b G A j n x.1 i * HarmonicFields.character j (b.frequency n * b.phase n x.1 + ↑(b.angularFrequency n) * x.2) = (good j n x.1 i + gaussian j n x.1 i) * HarmonicFields.character j (b.frequency n * b.phase n x.1 + ↑(b.angularFrequency n) * x.2)) : (fun (i : Fin 3) => ∑ j ∈ modes N, (res j n x i).re) + (HarmonicResidual.residualBlock c u b G A).oscillation n x = (assembledBlock N b.frequency b.phase b.angularFrequency good fun (x : ℤ) (x_1 : ℕ) (x_2 : D) => 0).oscillation n x + (assembledBlock N b.frequency b.phase b.angularFrequency gaussian fun (x : ℤ) (x_1 : ℕ) (x_2 : D) => 0).oscillation n x

theorem NavierStokes.ParticularWaveAssembly.real_linearResidual_sum {E ι : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (J : Finset ι) {U : Set E} (hU : IsOpen U) (ε : ℝ) (R : E → ℝ) {Vr Vθ Vz : E → E} (Vt : E → E) (hr : ContDiffOn ℝ (↑⊤) Vr U) (hθ : ContDiffOn ℝ (↑⊤) Vθ U) (hz : ContDiffOn ℝ (↑⊤) Vz U) (B : E → Fin 3 → ℝ) (v : ι → E → HarmonicCalculus.ComplexVector) (p : ι → E → ℂ) (hv : ∀ l ∈ J, ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : E) => v l y i) U) (hp : ∀ l ∈ J, ContDiffOn ℝ (↑⊤) (p l) U) {x : E} (hB : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : E) => B y i) x) (hx : x ∈ U) : LinearWaveResidual.realComponentLinearResidual ε R Vr Vθ Vz Vt B (fun (y : E) (i : Fin 3) => ∑ l ∈ J, (v l y i).re) (fun (y : E) => ∑ l ∈ J, (p l y).re) x = fun (i : Fin 3) => ∑ l ∈ J, (LinearWaveResidual.linearResidual ε R Vr Vθ Vz Vt (LinearWaveResidual.realLift B) (v l) (p l) x i).re

The real differential operator commutes with the actual finite sum of real parts. This connects the coefficient cancellation to one field.

Restriction of actual native coefficients to the angular section

noncomputable def NavierStokes.ParticularWaveAssembly.sectionStrip {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)) : WeightedClasses.StripData (P × TorusInverse.Plane)

Section strip, given by SignedWaveUpdate.sectionStrip (reindexStrip (angleShuffle (P := P)) s).

Equations

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

noncomputable def NavierStokes.ParticularWaveAssembly.nativeModeBlock {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (j : ℤ) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (a : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)

Native mode block, given by fullModeBlock j b.frequency b.phase b.angularFrequency (reindexCoefficients angleShuffle a).

Equations

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

theorem NavierStokes.ParticularWaveAssembly.nativeSlice_class {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {w : ℕ → (P × ℝ) × TorusInverse.Plane → ℝ} {α : ℝ} {f : ℕ → (P × ℝ) × TorusInverse.Plane → F} (hf : WeightedClasses.MemClass s w α f) : WeightedClasses.MemClass (sectionStrip s) (fun (n : ℕ) (x : P × TorusInverse.Plane) => w n (angleShuffle (x, 0))) α fun (n : ℕ) (x : P × TorusInverse.Plane) => f n (angleShuffle (x, 0))

theorem NavierStokes.ParticularWaveAssembly.nativeSlice_waveClass {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {W : ℕ → (P × ℝ) × TorusInverse.Plane → ℝ} {α : ℝ} {f : ℕ → (P × ℝ) × TorusInverse.Plane → F} (hf : WeightedClasses.WaveClass s W α f) : WeightedClasses.WaveClass (sectionStrip s) (fun (n : ℕ) (x : P × TorusInverse.Plane) => W n (angleShuffle (x, 0))) α fun (n : ℕ) (x : P × TorusInverse.Plane) => f n (angleShuffle (x, 0))

theorem NavierStokes.ParticularWaveAssembly.nativeModeBlock_classes {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {W : ℕ → (P × ℝ) × TorusInverse.Plane → ℝ} {α γ : ℝ} (j : ℤ) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (a : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (ha : WeightedClasses.WaveClass s W α a.amplitude) (hp : WeightedClasses.WaveClass s W γ a.pressure) : CorrectionState.HarmonicBlock.WaveBounds (sectionStrip s) (fun (n : ℕ) (x : P × TorusInverse.Plane) => W n (angleShuffle (x, 0))) α (nativeModeBlock j b a) ∧ CorrectionState.HarmonicBlock.PressureBounds (sectionStrip s) (fun (n : ℕ) (x : P × TorusInverse.Plane) => W n (angleShuffle (x, 0))) γ (nativeModeBlock j b a)

theorem NavierStokes.ParticularWaveAssembly.nativeModeBlock_represents {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (j : ℤ) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (a : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (ha : ∀ (n : ℕ), CopyAngularInvariance.Invariant ((0, 1), 0) (a.amplitude n)) (hp : ∀ (n : ℕ), CopyAngularInvariance.Invariant ((0, 1), 0) (a.pressure n)) (hphase : ∀ (n : ℕ) (x : P × TorusInverse.Plane) (θ : ℝ), a.frequency n * a.phase n (angleShuffle (x, θ)) = ↑j * (b.frequency n * b.phase n x + ↑(b.angularFrequency n) * θ)) : ((nativeModeBlock j b a).oscillation = fun (n : ℕ) (x : (P × TorusInverse.Plane) × ℝ) (i : Fin 3) => (HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) (a.amplitude n) (angleShuffle x) i).re) ∧ (nativeModeBlock j b a).oscillatoryPressure = fun (n : ℕ) (x : (P × TorusInverse.Plane) × ℝ) => (HarmonicCalculus.mode (a.frequency n) (a.phase n) (a.pressure n) (angleShuffle x)).re

theorem NavierStokes.ParticularWaveAssembly.actualCarrier_character {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (j : ℤ) (hfrequency : ∀ (n : ℕ), b.frequency n ≠ 0) (n : ℕ) (x : (P × TorusInverse.Plane) × ℝ) : HarmonicCalculus.carrier ((actualCarrier base b j).frequency n) ((actualCarrier base b j).phase n) (angleShuffle x) = HarmonicFields.character j (b.frequency n * b.phase n x.1 + ↑(b.angularFrequency n) * x.2)

Primitive controls for the actual residual-source construction

noncomputable def NavierStokes.ParticularWaveAssembly.sourceFamily {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) : ℕ → (P × ℝ) × TorusInverse.Plane → HarmonicCalculus.ComplexVector

Source family, defined pointwise by angleLift (residualSource c u b G A j n).

Equations

• NavierStokes.ParticularWaveAssembly.sourceFamily c u b G A j n = NavierStokes.ParticularWaveAssembly.angleLift (NavierStokes.ParticularWaveAssembly.residualSource c u b G A j n)

noncomputable def NavierStokes.ParticularWaveAssembly.tangentFamily {P : Type} (r : Reference P) (charts : BandCharts P) (j : ℤ) : ℕ → CommonCoverSolve.TangentData (P × ℝ) ProblemStatement.Space

Tangent family, defined pointwise by angleTangent (bandTangent r charts j n).

Equations

• NavierStokes.ParticularWaveAssembly.tangentFamily r charts j n = NavierStokes.ParticularWaveAssembly.angleTangent (NavierStokes.ParticularWaveAssembly.bandTangent r charts j n)

noncomputable def NavierStokes.ParticularWaveAssembly.envelopeWeight {P : Type} (r : Reference P) (charts : BandCharts P) (copy : ℕ → TorusInverse.Frequency) (W : ℕ → ℝ → ℝ) : ℕ → (P × ℝ) × TorusInverse.Plane → ℝ

Envelope weight, defined pointwise by W n ((bandGeometry r charts n).coordinates (copy n) p.2).2.

Equations

• NavierStokes.ParticularWaveAssembly.envelopeWeight r charts copy W n p = W n ((NavierStokes.ParticularWaveAssembly.bandGeometry r charts n).coordinates (copy n) p.2).2

structure NavierStokes.ParticularWaveAssembly.BackgroundControl {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)) (dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)) (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (j : ℤ) : Prop

Differential and angular facts about the primitive background fields. No solved amplitude, pressure, or error estimate is stored here.

• angular : dirs.angular = ((0, 1), 0)
• phase_smooth (n : ℕ) : ContDiffOn ℝ (↑⊤) ((actualCarrier base b j).phase n) s.domain
• radius_ne (n : ℕ) (x : (P × ℝ) × TorusInverse.Plane) : x ∈ s.domain → base.radius n x ≠ 0
• radial_radius (n : ℕ) (x : (P × ℝ) × TorusInverse.Plane) : x ∈ s.domain → HarmonicCalculus.along (dirs.radialField n) (base.radius n) x = 1
• radius_invariant (n : ℕ) : CopyAngularInvariance.Invariant dirs.angular (base.radius n)
• radial_base_invariant (n : ℕ) : CopyAngularInvariance.Invariant dirs.angular (base.radialBase n)
• frequency_base_invariant (n : ℕ) : CopyAngularInvariance.Invariant dirs.angular (base.frequencyBase n)
• axial_base_invariant (n : ℕ) : CopyAngularInvariance.Invariant dirs.angular (base.axialBase n)
• radial_invariant (n : ℕ) : CopyAngularInvariance.Invariant dirs.angular (dirs.radialField n)
• axial_invariant (n : ℕ) : CopyAngularInvariance.Invariant dirs.angular (dirs.axialField s n)
• cylindrical (n : ℕ) : CurlClassBounds.CylindricalGeometry s.domain (base.radius n) (dirs.radialField n) (fun (x : (P × ℝ) × TorusInverse.Plane) => dirs.angular) (dirs.axialField s n)

structure NavierStokes.ParticularWaveAssembly.LocalControl {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (r : Reference P) (charts : BandCharts P) (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (copy : ℕ → TorusInverse.Frequency) (s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)) (dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)) (α κ : ℝ) : Type

Primitive modal, background, envelope, and native-chart input bounds for the actual HR-source constructor. Every solution and residual below is computed, rather than supplied as a record field.

• harmonic_ne : j ≠ 0
• frequency_ne (n : ℕ) : b.frequency n ≠ 0
• envelope : ℕ → ℝ → ℝ

  Envelope of LocalControl, of type ℕ → ℝ → ℝ.

• frame : ℕ → PrimaryODE.FrameData ((P × ℝ) × ℝ)

  Frame of LocalControl, of type ℕ → PrimaryODE.FrameData ((P × ℝ) × ℝ).

• modalReal : ParticularWaveBounds.ModalCopyControl s α self.frame (fun (n : ℕ) => ParticularWaveBounds.realData (tangentFamily r charts j n) (sourceFamily c u b G A j n)) j (bandGeometry r charts) copy (fun (x : ℕ) => r.length) self.envelope

  Modal real supplied by LocalControl.

• modalImag : ParticularWaveBounds.ModalCopyControl s α self.frame (fun (n : ℕ) => ParticularWaveBounds.imagData (tangentFamily r charts j n) (sourceFamily c u b G A j n)) j (bandGeometry r charts) copy (fun (x : ℕ) => r.length) self.envelope

  Modal imag supplied by LocalControl.

• base_bounds : LinearWaveBounds.InputBounds s (envelopeWeight r charts copy self.envelope) α κ dirs (ParticularWaveBounds.zeroAmplitudes (actualCarrier base b j))
• background : BackgroundControl s dirs base b j
• normal_jets : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain s) fun (n : ℕ) (x : (P × ℝ) × TorusInverse.Plane) => (tangentFamily r charts j n).normal (ParticularWaveBounds.nativePoint (bandGeometry r charts n) (copy n) x)
• normal_derivative : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : (P × ℝ) × TorusInverse.Plane) => (tangentFamily r charts j n).normalDot (ParticularWaveBounds.nativePoint (bandGeometry r charts n) (copy n) x)
• action_bounds : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : (P × ℝ) × TorusInverse.Plane) => (tangentFamily r charts j n).action (ParticularWaveBounds.nativePoint (bandGeometry r charts n) (copy n) x)
• source_bounds : WeightedClasses.WaveClass s (envelopeWeight r charts copy self.envelope) α (sourceFamily c u b G A j)
• normalMin : ℝ

  Normal min of LocalControl, of type ℝ.

• normalMax : ℝ

  Normal max of LocalControl, of type ℝ.

• normal_min_pos : 0 < self.normalMin
• normal_lower (n : ℕ) (x : (P × ℝ) × TorusInverse.Plane) : x ∈ s.domain → self.normalMin ≤ ‖(tangentFamily r charts j n).normal (ParticularWaveBounds.nativePoint (bandGeometry r charts n) (copy n) x)‖
• normal_upper (n : ℕ) (x : (P × ℝ) × TorusInverse.Plane) : x ∈ s.domain → ‖(tangentFamily r charts j n).normal (ParticularWaveBounds.nativePoint (bandGeometry r charts n) (copy n) x)‖ ≤ self.normalMax
• inverse_frequency : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / (↑j * b.frequency n)
• geometry : ParticularWaveBounds.CopyGeometryMatch s dirs (actualCarrier base b j) (tangentFamily r charts j) (bandGeometry r charts) copy
• loss_le_half : κ ≤ 1 / 2
• radius : (P × ℝ) × TorusInverse.Plane → ℝ

  Radius of LocalControl, of type (P × ℝ) × Plane → ℝ.

• radius_eq : base.radius = fun (x : ℕ) => self.radius
• slot : GaussianTailFlat.SlotFamily s

  Slot of LocalControl, of type GaussianTailFlat.SlotFamily s.

• slot_angular (n : ℕ) : (self.slot.linear n) dirs.angular = 0
• slot_fast (n : ℕ) : (self.slot.linear n) (dirs.fastScale n • dirs.fast) = (self.slot.length n)⁻¹
• flatEdges : GaussianTailFlat.FlatEdges s

  Flat edges of LocalControl, of type GaussianTailFlat.FlatEdges s.

• bandScales : GaussianTailFlat.BandScaleControl s

  Band scales of LocalControl, of type GaussianTailFlat.BandScaleControl s.

• gaussianRate : ℝ

  Gaussian rate of LocalControl, of type ℝ.

• gaussian_rate_pos : 0 < self.gaussianRate
• gaussian_envelope (n : ℕ) (x : (P × ℝ) × TorusInverse.Plane) : x ∈ s.domain → envelopeWeight r charts copy self.envelope n x ≤ Real.exp (-self.gaussianRate * (self.slot.coordinate n x - 1 / 2) ^ 2 * self.slot.length n)
• patch : ℕ → Set TorusInverse.Plane

  Patch of LocalControl, of type ℕ → Set Plane.

• patch_open (n : ℕ) : IsOpen (self.patch n)
• patch_injective (n : ℕ) : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (bandGeometry r charts n).center + (bandGeometry r charts n).basis z) '' self.patch n)
• cutoff_support (n : ℕ) : Function.support r.cutoff ⊆ self.patch n
• domain_patch (n : ℕ) (x : (P × ℝ) × TorusInverse.Plane) : x ∈ s.domain → (bandGeometry r charts n).coordinates (copy n) x.2 ∈ self.patch n
• cutoff_match (n : ℕ) : Set.EqOn (nativeCutoff r charts copy n) (self.slot.cutoff n) s.domain

noncomputable def NavierStokes.ParticularWaveAssembly.LocalControl.weight {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) : ℕ → (P × ℝ) × TorusInverse.Plane → ℝ

Weight, given by envelopeWeight r charts copy C.envelope.

Equations

• C.weight = NavierStokes.ParticularWaveAssembly.envelopeWeight r charts copy C.envelope

theorem NavierStokes.ParticularWaveAssembly.LocalControl.frequency_nonzero {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) (n : ℕ) : ↑j * b.frequency n ≠ 0

theorem NavierStokes.ParticularWaveAssembly.LocalControl.slot_invariant {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) (n : ℕ) : CopyAngularInvariance.Invariant dirs.angular (C.slot.cutoff n)

theorem NavierStokes.ParticularWaveAssembly.LocalControl.affine_phase {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) (n : ℕ) : ∃ (m : ℝ), CopyAngularInvariance.AffinePhase dirs.angular m ((actualCarrier base b j).phase n)

theorem NavierStokes.ParticularWaveAssembly.LocalControl.amplitude_invariant {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) (n : ℕ) : CopyAngularInvariance.Invariant dirs.angular ((actualCopyCoefficients r charts c u b G A j base copy).amplitude n)

theorem NavierStokes.ParticularWaveAssembly.LocalControl.pressure_invariant {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) (n : ℕ) : CopyAngularInvariance.Invariant dirs.angular ((actualCopyCoefficients r charts c u b G A j base copy).pressure n)

theorem NavierStokes.ParticularWaveAssembly.LocalControl.exact_conditions {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) : LinearWaveBounds.ExactConditions s dirs ((actualCopyCoefficients r charts c u b G A j base copy).corrected s dirs C.slot.cutoff)

theorem NavierStokes.ParticularWaveAssembly.LocalControl.raw_bounds {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) : LinearWaveBounds.InputBounds s C.weight α κ dirs (actualCopyCoefficients r charts c u b G A j base copy)

theorem NavierStokes.ParticularWaveAssembly.LocalControl.local_result {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) : have a := actualCopyCoefficients r charts c u b G A j base copy; WeightedClasses.WaveClass s C.weight α a.amplitude ∧ WeightedClasses.WaveClass s C.weight α (a.corrected s dirs C.slot.cutoff).amplitude ∧ WeightedClasses.WaveClass s C.weight (α + 1 / 2) (a.corrected s dirs C.slot.cutoff).pressure ∧ WeightedClasses.WaveClass s C.weight (α + 1 / 2 - 3 * κ) (a.constructedGood s dirs C.slot.cutoff) ∧ ∀ (n : ℕ), ∀ x ∈ s.domain, ((a.corrected s dirs C.slot.cutoff).harmonicResidual s dirs n x + fun (i : Fin 3) => sourceFamily c u b G A j n x i * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x) = fun (i : Fin 3) => (a.constructedGood s dirs C.slot.cutoff n x i + LinearWaveBounds.excludedSlotError dirs C.slot.cutoff a.amplitude (sourceFamily c u b G A j) n x i) * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x

theorem NavierStokes.ParticularWaveAssembly.LocalControl.gaussian_flat {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) (β : ℝ) : WeightedClasses.UnweightedClass s β (LinearWaveBounds.excludedSlotError dirs C.slot.cutoff (actualCopyCoefficients r charts c u b G A j base copy).amplitude (sourceFamily c u b G A j))

theorem NavierStokes.ParticularWaveAssembly.LocalControl.raw_tangent {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) (n : ℕ) (x : (P × ℝ) × TorusInverse.Plane) : x ∈ s.domain → HarmonicCalculus.normalDot ((actualCarrier base b j).normal s dirs n x) ((actualCopyCoefficients r charts c u b G A j base copy).amplitude n x) = 0

theorem NavierStokes.ParticularWaveAssembly.LocalControl.normal_nonzero {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) (n : ℕ) (x : (P × ℝ) × TorusInverse.Plane) (hx : x ∈ s.domain) : (actualCarrier base b j).normal s dirs n x ≠ 0

theorem NavierStokes.ParticularWaveAssembly.LocalControl.exact_curl {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) (n : ℕ) {x : (P × ℝ) × TorusInverse.Plane} (hx : x ∈ s.domain) : have a := actualCopyCoefficients r charts c u b G A j base copy; CurlClassBounds.cylindricalCurl (base.radius n) (dirs.radialField n) (fun (x : (P × ℝ) × TorusInverse.Plane) => dirs.angular) (dirs.axialField s n) ((a.withCutoff C.slot.cutoff).curlPotential s dirs n) x = HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) ((a.corrected s dirs C.slot.cutoff).amplitude n) x

theorem NavierStokes.ParticularWaveAssembly.LocalControl.divergence_zero {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) (n : ℕ) {x : (P × ℝ) × TorusInverse.Plane} (hx : x ∈ s.domain) : have a := actualCopyCoefficients r charts c u b G A j base copy; HarmonicCalculus.cylindricalDivergence (base.radius n) (dirs.radialField n) (fun (x : (P × ℝ) × TorusInverse.Plane) => dirs.angular) (dirs.axialField s n) (HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) ((a.corrected s dirs C.slot.cutoff).amplitude n)) x = 0

theorem NavierStokes.ParticularWaveAssembly.LocalControl.cutoff_germ {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) (n : ℕ) {x : (P × ℝ) × TorusInverse.Plane} (hx : x ∈ s.domain) : nativeCutoff r charts copy n =ᶠ[nhds x] C.slot.cutoff n

theorem NavierStokes.ParticularWaveAssembly.LocalControl.common_germ {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) (n : ℕ) {x : (P × ℝ) × TorusInverse.Plane} (hx : x ∈ s.domain) : (actualCorrectedCommon r charts c u b G A j base s dirs).amplitude n =ᶠ[nhds x] ((actualCopyCoefficients r charts c u b G A j base copy).corrected s dirs C.slot.cutoff).amplitude n ∧ (actualCorrectedCommon r charts c u b G A j base s dirs).pressure n =ᶠ[nhds x] ((actualCopyCoefficients r charts c u b G A j base copy).corrected s dirs C.slot.cutoff).pressure n

theorem NavierStokes.ParticularWaveAssembly.LocalControl.common_residual_germ {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) (n : ℕ) {x : (P × ℝ) × TorusInverse.Plane} (hx : x ∈ s.domain) : (actualCorrectedCommon r charts c u b G A j base s dirs).harmonicResidual s dirs n =ᶠ[nhds x] ((actualCopyCoefficients r charts c u b G A j base copy).corrected s dirs C.slot.cutoff).harmonicResidual s dirs n

theorem NavierStokes.ParticularWaveAssembly.LocalControl.common_classes {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) : WeightedClasses.WaveClass s C.weight α (actualCorrectedCommon r charts c u b G A j base s dirs).amplitude ∧ WeightedClasses.WaveClass s C.weight (α + 1 / 2) (actualCorrectedCommon r charts c u b G A j base s dirs).pressure

theorem NavierStokes.ParticularWaveAssembly.LocalControl.common_cancellation {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) (n : ℕ) {x : (P × ℝ) × TorusInverse.Plane} (hx : x ∈ s.domain) : have a := actualCopyCoefficients r charts c u b G A j base copy; ((actualCorrectedCommon r charts c u b G A j base s dirs).harmonicResidual s dirs n x + fun (i : Fin 3) => sourceFamily c u b G A j n x i * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x) = fun (i : Fin 3) => (a.constructedGood s dirs C.slot.cutoff n x i + LinearWaveBounds.excludedSlotError dirs C.slot.cutoff a.amplitude (sourceFamily c u b G A j) n x i) * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x

Actual periodized, curl-corrected field cancellation. Both terms of excludedSlotError remain in this exact identity.

theorem NavierStokes.ParticularWaveAssembly.LocalControl.good_invariant {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) (n : ℕ) : CopyAngularInvariance.Invariant dirs.angular ((actualCopyCoefficients r charts c u b G A j base copy).constructedGood s dirs C.slot.cutoff n)

theorem NavierStokes.ParticularWaveAssembly.LocalControl.gaussian_invariant {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) (n : ℕ) : CopyAngularInvariance.Invariant dirs.angular (LinearWaveBounds.excludedSlotError dirs C.slot.cutoff (actualCopyCoefficients r charts c u b G A j base copy).amplitude (sourceFamily c u b G A j) n)

theorem NavierStokes.ParticularWaveAssembly.LocalControl.common_amplitude_invariant {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) (n : ℕ) : CopyAngularInvariance.Invariant dirs.angular ((actualCorrectedCommon r charts c u b G A j base s dirs).amplitude n)

theorem NavierStokes.ParticularWaveAssembly.LocalControl.common_pressure_invariant {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) (n : ℕ) : CopyAngularInvariance.Invariant dirs.angular ((actualCorrectedCommon r charts c u b G A j base s dirs).pressure n)

theorem NavierStokes.ParticularWaveAssembly.LocalControl.common_divergence_zero {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) (n : ℕ) {x : (P × ℝ) × TorusInverse.Plane} (hx : x ∈ s.domain) : have a := actualCorrectedCommon r charts c u b G A j base s dirs; HarmonicCalculus.cylindricalDivergence (base.radius n) (dirs.radialField n) (fun (x : (P × ℝ) × TorusInverse.Plane) => dirs.angular) (dirs.axialField s n) (HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) (a.amplitude n)) x = 0

noncomputable def NavierStokes.ParticularWaveAssembly.LocalControl.good {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) : ℕ → (P × ℝ) × TorusInverse.Plane → HarmonicCalculus.ComplexVector

Good, given by (actualCopyCoefficients r charts c u b G A j base copy).constructedGood s dirs C.slot.cutoff.

Equations

• C.good = (NavierStokes.ParticularWaveAssembly.actualCopyCoefficients r charts c u b G A j base copy).constructedGood s dirs C.slot.cutoff

noncomputable def NavierStokes.ParticularWaveAssembly.LocalControl.gaussian {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) : ℕ → (P × ℝ) × TorusInverse.Plane → HarmonicCalculus.ComplexVector

Gaussian, given by excludedSlotError dirs C.slot.cutoff (actualCopyCoefficients r charts c u b G A j base copy).amplitude (sourceFamily c u b G A j).

Equations

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

theorem NavierStokes.ParticularWaveAssembly.LocalControl.section_cancellation {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) (n : ℕ) (x : (P × TorusInverse.Plane) × ℝ) (hx : angleShuffle x ∈ s.domain) (i : Fin 3) : (actualCorrectedCommon r charts c u b G A j base s dirs).harmonicResidual s dirs n (angleShuffle x) i + residualSource c u b G A j n x.1 i * HarmonicFields.character j (b.frequency n * b.phase n x.1 + ↑(b.angularFrequency n) * x.2) = (C.good n (angleShuffle (x.1, 0)) i + C.gaussian n (angleShuffle (x.1, 0)) i) * HarmonicFields.character j (b.frequency n * b.phase n x.1 + ↑(b.angularFrequency n) * x.2)

theorem NavierStokes.ParticularWaveAssembly.LocalControl.block_represents {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {r : Reference P} {charts : BandCharts P} {c : CorrectionState.Context (P × TorusInverse.Plane)} {u : CorrectionState.State (P × TorusInverse.Plane)} {b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)} {G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)} {j : ℤ} {base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)} {copy : ℕ → TorusInverse.Frequency} {s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)} {dirs : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)} {α κ : ℝ} (C : LocalControl r charts c u b G A j base copy s dirs α κ) : ((nativeModeBlock j b (actualCorrectedCommon r charts c u b G A j base s dirs)).oscillation = fun (n : ℕ) (x : (P × TorusInverse.Plane) × ℝ) (i : Fin 3) => (HarmonicCalculus.vectorMode (↑j * b.frequency n) ((actualCarrier base b j).phase n) ((actualCorrectedCommon r charts c u b G A j base s dirs).amplitude n) (angleShuffle x) i).re) ∧ (nativeModeBlock j b (actualCorrectedCommon r charts c u b G A j base s dirs)).oscillatoryPressure = fun (n : ℕ) (x : (P × TorusInverse.Plane) × ℝ) => (HarmonicCalculus.mode (↑j * b.frequency n) ((actualCarrier base b j).phase n) ((actualCorrectedCommon r charts c u b G A j base s dirs).pressure n) (angleShuffle x)).re

Finite actual fields and residual cancellation

structure NavierStokes.ParticularWaveAssembly.AssemblyData (P : Type) [NormedAddCommGroup P] [NormedSpace ℝ P] : Type

All primitive choices for one original spatial label. There is only one reference and one family of band charts for its entire harmonic sum.

• reference : Reference P

  Reference of AssemblyData, of type Reference P.

• charts : BandCharts P

  Charts of AssemblyData, of type BandCharts P.

• context : CorrectionState.Context (P × TorusInverse.Plane)

  Context of AssemblyData, of type Context (P × Plane).

• state : CorrectionState.State (P × TorusInverse.Plane)

  State of AssemblyData, of type State (P × Plane).

• carrierBlock : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)

  Carrier block of AssemblyData, of type HarmonicBlock (P × Plane).

• gaussianInput : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)

  Gaussian input of AssemblyData, of type HarmonicResidual.BlockCoefficients (P × Plane).

• aliasInput : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)

  Alias input of AssemblyData, of type HarmonicResidual.BlockCoefficients (P × Plane).

• background : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)

  Background of AssemblyData, of type WaveCoefficients ((P × ℝ) × Plane).

• copy : ℕ → TorusInverse.Frequency

  Copy of AssemblyData, of type ℕ → Frequency.

• strip : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)

  Strip of AssemblyData, of type StripData ((P × ℝ) × Plane).

• directions : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)

  Directions of AssemblyData, of type GraphDirections ((P × ℝ) × Plane).

noncomputable def NavierStokes.ParticularWaveAssembly.AssemblyData.wave {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (D : AssemblyData P) (j : ℤ) : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)

Wave, constructed using actualCorrectedCommon.

Equations

• D.wave j = NavierStokes.ParticularWaveAssembly.actualCorrectedCommon D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.strip D.directions

noncomputable def NavierStokes.ParticularWaveAssembly.AssemblyData.controls {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (D : AssemblyData P) (N : ℕ) (α κ : ℝ) : Type

Controls as an element of Type.

Equations

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

noncomputable def NavierStokes.ParticularWaveAssembly.AssemblyData.velocity {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (D : AssemblyData P) (N : ℕ) : ℕ → (P × ℝ) × TorusInverse.Plane → Fin 3 → ℝ

Velocity, defined pointwise by ∑ j ∈ modes N, (vectorMode ((D.wave j).frequency n) ((D.wave j).phase n) ((D.wave j).amplitude n) x i).re.

Equations

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

noncomputable def NavierStokes.ParticularWaveAssembly.AssemblyData.pressure {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (D : AssemblyData P) (N : ℕ) : ℕ → (P × ℝ) × TorusInverse.Plane → ℝ

Pressure, defined pointwise by ∑ j ∈ modes N, (mode ((D.wave j).frequency n) ((D.wave j).phase n) ((D.wave j).pressure n) x).re.

Equations

• D.pressure N n x = ∑ j ∈ NavierStokes.ParticularWaveAssembly.modes N, (NavierStokes.HarmonicCalculus.mode ((D.wave j).frequency n) ((D.wave j).phase n) ((D.wave j).pressure n) x).re

noncomputable def NavierStokes.ParticularWaveAssembly.AssemblyData.updateBlock {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (D : AssemblyData P) (N : ℕ) : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)

Update block, constructed using assembledBlock.

Equations

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

noncomputable def NavierStokes.ParticularWaveAssembly.AssemblyData.goodFamily {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (D : AssemblyData P) {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) (j : ℤ) : ℕ → (P × ℝ) × TorusInverse.Plane → HarmonicCalculus.ComplexVector

Good family, with branches according to hj : j ∈ modes N.

Equations

• D.goodFamily C j = if hj : j ∈ NavierStokes.ParticularWaveAssembly.modes N then (C j hj).good else fun (x : ℕ) (x_1 : (P × ℝ) × NavierStokes.TorusInverse.Plane) => 0

noncomputable def NavierStokes.ParticularWaveAssembly.AssemblyData.gaussianFamily {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (D : AssemblyData P) {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) (j : ℤ) : ℕ → (P × ℝ) × TorusInverse.Plane → HarmonicCalculus.ComplexVector

Gaussian family, with branches according to hj : j ∈ modes N.

Equations

• D.gaussianFamily C j = if hj : j ∈ NavierStokes.ParticularWaveAssembly.modes N then (C j hj).gaussian else fun (x : ℕ) (x_1 : (P × ℝ) × NavierStokes.TorusInverse.Plane) => 0

noncomputable def NavierStokes.ParticularWaveAssembly.AssemblyData.goodBlock {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (D : AssemblyData P) {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)

Good block, constructed using assembledBlock.

Equations

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

noncomputable def NavierStokes.ParticularWaveAssembly.AssemblyData.gaussianBlock {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (D : AssemblyData P) {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)

Gaussian block, constructed using assembledBlock.

Equations

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

theorem NavierStokes.ParticularWaveAssembly.AssemblyData.update_band {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (D : AssemblyData P) (N : ℕ) : (D.updateBlock N).BandLimited N

theorem NavierStokes.ParticularWaveAssembly.AssemblyData.update_real {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (D : AssemblyData P) (N : ℕ) : ErrorHarmonics.RealBlock (D.updateBlock N)

theorem NavierStokes.ParticularWaveAssembly.AssemblyData.good_band {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : AssemblyData P} {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) : (D.goodBlock C).BandLimited N

theorem NavierStokes.ParticularWaveAssembly.AssemblyData.gaussian_band {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : AssemblyData P} {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) : (D.gaussianBlock C).BandLimited N

theorem NavierStokes.ParticularWaveAssembly.AssemblyData.good_real {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : AssemblyData P} {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) : ErrorHarmonics.RealBlock (D.goodBlock C)

theorem NavierStokes.ParticularWaveAssembly.AssemblyData.gaussian_real {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : AssemblyData P} {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) : ErrorHarmonics.RealBlock (D.gaussianBlock C)

theorem NavierStokes.ParticularWaveAssembly.AssemblyData.error_mean_zero {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : AssemblyData P} {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) (hkp : ∀ (n : ℕ), D.carrierBlock.angularFrequency n ≠ 0) : ((∀ (i : Fin 3), (CorrectionState.angularAverage fun (n : ℕ) (x : (P × TorusInverse.Plane) × ℝ) => (D.goodBlock C).oscillation n x i) = 0) ∧ CorrectionState.angularAverage (D.goodBlock C).oscillatoryPressure = 0) ∧ (∀ (i : Fin 3), (CorrectionState.angularAverage fun (n : ℕ) (x : (P × TorusInverse.Plane) × ℝ) => (D.gaussianBlock C).oscillation n x i) = 0) ∧ CorrectionState.angularAverage (D.gaussianBlock C).oscillatoryPressure = 0

theorem NavierStokes.ParticularWaveAssembly.AssemblyData.update_mean_zero {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : AssemblyData P} {N : ℕ} (hkp : ∀ (n : ℕ), D.carrierBlock.angularFrequency n ≠ 0) : (∀ (i : Fin 3), (CorrectionState.angularAverage fun (n : ℕ) (x : (P × TorusInverse.Plane) × ℝ) => (D.updateBlock N).oscillation n x i) = 0) ∧ CorrectionState.angularAverage (D.updateBlock N).oscillatoryPressure = 0

theorem NavierStokes.ParticularWaveAssembly.AssemblyData.update_represents {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : AssemblyData P} {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) : ((D.updateBlock N).oscillation = fun (n : ℕ) (x : (P × TorusInverse.Plane) × ℝ) => D.velocity N n (angleShuffle x)) ∧ (D.updateBlock N).oscillatoryPressure = fun (n : ℕ) (x : (P × TorusInverse.Plane) × ℝ) => D.pressure N n (angleShuffle x)

theorem NavierStokes.ParticularWaveAssembly.AssemblyData.update_classes {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : AssemblyData P} {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) (W : ℕ → (P × ℝ) × TorusInverse.Plane → ℝ) (hW : ∀ (n : ℕ), ∀ x ∈ D.strip.domain, 0 ≤ W n x) (hCW : ∀ (j : ℤ) (hj : j ∈ modes N) (n : ℕ), ∀ x ∈ D.strip.domain, (C j hj).weight n x ≤ W n x) : CorrectionState.HarmonicBlock.WaveBounds (sectionStrip D.strip) (fun (n : ℕ) (x : P × TorusInverse.Plane) => W n (angleShuffle (x, 0))) α (D.updateBlock N) ∧ CorrectionState.HarmonicBlock.PressureBounds (sectionStrip D.strip) (fun (n : ℕ) (x : P × TorusInverse.Plane) => W n (angleShuffle (x, 0))) (α + 1 / 2) (D.updateBlock N)

theorem NavierStokes.ParticularWaveAssembly.AssemblyData.good_classes {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : AssemblyData P} {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) (W : ℕ → (P × ℝ) × TorusInverse.Plane → ℝ) (hW : ∀ (n : ℕ), ∀ x ∈ D.strip.domain, 0 ≤ W n x) (hCW : ∀ (j : ℤ) (hj : j ∈ modes N) (n : ℕ), ∀ x ∈ D.strip.domain, (C j hj).weight n x ≤ W n x) : CorrectionState.HarmonicBlock.WaveBounds (sectionStrip D.strip) (fun (n : ℕ) (x : P × TorusInverse.Plane) => W n (angleShuffle (x, 0))) (α + 1 / 2 - 3 * κ) (D.goodBlock C)

theorem NavierStokes.ParticularWaveAssembly.AssemblyData.gaussian_classes {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : AssemblyData P} {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) (β : ℝ) (i : Fin 3) (m : ℤ) : WeightedClasses.UnweightedClass (sectionStrip D.strip) β fun (n : ℕ) (x : P × TorusInverse.Plane) => ((D.gaussianBlock C).velocity n i).coeff m x

theorem NavierStokes.ParticularWaveAssembly.AssemblyData.cancellation_sum {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : AssemblyData P} {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) (hN : (HarmonicResidual.residualBlock D.context D.state D.carrierBlock D.gaussianInput D.aliasInput).BandLimited N) (n : ℕ) (x : (P × TorusInverse.Plane) × ℝ) (hx : angleShuffle x ∈ D.strip.domain) : (fun (i : Fin 3) => ∑ j ∈ modes N, ((D.wave j).harmonicResidual D.strip D.directions n (angleShuffle x) i).re) + (HarmonicResidual.residualBlock D.context D.state D.carrierBlock D.gaussianInput D.aliasInput).oscillation n x = (D.goodBlock C).oscillation n x + (D.gaussianBlock C).oscillation n x

theorem NavierStokes.ParticularWaveAssembly.along_finset_sum {E F ι : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (J : Finset ι) (V : E → E) (f : ι → E → F) {x : E} (hf : ∀ j ∈ J, DifferentiableAt ℝ (f j) x) : HarmonicCalculus.along V (fun (y : E) => ∑ j ∈ J, f j y) x = ∑ j ∈ J, HarmonicCalculus.along V (f j) x

theorem NavierStokes.ParticularWaveAssembly.divergence_finset_sum {E ι : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (J : Finset ι) (R : E → ℝ) (Vr Vθ Vz : E → E) (v : ι → E → HarmonicCalculus.ComplexVector) {x : E} (hv : ∀ j ∈ J, ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : E) => v j y i) x) : HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz (fun (y : E) (i : Fin 3) => ∑ j ∈ J, v j y i) x = ∑ j ∈ J, HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz (v j) x

theorem NavierStokes.ParticularWaveAssembly.divergence_map {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : ℂ →L[ℝ] ℂ) (R : E → ℝ) (Vr Vθ Vz : E → E) {v : E → HarmonicCalculus.ComplexVector} {x : E} (hv : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : E) => v y i) x) : HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz (fun (y : E) (i : Fin 3) => L (v y i)) x = L (HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz v x)

theorem NavierStokes.ParticularWaveAssembly.real_divergence_sum_zero {E ι : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (J : Finset ι) (R : E → ℝ) (Vr Vθ Vz : E → E) (v : ι → E → HarmonicCalculus.ComplexVector) {x : E} (hv : ∀ j ∈ J, ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : E) => v j y i) x) (hdiv : ∀ j ∈ J, HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz (v j) x = 0) : HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz (fun (y : E) (i : Fin 3) => ↑(∑ j ∈ J, (v j y i).re)) x = 0

theorem NavierStokes.ParticularWaveAssembly.AssemblyData.wave_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : AssemblyData P} {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) (j : ℤ) (hj : j ∈ modes N) (n : ℕ) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (x : (P × ℝ) × TorusInverse.Plane) => HarmonicCalculus.vectorMode ((D.wave j).frequency n) ((D.wave j).phase n) ((D.wave j).amplitude n) x i) D.strip.domain

theorem NavierStokes.ParticularWaveAssembly.AssemblyData.pressure_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : AssemblyData P} {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) (j : ℤ) (hj : j ∈ modes N) (n : ℕ) : ContDiffOn ℝ (↑⊤) (HarmonicCalculus.mode ((D.wave j).frequency n) ((D.wave j).phase n) ((D.wave j).pressure n)) D.strip.domain

theorem NavierStokes.ParticularWaveAssembly.AssemblyData.divergence_zero {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : AssemblyData P} {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) (n : ℕ) {x : (P × ℝ) × TorusInverse.Plane} (hx : x ∈ D.strip.domain) : HarmonicCalculus.cylindricalDivergence (D.background.radius n) (D.directions.radialField n) (fun (x : (P × ℝ) × TorusInverse.Plane) => D.directions.angular) (D.directions.axialField D.strip n) (fun (y : (P × ℝ) × TorusInverse.Plane) (i : Fin 3) => ↑(D.velocity N n y i)) x = 0

theorem NavierStokes.ParticularWaveAssembly.AssemblyData.real_cancellation {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : AssemblyData P} {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) (hpos : 0 < N) (hN : (HarmonicResidual.residualBlock D.context D.state D.carrierBlock D.gaussianInput D.aliasInput).BandLimited N) (n : ℕ) (x : (P × TorusInverse.Plane) × ℝ) (hx : angleShuffle x ∈ D.strip.domain) : LinearWaveResidual.realComponentLinearResidual (D.strip.epsilon n) (D.background.radius n) (D.directions.radialField n) (fun (x : (P × ℝ) × TorusInverse.Plane) => D.directions.angular) (D.directions.axialField D.strip n) (LinearWaveResidual.timeDirection (D.strip.epsilon n) (D.directions.fastField n) fun (x : (P × ℝ) × TorusInverse.Plane) => D.directions.slow) (LinearWaveResidual.base (D.background.radius n) (D.background.radialBase n) (D.background.frequencyBase n) (D.background.axialBase n)) (D.velocity N n) (D.pressure N n) (angleShuffle x) + (HarmonicResidual.residualBlock D.context D.state D.carrierBlock D.gaussianInput D.aliasInput).oscillation n x = (D.goodBlock C).oscillation n x + (D.gaussianBlock C).oscillation n x

One actual real field cancels the current grouped residual, with the computed good field and both Gaussian tails retained on the right.