Weighted bounds for the actual linear wave remainder

The classes in this file bound iteratedFDeriv of the actual stripped coefficients uniformly in the band. Radial graph differentiation, axial rescaling, and the fast direction are kept explicit.

theorem NavierStokes.LinearWaveBounds.class_congr {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f g : ℕ → D → E} (hf : WeightedClasses.MemClass s w α f) (he : ∀ (n : ℕ), Set.EqOn (f n) (g n) s.domain) : WeightedClasses.MemClass s w α g

theorem NavierStokes.LinearWaveBounds.class_neg {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → E} (hf : WeightedClasses.MemClass s w α f) : WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => -f n x

theorem NavierStokes.LinearWaveBounds.class_sub {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f g : ℕ → D → E} (hf : WeightedClasses.MemClass s w α f) (hg : WeightedClasses.MemClass s w α g) : WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => f n x - g n x

theorem NavierStokes.LinearWaveBounds.unweighted_mul {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {α β : ℝ} {f g : ℕ → D → ℝ} (hf : WeightedClasses.UnweightedClass s α f) (hg : WeightedClasses.UnweightedClass s β g) : WeightedClasses.UnweightedClass s (α + β) fun (n : ℕ) (x : D) => f n x * g n x

theorem NavierStokes.LinearWaveBounds.unweighted_smul {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α β : ℝ} {f : ℕ → D → ℝ} {g : ℕ → D → E} (hf : WeightedClasses.UnweightedClass s α f) (hg : WeightedClasses.MemClass s w β g) : WeightedClasses.MemClass s w (α + β) fun (n : ℕ) (x : D) => f n x • g n x

theorem NavierStokes.LinearWaveBounds.real_mul_complex {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α β : ℝ} {f : ℕ → D → ℝ} {g : ℕ → D → ℂ} (hf : WeightedClasses.UnweightedClass s α f) (hg : WeightedClasses.MemClass s w β g) : WeightedClasses.MemClass s w (α + β) fun (n : ℕ) (x : D) => ↑(f n x) * g n x

theorem NavierStokes.LinearWaveBounds.complex_mul_real {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α β : ℝ} {f : ℕ → D → ℂ} {g : ℕ → D → ℝ} (hf : WeightedClasses.MemClass s w α f) (hg : WeightedClasses.UnweightedClass s β g) : WeightedClasses.MemClass s w (α + β) fun (n : ℕ) (x : D) => f n x * ↑(g n x)

theorem NavierStokes.LinearWaveBounds.constant_complex_mul {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → ℂ} (hf : WeightedClasses.MemClass s w α f) (c : ℂ) : WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => c * f n x

theorem NavierStokes.LinearWaveBounds.constant_real_mul {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → ℝ} (hf : WeightedClasses.MemClass s w α f) (c : ℝ) : WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => c * f n x

theorem NavierStokes.LinearWaveBounds.band_epsilon {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) : WeightedClasses.BandBound s 1 s.epsilon

theorem NavierStokes.LinearWaveBounds.mean_unweighted {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {α : ℝ} {f : ℕ → D → E} (hf : WeightedClasses.MeanClass s α f) (hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1) : WeightedClasses.UnweightedClass s α f

structure NavierStokes.LinearWaveBounds.GraphDirections (D : Type u_4) [NormedAddCommGroup D] [NormedSpace ℝ D] : Type u_4

Raw direction data. Its numerical and class hypotheses are separate.

• radial : D

  Radial of GraphDirections, of type D.

• auxiliary : D

  Auxiliary of GraphDirections, of type D.

• axial : D

  Axial of GraphDirections, of type D.

• angular : D

  Angular of GraphDirections, of type D.

• slow : D

  Slow of GraphDirections, of type D.

• fast : D

  Fast of GraphDirections, of type D.

• radialScale : ℕ → ℝ

  Radial scale of GraphDirections, of type ℕ → ℝ.

• fastScale : ℕ → ℝ

  Fast scale of GraphDirections, of type ℕ → ℝ.

• radialProfile : D → ℝ

  Radial profile of GraphDirections, of type D → ℝ.

noncomputable def NavierStokes.LinearWaveBounds.GraphDirections.radialField {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (d : GraphDirections D) (n : ℕ) (x : D) : D

Radial field, given by d.radial + d.radialScale n • (d.radialProfile x • d.auxiliary).

Equations

• d.radialField n x = d.radial + d.radialScale n • d.radialProfile x • d.auxiliary

noncomputable def NavierStokes.LinearWaveBounds.GraphDirections.axialField {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (d : GraphDirections D) (s : WeightedClasses.StripData D) (n : ℕ) : D → D

Axial field, given by s.epsilon n • d.axial.

Equations

• d.axialField s n x✝ = s.epsilon n • d.axial

noncomputable def NavierStokes.LinearWaveBounds.GraphDirections.fastField {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (d : GraphDirections D) (n : ℕ) : D → D

Fast field, given by d.fastScale n • d.fast.

Equations

• d.fastField n x✝ = d.fastScale n • d.fast

noncomputable def NavierStokes.LinearWaveBounds.GraphDirections.Dr {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : GraphDirections D) (f : ℕ → D → E) : ℕ → D → E

Dr, defined pointwise by along (d.radialField n) (f n).

Equations

• d.Dr f n = NavierStokes.HarmonicCalculus.along (d.radialField n) (f n)

noncomputable def NavierStokes.LinearWaveBounds.GraphDirections.Dz {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : GraphDirections D) (s : WeightedClasses.StripData D) (f : ℕ → D → E) : ℕ → D → E

Dz, defined pointwise by along (d.axialField s n) (f n).

Equations

• d.Dz s f n = NavierStokes.HarmonicCalculus.along (d.axialField s n) (f n)

noncomputable def NavierStokes.LinearWaveBounds.GraphDirections.Dt {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : GraphDirections D) (f : ℕ → D → E) : ℕ → D → E

Dt, defined pointwise by along (fun _ => d.slow) (f n).

Equations

• d.Dt f n = NavierStokes.HarmonicCalculus.along (fun (x : D) => d.slow) (f n)

noncomputable def NavierStokes.LinearWaveBounds.GraphDirections.Dfast {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : GraphDirections D) (f : ℕ → D → E) : ℕ → D → E

Dfast, defined pointwise by along (d.fastField n) (f n).

Equations

• d.Dfast f n = NavierStokes.HarmonicCalculus.along (d.fastField n) (f n)

theorem NavierStokes.LinearWaveBounds.GraphDirections.Dr_eq {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : GraphDirections D) (f : ℕ → D → E) : d.Dr f = WeightedClasses.graphDerivative d.radialScale d.radialProfile d.radial d.auxiliary f

theorem NavierStokes.LinearWaveBounds.GraphDirections.Dr_mem {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α κ : ℝ} (d : GraphDirections D) {f : ℕ → D → E} (hf : WeightedClasses.MemClass s w α f) (hρ : WeightedClasses.UnweightedClass s 0 fun (x : ℕ) => d.radialProfile) (hM : WeightedClasses.BandBound s (-κ) d.radialScale) (hκ : 0 ≤ κ) : WeightedClasses.MemClass s w (α - κ) (d.Dr f)

theorem NavierStokes.LinearWaveBounds.GraphDirections.Dz_mem {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} (d : GraphDirections D) {f : ℕ → D → E} (hf : WeightedClasses.MemClass s w α f) : WeightedClasses.MemClass s w (α + 1) (d.Dz s f)

theorem NavierStokes.LinearWaveBounds.GraphDirections.Dt_mem {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} (d : GraphDirections D) {f : ℕ → D → E} (hf : WeightedClasses.MemClass s w α f) : WeightedClasses.MemClass s w α (d.Dt f)

theorem NavierStokes.LinearWaveBounds.GraphDirections.Dfast_mem {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} (d : GraphDirections D) {f : ℕ → D → E} (hf : WeightedClasses.MemClass s w α f) (hfast : WeightedClasses.BandBound s 0 d.fastScale) : WeightedClasses.MemClass s w α (d.Dfast f)

theorem NavierStokes.LinearWaveBounds.GraphDirections.Dr_base_mem {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} (d : GraphDirections D) {f : ℕ → D → E} (hf : WeightedClasses.MemClass s w α f) (haux : ∀ (n : ℕ), ∀ x ∈ s.domain, (fderiv ℝ (f n) x) d.auxiliary = 0) : WeightedClasses.MemClass s w α (d.Dr f)

Base fields independent of the auxiliary coordinate incur no graph loss.

theorem NavierStokes.LinearWaveBounds.frequency_mul {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → ℂ} {kfreq : ℕ → ℝ} (hf : WeightedClasses.MemClass s w α f) (hkfreq : WeightedClasses.BandBound s (-(1 / 2)) kfreq) : WeightedClasses.MemClass s w (α - 1 / 2) fun (n : ℕ) (x : D) => HarmonicCalculus.phaseFactor (kfreq n) * f n x

structure NavierStokes.LinearWaveBounds.WaveCoefficients (D : Type u_4) : Type u_4

Families of actual phase, base, velocity, and pressure coefficients.

• radius : ℕ → D → ℝ

  Radius of WaveCoefficients, of type ℕ → D → ℝ.

• radialBase : ℕ → D → ℝ

  Radial base of WaveCoefficients, of type ℕ → D → ℝ.

• frequencyBase : ℕ → D → ℝ

  Frequency base of WaveCoefficients, of type ℕ → D → ℝ.

• axialBase : ℕ → D → ℝ

  Axial base of WaveCoefficients, of type ℕ → D → ℝ.

• phase : ℕ → D → ℝ

  Phase of WaveCoefficients, of type ℕ → D → ℝ.

• amplitude : ℕ → D → HarmonicCalculus.ComplexVector

  Amplitude of WaveCoefficients, of type ℕ → D → ComplexVector.

• pressure : ℕ → D → ℂ

  Pressure field of WaveCoefficients, of type ℕ → D → ℂ.

• frequency : ℕ → ℝ

  Frequency of WaveCoefficients, of type ℕ → ℝ.

noncomputable def NavierStokes.LinearWaveBounds.WaveCoefficients.normal {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : WaveCoefficients D) (s : WeightedClasses.StripData D) (d : GraphDirections D) (n : ℕ) : D → EuclideanSpace ℝ (Fin 3)

Normal, given by phaseNormal (a.radius n) (d.radialField n) (fun _ => d.angular) (d.axialField s n) (a.phase n).

Equations

• a.normal s d n = NavierStokes.HarmonicCalculus.phaseNormal (a.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n) (a.phase n)

noncomputable def NavierStokes.LinearWaveBounds.WaveCoefficients.defect {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : WaveCoefficients D) (s : WeightedClasses.StripData D) (d : GraphDirections D) (n : ℕ) : D → ℝ

Defect, constructed using LinearWaveResidual.materialPhaseDefect.

Equations

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

noncomputable def NavierStokes.LinearWaveBounds.WaveCoefficients.remainder {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : WaveCoefficients D) (s : WeightedClasses.StripData D) (d : GraphDirections D) (n : ℕ) : D → HarmonicCalculus.ComplexVector

Remainder, constructed using LinearWaveResidual.remainder.

Equations

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

noncomputable def NavierStokes.LinearWaveBounds.WaveCoefficients.principal {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : WaveCoefficients D) (s : WeightedClasses.StripData D) (d : GraphDirections D) (n : ℕ) : D → HarmonicCalculus.ComplexVector

Principal, constructed using LinearWaveResidual.principal.

Equations

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

noncomputable def NavierStokes.LinearWaveBounds.WaveCoefficients.principalVelocity {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : WaveCoefficients D) (s : WeightedClasses.StripData D) (d : GraphDirections D) (f : ℕ → D → HarmonicCalculus.ComplexVector) (n : ℕ) : D → HarmonicCalculus.ComplexVector

Principal velocity, constructed using LinearWaveResidual.principal.

Equations

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

noncomputable def NavierStokes.LinearWaveBounds.WaveCoefficients.addAmplitude {D : Type u_1} (a : WaveCoefficients D) (f : ℕ → D → HarmonicCalculus.ComplexVector) : WaveCoefficients D

Add amplitude, given by {a with amplitude := fun n x => a.amplitude n x + f n x}.

Equations

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

noncomputable def NavierStokes.LinearWaveBounds.WaveCoefficients.withCutoff {D : Type u_1} (a : WaveCoefficients D) (ψ : ℕ → D → ℝ) : WaveCoefficients D

With cutoff, given by { a with amplitude := fun n x => ψ n x • a.amplitude n x pressure := fun n x => (ψ n x : ℂ) * a.pressure n x }.

Equations

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

noncomputable def NavierStokes.LinearWaveBounds.WaveCoefficients.goodCoefficient {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : WaveCoefficients D) (s : WeightedClasses.StripData D) (d : GraphDirections D) (ψ : ℕ → D → ℝ) (f : ℕ → D → HarmonicCalculus.ComplexVector) (n : ℕ) (x : D) : HarmonicCalculus.ComplexVector

The retained coefficient after cutoff and exact-curl correction. The two slot tails are not included in this definition.

Equations

• a.goodCoefficient s d ψ f n x = a.principalVelocity s d f n x + ((a.withCutoff ψ).addAmplitude f).remainder s d n x

noncomputable def NavierStokes.LinearWaveBounds.WaveCoefficients.harmonicResidual {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : WaveCoefficients D) (s : WeightedClasses.StripData D) (d : GraphDirections D) (n : ℕ) : D → HarmonicCalculus.ComplexVector

Harmonic residual, constructed using LinearWaveResidual.linearResidual.

Equations

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

noncomputable def NavierStokes.LinearWaveBounds.WaveCoefficients.curlCorrection {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : WaveCoefficients D) (s : WeightedClasses.StripData D) (d : GraphDirections D) (n : ℕ) : D → HarmonicCalculus.ComplexVector

The actual coefficient error from taking the curl of the normalized harmonic vector potential.

Equations

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

noncomputable def NavierStokes.LinearWaveBounds.WaveCoefficients.curlPotential {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : WaveCoefficients D) (s : WeightedClasses.StripData D) (d : GraphDirections D) (n : ℕ) : D → HarmonicCalculus.ComplexVector

Curl potential, constructed using CurlClassBounds.vectorPotential.

Equations

• a.curlPotential s d n = NavierStokes.CurlClassBounds.vectorPotential (a.frequency n) (a.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n) (a.phase n) (a.amplitude n)

noncomputable def NavierStokes.LinearWaveBounds.WaveCoefficients.corrected {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : WaveCoefficients D) (s : WeightedClasses.StripData D) (d : GraphDirections D) (ψ : ℕ → D → ℝ) : WaveCoefficients D

Corrected, given by (a.withCutoff ψ).addAmplitude ((a.withCutoff ψ).curlCorrection s d).

Equations

• a.corrected s d ψ = (a.withCutoff ψ).addAmplitude ((a.withCutoff ψ).curlCorrection s d)

noncomputable def NavierStokes.LinearWaveBounds.WaveCoefficients.constructedGood {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : WaveCoefficients D) (s : WeightedClasses.StripData D) (d : GraphDirections D) (ψ : ℕ → D → ℝ) : ℕ → D → HarmonicCalculus.ComplexVector

Constructed good, given by a.goodCoefficient s d ψ ((a.withCutoff ψ).curlCorrection s d).

Equations

• a.constructedGood s d ψ = a.goodCoefficient s d ψ ((a.withCutoff ψ).curlCorrection s d)

structure NavierStokes.LinearWaveBounds.InputBounds {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (P : ℕ → D → ℝ) (α κ : ℝ) (d : GraphDirections D) (a : WaveCoefficients D) : Prop

Only primitive coefficient classes and scale bounds are inputs. No remainder or residual bound occurs in this structure.

• loss_nonneg : 0 ≤ κ
• zeta_le_one (x : D) : x ∈ s.domain → s.zeta x ≤ 1
• radial_profile : WeightedClasses.UnweightedClass s 0 fun (x : ℕ) => d.radialProfile
• radial_scale : WeightedClasses.BandBound s (-κ) d.radialScale
• fast_scale : WeightedClasses.BandBound s 0 d.fastScale
• frequency_scale : WeightedClasses.BandBound s (-(1 / 2)) a.frequency
• radius : WeightedClasses.UnweightedClass s 0 a.radius
• inverse_radius : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : D) => (a.radius n x)⁻¹
• radial_base : WeightedClasses.UnweightedClass s 1 a.radialBase
• frequency_base : WeightedClasses.UnweightedClass s 0 a.frequencyBase
• axial_base : WeightedClasses.UnweightedClass s 0 a.axialBase
• radial_base_aux (n : ℕ) (x : D) : x ∈ s.domain → (fderiv ℝ (a.radialBase n) x) d.auxiliary = 0
• frequency_base_aux (n : ℕ) (x : D) : x ∈ s.domain → (fderiv ℝ (a.frequencyBase n) x) d.auxiliary = 0
• axial_base_aux (n : ℕ) (x : D) : x ∈ s.domain → (fderiv ℝ (a.axialBase n) x) d.auxiliary = 0
• normal (i : Fin 3) : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : D) => (a.normal s d n x).ofLp i
• defect : WeightedClasses.UnweightedClass s 1 (a.defect s d)
• amplitude (i : Fin 3) : WeightedClasses.WaveClass s P α fun (n : ℕ) (x : D) => a.amplitude n x i
• pressure : WeightedClasses.WaveClass s P (α + 1 / 2) a.pressure

noncomputable def NavierStokes.LinearWaveBounds.insertComponent (i : Fin 3) : ℂ →L[ℝ] HarmonicCalculus.ComplexVector

Insert component, given by ContinuousLinearMap.pi fun j => if j = i then ContinuousLinearMap.id ℝ ℂ else 0.

Equations

• NavierStokes.LinearWaveBounds.insertComponent i = ContinuousLinearMap.pi fun (j : Fin 3) => if j = i then ContinuousLinearMap.id ℝ ℂ else 0

theorem NavierStokes.LinearWaveBounds.component_classes {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → HarmonicCalculus.ComplexVector} (hf : ∀ (i : Fin 3), WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => f n x i) : WeightedClasses.MemClass s w α f

theorem NavierStokes.LinearWaveBounds.angular_classes {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → HarmonicCalculus.ComplexVector} (hf : ∀ (i : Fin 3), WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => f n x i) (i : Fin 3) : WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => HarmonicCalculus.angularGenerator (f n x) i

theorem NavierStokes.LinearWaveBounds.InputBounds.b_unweighted {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) : WeightedClasses.UnweightedClass s 1 a.radialBase

theorem NavierStokes.LinearWaveBounds.InputBounds.inverse_radius_sq {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : D) => (a.radius n x ^ 2)⁻¹

theorem NavierStokes.LinearWaveBounds.InputBounds.base_components {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) (i : Fin 3) : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : D) => LinearWaveResidual.base (a.radius n) (a.radialBase n) (a.frequencyBase n) (a.axialBase n) x i

theorem NavierStokes.LinearWaveBounds.InputBounds.slowTransport_mem {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) (i : Fin 3) : WeightedClasses.WaveClass s P (α + 1 / 2 - 3 * κ) fun (n : ℕ) (x : D) => LinearWaveResidual.slowTransport (s.epsilon n) (a.radialBase n) (a.axialBase n) (fun (x : D) => d.slow) (d.radialField n) (d.axialField s n) (a.amplitude n) x i

theorem NavierStokes.LinearWaveBounds.InputBounds.phaseDefect_mem {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) (i : Fin 3) : WeightedClasses.WaveClass s P (α + 1 / 2 - 3 * κ) fun (n : ℕ) (x : D) => HarmonicCalculus.phaseFactor (a.frequency n) * ↑(a.defect s d n x) * a.amplitude n x i

theorem NavierStokes.LinearWaveBounds.InputBounds.baseDerivativeRemainder_mem {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) (i : Fin 3) : WeightedClasses.WaveClass s P (α + 1 / 2 - 3 * κ) fun (n : ℕ) (x : D) => LinearWaveResidual.baseDerivativeRemainder (a.radius n) (a.radialBase n) (a.frequencyBase n) (a.axialBase n) (d.radialField n) (d.axialField s n) (a.amplitude n) x i

theorem NavierStokes.LinearWaveBounds.InputBounds.pressureGradient_mem {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) (i : Fin 3) : WeightedClasses.WaveClass s P (α + 1 / 2 - 3 * κ) fun (n : ℕ) (x : D) => LinearWaveResidual.strippedPressureGradient (d.radialField n) (d.axialField s n) (a.pressure n) x i

theorem NavierStokes.LinearWaveBounds.InputBounds.viscousRemainder_mem {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) (i : Fin 3) : WeightedClasses.WaveClass s P (α - 1 / 2 - 3 * κ) fun (n : ℕ) (x : D) => LinearWaveResidual.viscousRemainder (a.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n) (a.frequency n) (a.phase n) (a.amplitude n) x i

theorem NavierStokes.LinearWaveBounds.InputBounds.viscousPart_mem {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) (i : Fin 3) : WeightedClasses.WaveClass s P (α + 1 / 2 - 3 * κ) fun (n : ℕ) (x : D) => ↑(s.epsilon n) * LinearWaveResidual.viscousRemainder (a.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n) (a.frequency n) (a.phase n) (a.amplitude n) x i

theorem NavierStokes.LinearWaveBounds.InputBounds.remainder_components {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) (i : Fin 3) : WeightedClasses.WaveClass s P (α + 1 / 2 - 3 * κ) fun (n : ℕ) (x : D) => a.remainder s d n x i

Every concrete term of (31), including the two frame corrections, has the claimed all-jet weighted bound.

theorem NavierStokes.LinearWaveBounds.InputBounds.remainder_class {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) : WeightedClasses.WaveClass s P (α + 1 / 2 - 3 * κ) (a.remainder s d)

theorem NavierStokes.LinearWaveBounds.InputBounds.normal_norm_sq {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : D) => ‖a.normal s d n x‖ ^ 2

theorem NavierStokes.LinearWaveBounds.InputBounds.shear_mem {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) {β : ℝ} {f : ℕ → D → HarmonicCalculus.ComplexVector} (hf : ∀ (i : Fin 3), WeightedClasses.WaveClass s P β fun (n : ℕ) (x : D) => f n x i) (i : Fin 3) : WeightedClasses.WaveClass s P β fun (n : ℕ) (x : D) => LinearWaveResidual.shear (a.radius n) (a.frequencyBase n) (a.axialBase n) (d.radialField n) (f n) x i

theorem NavierStokes.LinearWaveBounds.InputBounds.principalVelocity_components {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) {β : ℝ} {f : ℕ → D → HarmonicCalculus.ComplexVector} (hf : ∀ (i : Fin 3), WeightedClasses.WaveClass s P β fun (n : ℕ) (x : D) => f n x i) (i : Fin 3) : WeightedClasses.WaveClass s P β fun (n : ℕ) (x : D) => a.principalVelocity s d f n x i

The velocity principal operator has no negative epsilon exponent: the fast derivative is stripped and epsilon * frequency² has order zero.

theorem NavierStokes.LinearWaveBounds.InputBounds.principalVelocity_class {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) {β : ℝ} {f : ℕ → D → HarmonicCalculus.ComplexVector} (hf : ∀ (i : Fin 3), WeightedClasses.WaveClass s P β fun (n : ℕ) (x : D) => f n x i) : WeightedClasses.WaveClass s P β (a.principalVelocity s d f)

theorem NavierStokes.LinearWaveBounds.InputBounds.curl_principal_gain {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) {f : ℕ → D → HarmonicCalculus.ComplexVector} (hf : ∀ (i : Fin 3), WeightedClasses.WaveClass s P (α + 1 / 2 - κ) fun (n : ℕ) (x : D) => f n x i) : WeightedClasses.WaveClass s P (α + 1 / 2 - 3 * κ) (a.principalVelocity s d f)

A curl coefficient remainder retains its gain under the principal operator.

theorem NavierStokes.LinearWaveBounds.InputBounds.add_curl_amplitude {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) (hκ : κ ≤ 1 / 2) {f : ℕ → D → HarmonicCalculus.ComplexVector} (hf : ∀ (i : Fin 3), WeightedClasses.WaveClass s P (α + 1 / 2 - κ) fun (n : ℕ) (x : D) => f n x i) : InputBounds s P α κ d (a.addAmplitude f)

Adding the actual curl coefficient difference preserves the input wave class.

theorem NavierStokes.LinearWaveBounds.InputBounds.with_cutoff {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) {ψ : ℕ → D → ℝ} (hψ : WeightedClasses.UnweightedClass s 0 ψ) : InputBounds s P α κ d (a.withCutoff ψ)

theorem NavierStokes.LinearWaveBounds.InputBounds.goodCoefficient_class {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) (hκ : κ ≤ 1 / 2) {ψ : ℕ → D → ℝ} (hψ : WeightedClasses.UnweightedClass s 0 ψ) {f : ℕ → D → HarmonicCalculus.ComplexVector} (hf : ∀ (i : Fin 3), WeightedClasses.WaveClass s P (α + 1 / 2 - κ) fun (n : ℕ) (x : D) => f n x i) : WeightedClasses.WaveClass s P (α + 1 / 2 - 3 * κ) (a.goodCoefficient s d ψ f)

theorem NavierStokes.LinearWaveBounds.InputBounds.curlCorrection_class {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) {R : D → ℝ} (hR : a.radius = fun (x : ℕ) => R) (hN : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain s) (a.normal s d)) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ ‖a.normal s d n x‖) (hupper : ∀ (n : ℕ), ∀ x ∈ s.domain, ‖a.normal s d n x‖ ≤ M) (hK : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / a.frequency n) : WeightedClasses.WaveClass s P (α + 1 / 2 - κ) (a.curlCorrection s d)

The preceding principal estimate now uses the constructed curl error, whose class follows from primitive normal and amplitude jets.

theorem NavierStokes.LinearWaveBounds.InputBounds.constructed_goodCoefficient_class {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) (hκ : κ ≤ 1 / 2) {ψ : ℕ → D → ℝ} (hψ : WeightedClasses.UnweightedClass s 0 ψ) {R : D → ℝ} (hR : a.radius = fun (x : ℕ) => R) (hN : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain s) (a.normal s d)) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ ‖a.normal s d n x‖) (hupper : ∀ (n : ℕ), ∀ x ∈ s.domain, ‖a.normal s d n x‖ ≤ M) (hK : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / a.frequency n) : WeightedClasses.WaveClass s P (α + 1 / 2 - 3 * κ) (a.goodCoefficient s d ψ ((a.withCutoff ψ).curlCorrection s d))

theorem NavierStokes.LinearWaveBounds.InputBounds.principal_add_curl {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) {β : ℝ} {f : ℕ → D → HarmonicCalculus.ComplexVector} (hf : ∀ (i : Fin 3), WeightedClasses.WaveClass s P β fun (n : ℕ) (x : D) => f n x i) (n : ℕ) {x : D} (hx : x ∈ s.domain) : (a.addAmplitude f).principal s d n x = a.principal s d n x + a.principalVelocity s d f n x

Exact additivity in the supplied coefficient, while retaining the same projected pressure. It does not replace a curl coefficient by a tangent one.

theorem NavierStokes.LinearWaveBounds.InputBounds.corrected_good_coefficient {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) (hκ : κ ≤ 1 / 2) {f source : ℕ → D → HarmonicCalculus.ComplexVector} (hf : ∀ (i : Fin 3), WeightedClasses.WaveClass s P (α + 1 / 2 - κ) fun (n : ℕ) (x : D) => f n x i) (hsolve : ∀ (n : ℕ), ∀ x ∈ s.domain, a.principal s d n x = -source n x) : WeightedClasses.WaveClass s P (α + 1 / 2 - 3 * κ) fun (n : ℕ) (x : D) => (a.addAmplitude f).principal s d n x + (a.addAmplitude f).remainder s d n x + source n x

After the actual principal equation is solved for the tangent coefficient, the corrected coefficient's remaining source has the claimed class.

structure NavierStokes.LinearWaveBounds.ExactConditions {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (d : GraphDirections D) (a : WaveCoefficients D) : Prop

These hypotheses are the actual local geometric and angular conditions needed to apply the exact differential identity.

• phase_smooth (n : ℕ) : ContDiffOn ℝ (↑⊤) (a.phase n) s.domain
• radius_nonzero (n : ℕ) (x : D) : x ∈ s.domain → a.radius n x ≠ 0
• radial_radius (n : ℕ) (x : D) : x ∈ s.domain → HarmonicCalculus.along (d.radialField n) (a.radius n) x = 1
• base_angular (n : ℕ) (x : D) : x ∈ s.domain → ∀ (i : Fin 3), HarmonicCalculus.along (fun (x : D) => d.angular) (fun (y : D) => LinearWaveResidual.base (a.radius n) (a.radialBase n) (a.frequencyBase n) (a.axialBase n) y i) x = 0
• amplitude_angular (n : ℕ) (i : Fin 3) : Set.EqOn (HarmonicCalculus.along (fun (x : D) => d.angular) fun (y : D) => a.amplitude n y i) (fun (x : D) => 0) s.domain
• phase_angular (n : ℕ) : ∃ (p : ℝ), Set.EqOn (HarmonicCalculus.along (fun (x : D) => d.angular) (a.phase n)) (fun (x : D) => p) s.domain
• pressure_angular (n : ℕ) (x : D) : x ∈ s.domain → HarmonicCalculus.along (fun (x : D) => d.angular) (a.pressure n) x = 0

theorem NavierStokes.LinearWaveBounds.harmonicResidual_eq {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) (hg : ExactConditions s d a) (n : ℕ) {x : D} (hx : x ∈ s.domain) : a.harmonicResidual s d n x = fun (i : Fin 3) => (a.principal s d n x i + a.remainder s d n x i) * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x

theorem NavierStokes.LinearWaveBounds.curlPotential_realizes {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) (n : ℕ) (G : CurlClassBounds.CylindricalGeometry s.domain (a.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n)) (hK : a.frequency n ≠ 0) (hΦ : ContDiffOn ℝ (↑⊤) (a.phase n) s.domain) (hn : ∀ x ∈ s.domain, a.normal s d n x ≠ 0) (ht : ∀ x ∈ s.domain, HarmonicCalculus.normalDot (a.normal s d n x) (a.amplitude n x) = 0) {x : D} (hx : x ∈ s.domain) : CurlClassBounds.cylindricalCurl (a.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n) (a.curlPotential s d n) x = HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) ((a.addAmplitude (a.curlCorrection s d)).amplitude n) x

The correction used in the estimates is realized by an actual curl.

theorem NavierStokes.LinearWaveBounds.curlCorrection_divergence {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) (n : ℕ) (G : CurlClassBounds.CylindricalGeometry s.domain (a.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n)) (hK : a.frequency n ≠ 0) (hΦ : ContDiffOn ℝ (↑⊤) (a.phase n) s.domain) (hn : ∀ x ∈ s.domain, a.normal s d n x ≠ 0) (ht : ∀ x ∈ s.domain, HarmonicCalculus.normalDot (a.normal s d n x) (a.amplitude n x) = 0) {x : D} (hx : x ∈ s.domain) : HarmonicCalculus.cylindricalDivergence (a.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n) (HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) ((a.addAmplitude (a.curlCorrection s d)).amplitude n)) x = 0

theorem NavierStokes.LinearWaveBounds.cutoff_tangent {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {d : GraphDirections D} {a : WaveCoefficients D} (ψ : ℕ → D → ℝ) (n : ℕ) (ht : ∀ x ∈ s.domain, HarmonicCalculus.normalDot (a.normal s d n x) (a.amplitude n x) = 0) (x : D) : x ∈ s.domain → HarmonicCalculus.normalDot ((a.withCutoff ψ).normal s d n x) ((a.withCutoff ψ).amplitude n x) = 0

theorem NavierStokes.LinearWaveBounds.corrected_realizes_curl {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) {ψ : ℕ → D → ℝ} (hψ : WeightedClasses.UnweightedClass s 0 ψ) (n : ℕ) (G : CurlClassBounds.CylindricalGeometry s.domain (a.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n)) (hK : a.frequency n ≠ 0) (hΦ : ContDiffOn ℝ (↑⊤) (a.phase n) s.domain) (hn : ∀ x ∈ s.domain, a.normal s d n x ≠ 0) (ht : ∀ x ∈ s.domain, HarmonicCalculus.normalDot (a.normal s d n x) (a.amplitude n x) = 0) {x : D} (hx : x ∈ s.domain) : CurlClassBounds.cylindricalCurl (a.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n) ((a.withCutoff ψ).curlPotential s d n) x = HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) ((a.corrected s d ψ).amplitude n) x

Under the nondegeneracy and tangency hypotheses, the actual cutoff potential realizes the same corrected velocity whose residual is estimated.

theorem NavierStokes.LinearWaveBounds.corrected_divergence {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) {ψ : ℕ → D → ℝ} (hψ : WeightedClasses.UnweightedClass s 0 ψ) (n : ℕ) (G : CurlClassBounds.CylindricalGeometry s.domain (a.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n)) (hK : a.frequency n ≠ 0) (hΦ : ContDiffOn ℝ (↑⊤) (a.phase n) s.domain) (hn : ∀ x ∈ s.domain, a.normal s d n x ≠ 0) (ht : ∀ x ∈ s.domain, HarmonicCalculus.normalDot (a.normal s d n x) (a.amplitude n x) = 0) {x : D} (hx : x ∈ s.domain) : HarmonicCalculus.cylindricalDivergence (a.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n) (HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) ((a.corrected s d ψ).amplitude n)) x = 0

noncomputable def NavierStokes.LinearWaveBounds.excludedSlotError {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (d : GraphDirections D) (ψ : ℕ → D → ℝ) (a source : ℕ → D → HarmonicCalculus.ComplexVector) : ℕ → D → HarmonicCalculus.ComplexVector

The two excluded slot terms remain explicit fields. Their Gaussian flatness is a separate analytic theorem, never an instruction to set them to zero.

Equations

• NavierStokes.LinearWaveBounds.excludedSlotError d ψ a source n x = d.Dfast ψ n x • a n x + (1 - ψ n x) • source n x

theorem NavierStokes.LinearWaveBounds.principal_cutoff {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) (ψ : ℕ → D → ℝ) (source : ℕ → D → HarmonicCalculus.ComplexVector) (n : ℕ) {x : D} (hx : x ∈ s.domain) (hψ : DifferentiableAt ℝ (ψ n) x) : (a.withCutoff ψ).principal s d n x + source n x = ψ n x • (a.principal s d n x + source n x) + excludedSlotError d ψ a.amplitude source n x

theorem NavierStokes.LinearWaveBounds.principal_cutoff_of_solve {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) (ψ : ℕ → D → ℝ) (source : ℕ → D → HarmonicCalculus.ComplexVector) (n : ℕ) {x : D} (hx : x ∈ s.domain) (hψ : DifferentiableAt ℝ (ψ n) x) (hsolve : a.principal s d n x = -source n x) : (a.withCutoff ψ).principal s d n x + source n x = excludedSlotError d ψ a.amplitude source n x

theorem NavierStokes.LinearWaveBounds.corrected_coefficient_eq_good_add_excluded {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) {ψ : ℕ → D → ℝ} (hψ : WeightedClasses.UnweightedClass s 0 ψ) {f source : ℕ → D → HarmonicCalculus.ComplexVector} {β : ℝ} (hf : ∀ (i : Fin 3), WeightedClasses.WaveClass s P β fun (n : ℕ) (x : D) => f n x i) (n : ℕ) {x : D} (hx : x ∈ s.domain) (hsolve : a.principal s d n x = -source n x) : ((a.withCutoff ψ).addAmplitude f).principal s d n x + ((a.withCutoff ψ).addAmplitude f).remainder s d n x + source n x = a.goodCoefficient s d ψ f n x + excludedSlotError d ψ a.amplitude source n x

The entire stripped source, with both cutoff tails still present as an explicit additive field. The curl correction is supplied to the actual operator.

theorem NavierStokes.LinearWaveBounds.harmonicResidual_eq_good_add_excluded {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) (hκ : κ ≤ 1 / 2) {ψ : ℕ → D → ℝ} (hψ : WeightedClasses.UnweightedClass s 0 ψ) {f source : ℕ → D → HarmonicCalculus.ComplexVector} (hf : ∀ (i : Fin 3), WeightedClasses.WaveClass s P (α + 1 / 2 - κ) fun (n : ℕ) (x : D) => f n x i) (hg : ExactConditions s d ((a.withCutoff ψ).addAmplitude f)) (n : ℕ) {x : D} (hx : x ∈ s.domain) (hsolve : a.principal s d n x = -source n x) : (((a.withCutoff ψ).addAmplitude f).harmonicResidual s d n x + fun (i : Fin 3) => source n x i * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x) = fun (i : Fin 3) => (a.goodCoefficient s d ψ f n x i + excludedSlotError d ψ a.amplitude source n x i) * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x

Actual harmonic linearization, including the source, equals the proved good coefficient plus the explicitly retained slot error, times the carrier.

theorem NavierStokes.LinearWaveBounds.linear_wave_bound_with_excluded_error {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) (hκ : κ ≤ 1 / 2) {ψ : ℕ → D → ℝ} (hψ : WeightedClasses.UnweightedClass s 0 ψ) {f source : ℕ → D → HarmonicCalculus.ComplexVector} (hf : ∀ (i : Fin 3), WeightedClasses.WaveClass s P (α + 1 / 2 - κ) fun (n : ℕ) (x : D) => f n x i) (hsolve : ∀ (n : ℕ), ∀ x ∈ s.domain, a.principal s d n x = -source n x) : WeightedClasses.WaveClass s P (α + 1 / 2 - 3 * κ) (a.goodCoefficient s d ψ f) ∧ ∀ (n : ℕ), ∀ x ∈ s.domain, ((a.withCutoff ψ).addAmplitude f).principal s d n x + ((a.withCutoff ψ).addAmplitude f).remainder s d n x + source n x = a.goodCoefficient s d ψ f n x + excludedSlotError d ψ a.amplitude source n x

theorem NavierStokes.LinearWaveBounds.constructed_linear_wave_with_excluded {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) (hκ : κ ≤ 1 / 2) {ψ : ℕ → D → ℝ} (hψ : WeightedClasses.UnweightedClass s 0 ψ) {R : D → ℝ} (hR : a.radius = fun (x : ℕ) => R) (hN : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain s) (a.normal s d)) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ ‖a.normal s d n x‖) (hupper : ∀ (n : ℕ), ∀ x ∈ s.domain, ‖a.normal s d n x‖ ≤ M) (hK : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / a.frequency n) {source : ℕ → D → HarmonicCalculus.ComplexVector} (hsolve : ∀ (n : ℕ), ∀ x ∈ s.domain, a.principal s d n x = -source n x) (hg : ExactConditions s d (a.corrected s d ψ)) : WeightedClasses.WaveClass s P (α + 1 / 2 - 3 * κ) (a.constructedGood s d ψ) ∧ ∀ (n : ℕ), ∀ x ∈ s.domain, ((a.corrected s d ψ).harmonicResidual s d n x + fun (i : Fin 3) => source n x i * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x) = fun (i : Fin 3) => (a.constructedGood s d ψ n x i + excludedSlotError d ψ a.amplitude source n x i) * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x

The complete exact identity and good class for the constructed curl coefficient. Every estimate on the correction is obtained from primitive jets.

theorem NavierStokes.LinearWaveBounds.excludedSlotError_eq_gaussianError {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} (g : GaussianTailFlat.SlotFamily s) (d : GraphDirections D) (hfast : ∀ (n : ℕ), (g.linear n) (d.fastScale n • d.fast) = (g.length n)⁻¹) (a source : ℕ → D → HarmonicCalculus.ComplexVector) : excludedSlotError d g.cutoff a source = g.error a source

The cutoff error in the differential identity is precisely the field whose Gaussian estimates are proved in GaussianTailFlat.

theorem NavierStokes.LinearWaveBounds.excludedSlotError_all_gains {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} (g : GaussianTailFlat.SlotFamily s) (d : GraphDirections D) (hfast : ∀ (n : ℕ), (g.linear n) (d.fastScale n • d.fast) = (g.length n)⁻¹) (edges : GaussianTailFlat.FlatEdges s) (scales : GaussianTailFlat.BandScaleControl s) {P : ℕ → D → ℝ} {α c : ℝ} {a source : ℕ → D → HarmonicCalculus.ComplexVector} (ha : WeightedClasses.WaveClass s P α a) (hf : WeightedClasses.WaveClass s P α source) (hc : 0 < c) (hP : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ Real.exp (-c * (g.coordinate n x - 1 / 2) ^ 2 * g.length n)) (N : ℝ) : WeightedClasses.UnweightedClass s N (excludedSlotError d g.cutoff a source)

theorem NavierStokes.LinearWaveBounds.excludedSlotError_stripped_bound {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} (g : GaussianTailFlat.SlotFamily s) (d : GraphDirections D) (hfast : ∀ (n : ℕ), (g.linear n) (d.fastScale n • d.fast) = (g.length n)⁻¹) (edges : GaussianTailFlat.FlatEdges s) (scales : GaussianTailFlat.BandScaleControl s) {P : ℕ → D → ℝ} {α c : ℝ} {a source : ℕ → D → HarmonicCalculus.ComplexVector} (ha : WeightedClasses.WaveClass s P α a) (hf : WeightedClasses.WaveClass s P α source) (hc : 0 < c) (hP : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ Real.exp (-c * (g.coordinate n x - 1 / 2) ^ 2 * g.length n)) (m : ℕ) (N : ℝ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ j ≤ m, ‖iteratedFDeriv ℝ j (excludedSlotError d g.cutoff a source n) x‖ ≤ C * ChartScales.Q n ^ N

All actual stripped jets of the retained error decay to arbitrary order, uniformly including approach to the flat spatial support edges.

theorem NavierStokes.LinearWaveBounds.constructed_linear_wave_with_flat_error {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {d : GraphDirections D} {a : WaveCoefficients D} (h : InputBounds s P α κ d a) (hκ : κ ≤ 1 / 2) (g : GaussianTailFlat.SlotFamily s) (hfast : ∀ (n : ℕ), (g.linear n) (d.fastScale n • d.fast) = (g.length n)⁻¹) (edges : GaussianTailFlat.FlatEdges s) (scales : GaussianTailFlat.BandScaleControl s) {source : ℕ → D → HarmonicCalculus.ComplexVector} (hsource : WeightedClasses.WaveClass s P α source) {c : ℝ} (hc : 0 < c) (hP : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ Real.exp (-c * (g.coordinate n x - 1 / 2) ^ 2 * g.length n)) {R : D → ℝ} (hR : a.radius = fun (x : ℕ) => R) (hN : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain s) (a.normal s d)) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ ‖a.normal s d n x‖) (hupper : ∀ (n : ℕ), ∀ x ∈ s.domain, ‖a.normal s d n x‖ ≤ M) (hK : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / a.frequency n) (hsolve : ∀ (n : ℕ), ∀ x ∈ s.domain, a.principal s d n x = -source n x) (hg : ExactConditions s d (a.corrected s d g.cutoff)) : WeightedClasses.WaveClass s P (α + 1 / 2 - 3 * κ) (a.constructedGood s d g.cutoff) ∧ (∀ (N : ℝ), WeightedClasses.UnweightedClass s N (excludedSlotError d g.cutoff a.amplitude source)) ∧ ∀ (n : ℕ), ∀ x ∈ s.domain, ((a.corrected s d g.cutoff).harmonicResidual s d n x + fun (i : Fin 3) => source n x i * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x) = fun (i : Fin 3) => (a.constructedGood s d g.cutoff n x i + excludedSlotError d g.cutoff a.amplitude source n x i) * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x

Proposition 9.3 at the coefficient level: the actual harmonic residual has the proved good class plus an explicitly proved all-order flat error.

theorem NavierStokes.LinearWaveBounds.excludedSlotError_carrier_physical_bound {s : WeightedClasses.StripData PhysicalGraphBounds.LiftPoint} (g : GaussianTailFlat.SlotFamily s) (d : GraphDirections PhysicalGraphBounds.LiftPoint) (hfast : ∀ (n : ℕ), (g.linear n) (d.fastScale n • d.fast) = (g.length n)⁻¹) (edges : GaussianTailFlat.FlatEdges s) (scales : GaussianTailFlat.BandScaleControl s) {P : ℕ → PhysicalGraphBounds.LiftPoint → ℝ} {α c : ℝ} {a source : ℕ → PhysicalGraphBounds.LiftPoint → HarmonicCalculus.ComplexVector} (ha : WeightedClasses.WaveClass s P α a) (hf : WeightedClasses.WaveClass s P α source) (hc : 0 < c) (hP : ∀ (n : ℕ), ∀ x ∈ s.domain, P n x ≤ Real.exp (-c * (g.coordinate n x - 1 / 2) ^ 2 * g.length n)) (ha_smooth : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (a n) {x : PhysicalGraphBounds.LiftPoint | g.coordinate n x ∈ Set.Ioo 0 1}) (hf_smooth : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (source n)) {h rLower rUpper B e H : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 2) (hrLower : 0 < rLower) (hB : 1 ≤ B) (he : 0 ≤ e) (hH : 0 ≤ H) (i : Fin 3) (m : ℕ) (N : ℝ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), 4 ≤ n → ∀ (p : ProblemStatement.SpaceTime), (PhysicalGraphBounds.scaledRadial n) p ∈ PhysicalGraphBounds.annulus rLower rUpper → |p.1| ≤ 1 → PhysicalGraphBounds.physicalLift h n p ∈ s.domain → ∀ (q : ℝ), 0 < q → q / 2 ≤ ChartScales.Q n → ChartScales.Q n ≤ 2 * q → ∀ (Φ : PhysicalGraphBounds.LiftPoint → ℝ) (j : ℤ), ContDiff ℝ (↑⊤) Φ → |↑j| ≤ H → (∀ k ≤ m, ‖iteratedFDeriv ℝ k Φ (PhysicalGraphBounds.physicalLift h n p)‖ ≤ B * ChartScales.S n ^ e * ChartScales.Q n ^ (-1)) → ‖iteratedFDeriv ℝ m ((fun (y : PhysicalGraphBounds.LiftPoint) => excludedSlotError d g.cutoff a source n y i * PhysicalGraphBounds.character (↑(ChartScales.carrier h n) * ↑j) (Φ y)) ∘ PhysicalGraphBounds.physicalLift h n) p‖ ≤ C * q ^ N

The retained error remains flat after multiplication by the actual rounded harmonic carrier and restriction to the physical graph.