Actual reference particular waves in physical coordinates

The input is the constructed reference Volterra solve. Curl identities are conclusions, not compatibility assumptions on solved velocities.

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

Raw common, given by actualCommonCoefficients D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background.

Equations

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

noncomputable def NavierStokes.PhysicalParticularWave.commonPotential {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (D : ParticularWaveAssembly.AssemblyData P) (j : ℤ) (n : ℕ) : (P × ℝ) × TorusInverse.Plane → HarmonicCalculus.ComplexVector

Common potential, given by (rawCommon D j).curlPotential D.strip D.directions n.

Equations

• NavierStokes.PhysicalParticularWave.commonPotential D j n = (NavierStokes.PhysicalParticularWave.rawCommon D j).curlPotential D.strip D.directions n

noncomputable def NavierStokes.PhysicalParticularWave.commonPressure {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (D : ParticularWaveAssembly.AssemblyData P) (j : ℤ) (n : ℕ) : (P × ℝ) × TorusInverse.Plane → ℂ

Common pressure, given by mode ((rawCommon D j).frequency n) ((rawCommon D j).phase n) ((rawCommon D j).pressure n).

Equations

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

theorem NavierStokes.PhysicalParticularWave.commonRaw_germ {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (D : ParticularWaveAssembly.AssemblyData P) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) (n : ℕ) {x : (P × ℝ) × TorusInverse.Plane} (hx : x ∈ D.strip.domain) : (rawCommon D j).amplitude n =ᶠ[nhds x] fun (y : (P × ℝ) × TorusInverse.Plane) => C.slot.cutoff n y • (ParticularWaveAssembly.actualCopyCoefficients D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy).amplitude n y

theorem NavierStokes.PhysicalParticularWave.commonRaw_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (D : ParticularWaveAssembly.AssemblyData P) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((rawCommon D j).amplitude n) D.strip.domain

theorem NavierStokes.PhysicalParticularWave.commonRaw_tangent {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (D : ParticularWaveAssembly.AssemblyData P) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) (n : ℕ) {x : (P × ℝ) × TorusInverse.Plane} (hx : x ∈ D.strip.domain) : HarmonicCalculus.normalDot ((rawCommon D j).normal D.strip D.directions n x) ((rawCommon D j).amplitude n x) = 0

theorem NavierStokes.PhysicalParticularWave.commonPotential_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (D : ParticularWaveAssembly.AssemblyData P) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) (n : ℕ) : ContDiffOn ℝ (↑⊤) (commonPotential D j n) D.strip.domain

theorem NavierStokes.PhysicalParticularWave.commonPotential_curl {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (D : ParticularWaveAssembly.AssemblyData P) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) (n : ℕ) {x : (P × ℝ) × TorusInverse.Plane} (hx : x ∈ D.strip.domain) : CurlClassBounds.cylindricalCurl (D.background.radius n) (D.directions.radialField n) (fun (x : (P × ℝ) × TorusInverse.Plane) => D.directions.angular) (D.directions.axialField D.strip n) (commonPotential D j n) x = HarmonicCalculus.vectorMode ((D.wave j).frequency n) ((D.wave j).phase n) ((D.wave j).amplitude n) x

The constructed common coefficient, including its native cutoff, gives exactly the wave already used by the assembly.

theorem NavierStokes.PhysicalParticularWave.commonPotential_fullTurn {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (D : ParticularWaveAssembly.AssemblyData P) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) (n : ℕ) (x : (P × ℝ) × TorusInverse.Plane) : commonPotential D j n (x + (2 * Real.pi) • D.directions.angular) = commonPotential D j n x

theorem NavierStokes.PhysicalParticularWave.commonPressure_fullTurn {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (D : ParticularWaveAssembly.AssemblyData P) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) (n : ℕ) (x : (P × ℝ) × TorusInverse.Plane) : commonPressure D j n (x + (2 * Real.pi) • D.directions.angular) = commonPressure D j n x

The actual physical changes of band and cover

@[reducible, inline]

abbrev NavierStokes.PhysicalParticularWave.Lift : Type

Lift: an abbreviation for PhysicalResidualBridge.Lift.

Equations

• NavierStokes.PhysicalParticularWave.Lift = NavierStokes.PhysicalResidualBridge.Lift

@[reducible, inline]

abbrev NavierStokes.PhysicalParticularWave.Cylinder : Type

Cylinder: an abbreviation for PhysicalResidualBridge.Cylinder.

Equations

• NavierStokes.PhysicalParticularWave.Cylinder = NavierStokes.PhysicalResidualBridge.Cylinder

@[reducible, inline]

abbrev NavierStokes.PhysicalParticularWave.Parameter : Type

Parameter: an abbreviation for ℝ × Plane.

Equations

• NavierStokes.PhysicalParticularWave.Parameter = (ℝ × NavierStokes.TorusInverse.Plane)

@[reducible, inline]

abbrev NavierStokes.PhysicalParticularWave.WaveSpace : Type

Wave space: an abbreviation for (Parameter × ℝ) × Plane.

Equations

• NavierStokes.PhysicalParticularWave.WaveSpace = ((NavierStokes.PhysicalParticularWave.Parameter × ℝ) × NavierStokes.TorusInverse.Plane)

noncomputable def NavierStokes.PhysicalParticularWave.waveEquiv : Cylinder ≃ₗᵢ[ℝ] WaveSpace

The wave solver uses (R,(T,Z),theta,Y). The physical graph theorem uses (R,(Z,T),Y,theta). This is the literal isometric reordering.

Equations

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

@[simp]

theorem NavierStokes.PhysicalParticularWave.waveEquiv_apply (x : Cylinder) : waveEquiv x = (((x.1.1, x.1.2.1.2, x.1.2.1.1), x.2), x.1.2.2)

noncomputable def NavierStokes.PhysicalParticularWave.nativeMap (h Q : ℝ) (i : ℕ) (z : ProblemStatement.SpaceTime) : WaveSpace

Native map, given by waveEquiv ((PhysicalResidualBridge.commonGraph Q h i).map z).

Equations

• NavierStokes.PhysicalParticularWave.nativeMap h Q i z = NavierStokes.PhysicalParticularWave.waveEquiv ((NavierStokes.PhysicalResidualBridge.commonGraph Q h i).map z)

noncomputable def NavierStokes.PhysicalParticularWave.ratioPower (Q Qr a : ℝ) : ℝ

Ratio power, given by Q ^ a / Qr ^ a.

Equations

• NavierStokes.PhysicalParticularWave.ratioPower Q Qr a = Q ^ a / Qr ^ a

theorem NavierStokes.PhysicalParticularWave.ratioPower_pos {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (a : ℝ) : 0 < ratioPower Q Qr a

theorem NavierStokes.PhysicalParticularWave.ratioPower_cancel {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (a : ℝ) : ratioPower Q Qr a * Q ^ (-a) = Qr ^ (-a)

theorem NavierStokes.PhysicalParticularWave.ratioPower_neg_div {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (a : ℝ) : Qr ^ (-a) / Q ^ (-a) = ratioPower Q Qr a

theorem NavierStokes.PhysicalParticularWave.ratioPower_mul {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (a b : ℝ) : ratioPower Q Qr a * ratioPower Q Qr b = ratioPower Q Qr (a + b)

theorem NavierStokes.PhysicalParticularWave.ratioPower_div {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (a b : ℝ) : ratioPower Q Qr a / ratioPower Q Qr b = ratioPower Q Qr (a - b)

noncomputable def NavierStokes.PhysicalParticularWave.chartChange (h Q Qr : ℝ) (gap : ℕ) : Lift →L[ℝ] Lift

A band-to-reference change, in the (Z,T) order used by PCC. The slow-coordinate swap is supplied by waveEquiv.

Equations

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

@[simp]

theorem NavierStokes.PhysicalParticularWave.chartChange_apply (h Q Qr : ℝ) (gap : ℕ) (x : Lift) : (chartChange h Q Qr gap) x = (ratioPower Q Qr (1 / 2) * x.1, (ratioPower Q Qr (CoordinateAlgebra.D h) * x.2.1.1, ratioPower Q Qr 1 * x.2.1.2), (CommonCoverSolve.coverPower gap) x.2.2)

noncomputable def NavierStokes.PhysicalParticularWave.cylinderChange (h Q Qr : ℝ) (gap : ℕ) : Cylinder →L[ℝ] Cylinder

Cylinder change, given by ((chartChange h Q Qr gap).comp (ContinuousLinearMap.fst ℝ Lift ℝ)).prod (ContinuousLinearMap.snd ℝ Lift ℝ).

Equations

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

@[simp]

theorem NavierStokes.PhysicalParticularWave.cylinderChange_apply (h Q Qr : ℝ) (gap : ℕ) (x : Cylinder) : (cylinderChange h Q Qr gap) x = ((chartChange h Q Qr gap) x.1, x.2)

theorem NavierStokes.PhysicalParticularWave.cylinderChange_graph {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (h : ℝ) (i gap : ℕ) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) : (cylinderChange h Q Qr gap) ((PhysicalResidualBridge.commonGraph Q h i).map z) = (PhysicalResidualBridge.commonGraph Qr h (i + gap)).map z

noncomputable def NavierStokes.PhysicalParticularWave.velocityWeight (h Q Qr : ℝ) : ℝ

Velocity weight, given by ratioPower Q Qr (CoordinateAlgebra.A h).

Equations

• NavierStokes.PhysicalParticularWave.velocityWeight h Q Qr = NavierStokes.PhysicalParticularWave.ratioPower Q Qr (NavierStokes.CoordinateAlgebra.A h)

noncomputable def NavierStokes.PhysicalParticularWave.clockWeight (h Q Qr : ℝ) : ℝ

Clock weight, given by ratioPower Q Qr (CoordinateAlgebra.A h + 1 / 2).

Equations

• NavierStokes.PhysicalParticularWave.clockWeight h Q Qr = NavierStokes.PhysicalParticularWave.ratioPower Q Qr (NavierStokes.CoordinateAlgebra.A h + 1 / 2)

noncomputable def NavierStokes.PhysicalParticularWave.sourceWeight (h Q Qr : ℝ) : ℝ

Source weight, given by ratioPower Q Qr (2 * CoordinateAlgebra.A h + 1 / 2).

Equations

• NavierStokes.PhysicalParticularWave.sourceWeight h Q Qr = NavierStokes.PhysicalParticularWave.ratioPower Q Qr (2 * NavierStokes.CoordinateAlgebra.A h + 1 / 2)

noncomputable def NavierStokes.PhysicalParticularWave.pressureWeight (h Q Qr : ℝ) : ℝ

Pressure weight, given by ratioPower Q Qr (2 * CoordinateAlgebra.A h).

Equations

• NavierStokes.PhysicalParticularWave.pressureWeight h Q Qr = NavierStokes.PhysicalParticularWave.ratioPower Q Qr (2 * NavierStokes.CoordinateAlgebra.A h)

noncomputable def NavierStokes.PhysicalParticularWave.normalWeight (Q Qr K Kr : ℝ) : ℝ

Normal weight, given by (Kr / K) * ratioPower Q Qr (1 / 2).

Equations

• NavierStokes.PhysicalParticularWave.normalWeight Q Qr K Kr = Kr / K * NavierStokes.PhysicalParticularWave.ratioPower Q Qr (1 / 2)

theorem NavierStokes.PhysicalParticularWave.clock_mul_velocity {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (h : ℝ) : clockWeight h Q Qr * velocityWeight h Q Qr = sourceWeight h Q Qr

theorem NavierStokes.PhysicalParticularWave.pressure_scaling {Q Qr K Kr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (hK : K ≠ 0) (hKr : Kr ≠ 0) (h : ℝ) : clockWeight h Q Qr * velocityWeight h Q Qr / normalWeight Q Qr K Kr * (Kr / K) = pressureWeight h Q Qr

Both clock scaling and normal scaling are needed for the physical pressure weight. Their frequency factors cancel exactly.

theorem NavierStokes.PhysicalParticularWave.linear_change_direction {X E F : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (C : E →L[ℝ] F) {f : X → E} {g : X → F} {x v : X} {a b : ℝ} {u : E} {w : F} (ha : a ≠ 0) (hf : DifferentiableAt ℝ f x) (he : (fun (y : X) => C (f y)) =ᶠ[nhds x] g) (hdf : (fderiv ℝ f x) v = a • u) (hdg : (fderiv ℝ g x) v = b • w) : C u = (b / a) • w

theorem NavierStokes.PhysicalParticularWave.cylinderChange_graph_germ {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (h : ℝ) (i gap : ℕ) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) : (fun (y : ProblemStatement.SpaceTime) => (cylinderChange h Q Qr gap) ((PhysicalResidualBridge.commonGraph Q h i).map y)) =ᶠ[nhds z] (PhysicalResidualBridge.commonGraph Qr h (i + gap)).map

theorem NavierStokes.PhysicalParticularWave.cylinderChange_radial_graph {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (h : ℝ) (i gap : ℕ) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) : have G := PhysicalResidualBridge.commonGraph Q h i; have H := PhysicalResidualBridge.commonGraph Qr h (i + gap); (cylinderChange h Q Qr gap) (G.radial (G.map z)) = ratioPower Q Qr (1 / 2) • H.radial (H.map z)

theorem NavierStokes.PhysicalParticularWave.cylinderChange_axial_graph {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (h : ℝ) (i gap : ℕ) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) : have G := PhysicalResidualBridge.commonGraph Q h i; have H := PhysicalResidualBridge.commonGraph Qr h (i + gap); (cylinderChange h Q Qr gap) (G.axial (G.map z)) = ratioPower Q Qr (1 / 2) • H.axial (H.map z)

theorem NavierStokes.PhysicalParticularWave.cylinderChange_temporal_graph {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (h : ℝ) (i gap : ℕ) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) : have G := PhysicalResidualBridge.commonGraph Q h i; have H := PhysicalResidualBridge.commonGraph Qr h (i + gap); (cylinderChange h Q Qr gap) (G.temporal (G.map z)) = clockWeight h Q Qr • H.temporal (H.map z)

theorem NavierStokes.PhysicalParticularWave.radial_sameRadius (G : PhysicalResidualBridge.ScaledGraph) {x y : Cylinder} (hxy : x.1.1 = y.1.1) : G.radial x = G.radial y

theorem NavierStokes.PhysicalParticularWave.cylinderChange_radial {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (h : ℝ) (i gap : ℕ) {x : Cylinder} (hx : 0 < x.1.1) : have G := PhysicalResidualBridge.commonGraph Q h i; have H := PhysicalResidualBridge.commonGraph Qr h (i + gap); (cylinderChange h Q Qr gap) (G.radial x) = ratioPower Q Qr (1 / 2) • H.radial ((cylinderChange h Q Qr gap) x)

theorem NavierStokes.PhysicalParticularWave.cylinderChange_axial {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (h : ℝ) (i gap : ℕ) (x : Cylinder) : have G := PhysicalResidualBridge.commonGraph Q h i; have H := PhysicalResidualBridge.commonGraph Qr h (i + gap); (cylinderChange h Q Qr gap) (G.axial x) = ratioPower Q Qr (1 / 2) • H.axial ((cylinderChange h Q Qr gap) x)

theorem NavierStokes.PhysicalParticularWave.cylinderChange_temporal {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (h : ℝ) (i gap : ℕ) (x : Cylinder) : have G := PhysicalResidualBridge.commonGraph Q h i; have H := PhysicalResidualBridge.commonGraph Qr h (i + gap); (cylinderChange h Q Qr gap) (G.temporal x) = clockWeight h Q Qr • H.temporal ((cylinderChange h Q Qr gap) x)

theorem NavierStokes.PhysicalParticularWave.cylinderChange_angular (h Q Qr : ℝ) (gap : ℕ) (x : Cylinder) : (cylinderChange h Q Qr gap) (PhysicalResidualBridge.ScaledGraph.angular x) = PhysicalResidualBridge.ScaledGraph.angular ((cylinderChange h Q Qr gap) x)

theorem NavierStokes.PhysicalParticularWave.phaseNormal_chartChange {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (h : ℝ) (i gap : ℕ) (K Kr : ℝ) {x : Cylinder} (hx : 0 < x.1.1) {Φ : Cylinder → ℝ} (hΦ : DifferentiableAt ℝ Φ ((cylinderChange h Q Qr gap) x)) : have G := PhysicalResidualBridge.commonGraph Q h i; have H := PhysicalResidualBridge.commonGraph Qr h (i + gap); HarmonicCalculus.phaseNormal PhysicalResidualBridge.ScaledGraph.radius G.radial PhysicalResidualBridge.ScaledGraph.angular G.axial (fun (y : PhysicalResidualBridge.Cylinder) => Kr / K * Φ ((cylinderChange h Q Qr gap) y)) x = normalWeight Q Qr K Kr • HarmonicCalculus.phaseNormal PhysicalResidualBridge.ScaledGraph.radius H.radial PhysicalResidualBridge.ScaledGraph.angular H.axial Φ ((cylinderChange h Q Qr gap) x)

The normal scale comes from the actual spatial chart differential and the raw carrier phase, independently of any solved velocity.

theorem NavierStokes.PhysicalParticularWave.phaseNormal_chartChange_of_phase {Q Qr K Kr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (hK : K ≠ 0) (h : ℝ) (i gap : ℕ) {x : Cylinder} (hx : 0 < x.1.1) {Φ Ψ : Cylinder → ℝ} (hΨ : DifferentiableAt ℝ Ψ ((cylinderChange h Q Qr gap) x)) (hphase : (fun (y : Cylinder) => K * Φ y) =ᶠ[nhds x] fun (y : Cylinder) => Kr * Ψ ((cylinderChange h Q Qr gap) y)) : have G := PhysicalResidualBridge.commonGraph Q h i; have H := PhysicalResidualBridge.commonGraph Qr h (i + gap); HarmonicCalculus.phaseNormal PhysicalResidualBridge.ScaledGraph.radius G.radial PhysicalResidualBridge.ScaledGraph.angular G.axial Φ x = normalWeight Q Qr K Kr • HarmonicCalculus.phaseNormal PhysicalResidualBridge.ScaledGraph.radius H.radial PhysicalResidualBridge.ScaledGraph.angular H.axial Ψ ((cylinderChange h Q Qr gap) x)

One potential built from the actual reference solve

noncomputable def NavierStokes.PhysicalParticularWave.referenceRaw (D : ParticularWaveAssembly.AssemblyData Parameter) (j : ℤ) : WaveSpace → HarmonicCalculus.ComplexVector

Reference raw, given by angleLift (referenceVelocity D.reference D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j).

Equations

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

noncomputable def NavierStokes.PhysicalParticularWave.referenceRawPressure (D : ParticularWaveAssembly.AssemblyData Parameter) (j : ℤ) : WaveSpace → ℂ

Reference raw pressure, given by angleLift (ParticularWaveAssembly.referencePressure D.reference D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j).

Equations

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

noncomputable def NavierStokes.PhysicalParticularWave.referenceFrequency (D : ParticularWaveAssembly.AssemblyData Parameter) (j : ℤ) : ℝ

Reference frequency, given by (j : ℝ) * D.carrierBlock.frequency D.reference.band.

Equations

• NavierStokes.PhysicalParticularWave.referenceFrequency D j = ↑j * D.carrierBlock.frequency D.reference.band

noncomputable def NavierStokes.PhysicalParticularWave.referencePhase (D : ParticularWaveAssembly.AssemblyData Parameter) (j : ℤ) : WaveSpace → ℝ

Reference phase, given by (actualCarrier D.background D.carrierBlock j).phase D.reference.band.

Equations

• NavierStokes.PhysicalParticularWave.referencePhase D j = (NavierStokes.ParticularWaveAssembly.actualCarrier D.background D.carrierBlock j).phase D.reference.band

noncomputable def NavierStokes.PhysicalParticularWave.physicalPhase (D : ParticularWaveAssembly.AssemblyData Parameter) (h Qr : ℝ) (I : ℕ) (j : ℤ) : ProblemStatement.SpaceTime → ℝ

Physical phase, defined pointwise by referencePhase D j (nativeMap h Qr I z).

Equations

• NavierStokes.PhysicalParticularWave.physicalPhase D h Qr I j z = NavierStokes.PhysicalParticularWave.referencePhase D j (NavierStokes.PhysicalParticularWave.nativeMap h Qr I z)

noncomputable def NavierStokes.PhysicalParticularWave.physicalRaw (D : ParticularWaveAssembly.AssemblyData Parameter) (h Qr : ℝ) (I : ℕ) (j : ℤ) : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector

Physical raw, defined pointwise by Qr ^ (-CoordinateAlgebra.A h) • referenceRaw D j (nativeMap h Qr I z).

Equations

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

noncomputable def NavierStokes.PhysicalParticularWave.referencePotential (D : ParticularWaveAssembly.AssemblyData Parameter) (h Qr : ℝ) (I : ℕ) (j : ℤ) : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector

The native cutoff is already inside the reference common solve. The potential is taken once, after that solve and before differentiation.

Equations

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

noncomputable def NavierStokes.PhysicalParticularWave.physicalPotential (D : ParticularWaveAssembly.AssemblyData Parameter) (h Qr : ℝ) (I : ℕ) (delta : ℝ) (j : ℤ) : ProblemStatement.VelocityField

Physical potential, given by PhysicalCurlCovariance.globalCartesianPotential delta (referencePotential D h Qr I j).

Equations

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

noncomputable def NavierStokes.PhysicalParticularWave.physicalVelocity (D : ParticularWaveAssembly.AssemblyData Parameter) (h Qr : ℝ) (I : ℕ) (delta : ℝ) (j : ℤ) : ProblemStatement.VelocityField

Physical velocity, given by SpatialCurl.spatialCurl (physicalPotential D h Qr I delta j).

Equations

• NavierStokes.PhysicalParticularWave.physicalVelocity D h Qr I delta j = NavierStokes.SpatialCurl.spatialCurl (NavierStokes.PhysicalParticularWave.physicalPotential D h Qr I delta j)

noncomputable def NavierStokes.PhysicalParticularWave.labelPotential (D : ParticularWaveAssembly.AssemblyData Parameter) (h Qr : ℝ) (I : ℕ) (delta : ℝ) (N : ℕ) : ProblemStatement.VelocityField

The finite harmonic sum for a single original spatial label is one actual Cartesian potential, rather than a collection of bandwise fields.

Equations

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

noncomputable def NavierStokes.PhysicalParticularWave.labelVelocity (D : ParticularWaveAssembly.AssemblyData Parameter) (h Qr : ℝ) (I : ℕ) (delta : ℝ) (N : ℕ) : ProblemStatement.VelocityField

Label velocity, given by SpatialCurl.spatialCurl (labelPotential D h Qr I delta N).

Equations

• NavierStokes.PhysicalParticularWave.labelVelocity D h Qr I delta N = NavierStokes.SpatialCurl.spatialCurl (NavierStokes.PhysicalParticularWave.labelPotential D h Qr I delta N)

theorem NavierStokes.PhysicalParticularWave.nativeMap_add_angle (h Q : ℝ) (i : ℕ) (z : ProblemStatement.SpaceTime) (s : ℝ) : nativeMap h Q i (z + s • (0, ProblemStatement.coordinateVector 1)) = nativeMap h Q i z + s • ((0, 1), 0)

theorem NavierStokes.PhysicalParticularWave.physicalPhase_affine (D : ParticularWaveAssembly.AssemblyData Parameter) (h Qr : ℝ) (I : ℕ) (j : ℤ) : CopyAngularInvariance.AffinePhase (0, ProblemStatement.coordinateVector 1) (↑(D.carrierBlock.angularFrequency D.reference.band) / D.carrierBlock.frequency D.reference.band) (physicalPhase D h Qr I j)

theorem NavierStokes.PhysicalParticularWave.physicalRaw_invariant (D : ParticularWaveAssembly.AssemblyData Parameter) (h Qr : ℝ) (I : ℕ) (j : ℤ) : CopyAngularInvariance.Invariant (0, ProblemStatement.coordinateVector 1) (physicalRaw D h Qr I j)

theorem NavierStokes.PhysicalParticularWave.angle_translate_pack (t r theta z s : ℝ) : (t, AxisymmetricResidual.pack r theta z) + s • (0, ProblemStatement.coordinateVector 1) = (t, AxisymmetricResidual.pack r (theta + s) z)

theorem NavierStokes.PhysicalParticularWave.referencePotential_periodic (D : ParticularWaveAssembly.AssemblyData Parameter) (h Qr : ℝ) (I : ℕ) (j : ℤ) (hk : D.carrierBlock.frequency D.reference.band ≠ 0) (t r z : ℝ) : Function.Periodic (fun (theta : ℝ) => referencePotential D h Qr I j (t, AxisymmetricResidual.pack r theta z)) (2 * Real.pi)

structure NavierStokes.PhysicalParticularWave.ReferenceIdentity (D : ParticularWaveAssembly.AssemblyData Parameter) : Prop

These are identities of the input chart at its own reference band.

• parameter : D.charts.parameter D.reference.band = id
• gap : D.charts.gap D.reference.band = 0
• amplitude : D.charts.amplitude D.reference.band = 1

theorem NavierStokes.PhysicalParticularWave.referenceRaw_eq_common (D : ParticularWaveAssembly.AssemblyData Parameter) (H : ReferenceIdentity D) (j : ℤ) : referenceRaw D j = (rawCommon D j).amplitude D.reference.band

structure NavierStokes.PhysicalParticularWave.ReferenceChart (D : ParticularWaveAssembly.AssemblyData Parameter) (h Qr : ℝ) (I : ℕ) : Prop

Literal input-operator matches at the reference chart. This record contains no condition on a solved velocity, pressure, potential or curl.

• identity : ReferenceIdentity D
• radius : (fun (x : Cylinder) => D.background.radius D.reference.band (↑waveEquiv x)) = PhysicalResidualBridge.ScaledGraph.radius
• radial : PhysicalCurlCovariance.reindexVector (↑waveEquiv) (D.directions.radialField D.reference.band) = (PhysicalResidualBridge.commonGraph Qr h I).radial
• angular : (PhysicalCurlCovariance.reindexVector ↑waveEquiv fun (x : WaveSpace) => D.directions.angular) = PhysicalResidualBridge.ScaledGraph.angular
• axial : PhysicalCurlCovariance.reindexVector (↑waveEquiv) (D.directions.axialField D.strip D.reference.band) = (PhysicalResidualBridge.commonGraph Qr h I).axial

noncomputable def NavierStokes.PhysicalParticularWave.referenceDomain (D : ParticularWaveAssembly.AssemblyData Parameter) : Set Cylinder

Reference domain, given by waveEquiv ⁻¹' D.strip.domain.

Equations

• NavierStokes.PhysicalParticularWave.referenceDomain D = ⇑NavierStokes.PhysicalParticularWave.waveEquiv ⁻¹' D.strip.domain

theorem NavierStokes.PhysicalParticularWave.referenceDomain_open (D : ParticularWaveAssembly.AssemblyData Parameter) : IsOpen (referenceDomain D)

noncomputable def NavierStokes.PhysicalParticularWave.liftPhase (D : ParticularWaveAssembly.AssemblyData Parameter) (j : ℤ) : Cylinder → ℝ

Lift phase, defined pointwise by referencePhase D j (waveEquiv x).

Equations

• NavierStokes.PhysicalParticularWave.liftPhase D j x = NavierStokes.PhysicalParticularWave.referencePhase D j (NavierStokes.PhysicalParticularWave.waveEquiv x)

noncomputable def NavierStokes.PhysicalParticularWave.liftRaw (D : ParticularWaveAssembly.AssemblyData Parameter) (j : ℤ) : Cylinder → HarmonicCalculus.ComplexVector

Lift raw, defined pointwise by referenceRaw D j (waveEquiv x).

Equations

• NavierStokes.PhysicalParticularWave.liftRaw D j x = NavierStokes.PhysicalParticularWave.referenceRaw D j (NavierStokes.PhysicalParticularWave.waveEquiv x)

theorem NavierStokes.PhysicalParticularWave.liftPhase_smooth (D : ParticularWaveAssembly.AssemblyData Parameter) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) : ContDiffOn ℝ (↑⊤) (liftPhase D j) (referenceDomain D)

theorem NavierStokes.PhysicalParticularWave.liftRaw_smooth (D : ParticularWaveAssembly.AssemblyData Parameter) {h Qr : ℝ} {I : ℕ} (H : ReferenceChart D h Qr I) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) : ContDiffOn ℝ (↑⊤) (liftRaw D j) (referenceDomain D)

theorem NavierStokes.PhysicalParticularWave.liftNormal_eq (D : ParticularWaveAssembly.AssemblyData Parameter) {h Qr : ℝ} {I : ℕ} (H : ReferenceChart D h Qr I) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) {x : Cylinder} (hx : x ∈ referenceDomain D) : HarmonicCalculus.phaseNormal PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph Qr h I).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph Qr h I).axial (liftPhase D j) x = (rawCommon D j).normal D.strip D.directions D.reference.band (waveEquiv x)

theorem NavierStokes.PhysicalParticularWave.liftNormal_ne (D : ParticularWaveAssembly.AssemblyData Parameter) {h Qr : ℝ} {I : ℕ} (H : ReferenceChart D h Qr I) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) {x : Cylinder} (hx : x ∈ referenceDomain D) : HarmonicCalculus.phaseNormal PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph Qr h I).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph Qr h I).axial (liftPhase D j) x ≠ 0

theorem NavierStokes.PhysicalParticularWave.liftRaw_tangent (D : ParticularWaveAssembly.AssemblyData Parameter) {h Qr : ℝ} {I : ℕ} (H : ReferenceChart D h Qr I) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) {x : Cylinder} (hx : x ∈ referenceDomain D) : HarmonicCalculus.normalDot (HarmonicCalculus.phaseNormal PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph Qr h I).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph Qr h I).axial (liftPhase D j) x) (liftRaw D j x) = 0

theorem NavierStokes.PhysicalParticularWave.reference_radius_ne (D : ParticularWaveAssembly.AssemblyData Parameter) {h Qr : ℝ} {I : ℕ} (H : ReferenceChart D h Qr I) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) {x : Cylinder} (hx : x ∈ referenceDomain D) : x.1.1 ≠ 0

theorem NavierStokes.PhysicalParticularWave.liftPotential_eq (D : ParticularWaveAssembly.AssemblyData Parameter) {h Qr : ℝ} {I : ℕ} (H : ReferenceChart D h Qr I) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) {x : Cylinder} (hx : x ∈ referenceDomain D) : CurlClassBounds.vectorPotential (referenceFrequency D j) PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph Qr h I).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph Qr h I).axial (liftPhase D j) (liftRaw D j) x = commonPotential D j D.reference.band (waveEquiv x)

theorem NavierStokes.PhysicalParticularWave.referencePotential_eq_common (D : ParticularWaveAssembly.AssemblyData Parameter) {h Qr : ℝ} {I : ℕ} (H : ReferenceChart D h Qr I) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) (hQr : 0 < Qr) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) (hx : nativeMap h Qr I z ∈ D.strip.domain) : referencePotential D h Qr I j z = Qr ^ (-h) • commonPotential D j D.reference.band (nativeMap h Qr I z)

theorem NavierStokes.PhysicalParticularWave.referencePotential_smoothAt (D : ParticularWaveAssembly.AssemblyData Parameter) {h Qr : ℝ} {I : ℕ} (H : ReferenceChart D h Qr I) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) (hQr : 0 < Qr) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) (hx : nativeMap h Qr I z ∈ D.strip.domain) : ContDiffAt ℝ (↑⊤) (referencePotential D h Qr I j) z

theorem NavierStokes.PhysicalParticularWave.reference_physical_velocity (D : ParticularWaveAssembly.AssemblyData Parameter) {h Qr : ℝ} {I : ℕ} (H : ReferenceChart D h Qr I) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) (hQr : 0 < Qr) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) (hx : nativeMap h Qr I z ∈ D.strip.domain) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) (component : Fin 3) : (HarmonicCalculus.vectorMode ((D.wave j).frequency D.reference.band) ((D.wave j).phase D.reference.band) ((D.wave j).amplitude D.reference.band) (nativeMap h Qr I z) component).re = Qr ^ CoordinateAlgebra.A h * ((CylindricalResidual.frame (-z.2.ofLp 1)) (physicalVelocity D h Qr I delta j (z.1, CylindricalResidual.chart z.2))).ofLp component

Actual solves with the rescaled native clock

noncomputable def NavierStokes.PhysicalParticularWave.parameterChange (h Q Qr : ℝ) (p : Parameter) : Parameter

Parameter change, given by (ratioPower Q Qr (1 / 2) * p.1, (ratioPower Q Qr 1 * p.2.1, ratioPower Q Qr (CoordinateAlgebra.D h) * p.2.2)).

Equations

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

theorem NavierStokes.PhysicalParticularWave.parameterChange_smooth (h Q Qr : ℝ) : ContDiff ℝ (↑⊤) (parameterChange h Q Qr)

theorem NavierStokes.PhysicalParticularWave.waveEquiv_cylinderChange (h Q Qr : ℝ) (gap : ℕ) (x : Cylinder) : waveEquiv ((cylinderChange h Q Qr gap) x) = ((parameterChange h Q Qr (waveEquiv x).1.1, (waveEquiv x).1.2), (CommonCoverSolve.coverPower gap) (waveEquiv x).2)

noncomputable def NavierStokes.PhysicalParticularWave.referenceSource (D : ParticularWaveAssembly.AssemblyData Parameter) (j : ℤ) : Parameter × TorusInverse.Plane → HarmonicCalculus.ComplexVector

Reference source, given by residualSource D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.reference.band.

Equations

• NavierStokes.PhysicalParticularWave.referenceSource D j = NavierStokes.ParticularWaveAssembly.residualSource D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.reference.band

noncomputable def NavierStokes.PhysicalParticularWave.bandAmplitude (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (gap : ℕ) (K : ℝ) (j : ℤ) : Parameter × TorusInverse.Plane → HarmonicCalculus.ComplexVector

Band amplitude, constructed using ParticularWaveBounds.commonVelocity.

Equations

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

noncomputable def NavierStokes.PhysicalParticularWave.bandPressure (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (gap : ℕ) (K : ℝ) (j : ℤ) : Parameter × TorusInverse.Plane → ℂ

Band pressure, constructed using ParticularWaveBounds.commonPressure.

Equations

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

structure NavierStokes.PhysicalParticularWave.ReferenceODE (D : ParticularWaveAssembly.AssemblyData Parameter) (j : ℤ) (U : Set Parameter) : Prop

Continuity of the actual primitive Volterra coefficients and source, and support inside the reference integration interval.

• coefficient : ContinuousOn (D.reference.tangent j).linearData.coefficient (U ×ˢ Set.univ)
• forcing : ContinuousOn (D.reference.tangent j).linearData.forcingMap (U ×ˢ Set.univ)
• source : ContinuousOn (referenceSource D j) (U ×ˢ Set.univ)
• cutoff : Function.support D.reference.cutoff ⊆ Set.univ ×ˢ Set.Icc 0 D.reference.length

theorem NavierStokes.PhysicalParticularWave.normalWeight_ne {Q Qr K Kr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (hK : K ≠ 0) (hKr : Kr ≠ 0) : normalWeight Q Qr K Kr ≠ 0

theorem NavierStokes.PhysicalParticularWave.bandAmplitude_eq_reference (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (gap : ℕ) {K : ℝ} (hK : K ≠ 0) (j : ℤ) (hKr : referenceFrequency D j ≠ 0) {U : Set Parameter} (R : ReferenceODE D j U) (p : Parameter) (hp : parameterChange h Q Qr p ∈ U) (Y : TorusInverse.Plane) : bandAmplitude D h hQ hQr gap K j (p, Y) = velocityWeight h Q Qr • ParticularWaveAssembly.referenceVelocity D.reference D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j (parameterChange h Q Qr p, (CommonCoverSolve.coverPower gap) Y)

theorem NavierStokes.PhysicalParticularWave.bandPressure_eq_reference (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (gap : ℕ) {K : ℝ} (hK : K ≠ 0) (j : ℤ) (hKr : referenceFrequency D j ≠ 0) {U : Set Parameter} (R : ReferenceODE D j U) (p : Parameter) (hp : parameterChange h Q Qr p ∈ U) (Y : TorusInverse.Plane) : bandPressure D h hQ hQr gap K j (p, Y) = pressureWeight h Q Qr • ParticularWaveAssembly.referencePressure D.reference D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j (parameterChange h Q Qr p, (CommonCoverSolve.coverPower gap) Y)

noncomputable def NavierStokes.PhysicalParticularWave.bandRaw (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (gap : ℕ) (K : ℝ) (j : ℤ) : Cylinder → HarmonicCalculus.ComplexVector

Band raw, defined pointwise by bandAmplitude D h hQ hQr gap K j ((waveEquiv x).1.1, (waveEquiv x).2).

Equations

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

noncomputable def NavierStokes.PhysicalParticularWave.bandRawPressure (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (gap : ℕ) (K : ℝ) (j : ℤ) : Cylinder → ℂ

Band raw pressure, defined pointwise by bandPressure D h hQ hQr gap K j ((waveEquiv x).1.1, (waveEquiv x).2).

Equations

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

noncomputable def NavierStokes.PhysicalParticularWave.bandPhase (D : ParticularWaveAssembly.AssemblyData Parameter) (h Q Qr : ℝ) (gap : ℕ) (K : ℝ) (j : ℤ) : Cylinder → ℝ

Band phase, defined pointwise by (referenceFrequency D j / K) * liftPhase D j (cylinderChange h Q Qr gap x).

Equations

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

noncomputable def NavierStokes.PhysicalParticularWave.bandVelocity (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (i gap : ℕ) (K : ℝ) (j : ℤ) : Cylinder → HarmonicCalculus.ComplexVector

Band velocity as an element of Cylinder → ComplexVector.

Equations

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

theorem NavierStokes.PhysicalParticularWave.bandRaw_eq_lift (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (gap : ℕ) {K : ℝ} (hK : K ≠ 0) (j : ℤ) (hKr : referenceFrequency D j ≠ 0) {U : Set Parameter} (R : ReferenceODE D j U) (x : Cylinder) (hx : parameterChange h Q Qr (waveEquiv x).1.1 ∈ U) : bandRaw D h hQ hQr gap K j x = velocityWeight h Q Qr • liftRaw D j ((cylinderChange h Q Qr gap) x)

noncomputable def NavierStokes.PhysicalParticularWave.bandDomain (D : ParticularWaveAssembly.AssemblyData Parameter) (h Q Qr : ℝ) (gap : ℕ) (U : Set Parameter) : Set Cylinder

Band domain, given by {x | 0 < x.1.1 ∧ cylinderChange h Q Qr gap x ∈ referenceDomain D ∧ parameterChange h Q Qr (waveEquiv x).1.1 ∈ U}.

Equations

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

theorem NavierStokes.PhysicalParticularWave.bandDomain_open (D : ParticularWaveAssembly.AssemblyData Parameter) (h Q Qr : ℝ) (gap : ℕ) {U : Set Parameter} (hU : IsOpen U) : IsOpen (bandDomain D h Q Qr gap U)

theorem NavierStokes.PhysicalParticularWave.normalDot_scaled (s c : ℝ) (n : ProblemStatement.Space) (a : HarmonicCalculus.ComplexVector) : HarmonicCalculus.normalDot (s • n) (c • a) = ↑s * ↑c * HarmonicCalculus.normalDot n a

theorem NavierStokes.PhysicalParticularWave.bandPhase_smooth (D : ParticularWaveAssembly.AssemblyData Parameter) {h Q Qr : ℝ} (gap : ℕ) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) {K : ℝ} {U : Set Parameter} : ContDiffOn ℝ (↑⊤) (bandPhase D h Q Qr gap K j) (bandDomain D h Q Qr gap U)

theorem NavierStokes.PhysicalParticularWave.bandRaw_smooth (D : ParticularWaveAssembly.AssemblyData Parameter) {h Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (i gap : ℕ) (H : ReferenceChart D h Qr (i + gap)) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) {K : ℝ} (hK : K ≠ 0) {U : Set Parameter} (R : ReferenceODE D j U) : ContDiffOn ℝ (↑⊤) (bandRaw D h hQ hQr gap K j) (bandDomain D h Q Qr gap U)

theorem NavierStokes.PhysicalParticularWave.bandNormal_ne (D : ParticularWaveAssembly.AssemblyData Parameter) {h Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (i gap : ℕ) (H : ReferenceChart D h Qr (i + gap)) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) {K : ℝ} (hK : K ≠ 0) {U : Set Parameter} {x : Cylinder} (hx : x ∈ bandDomain D h Q Qr gap U) : HarmonicCalculus.phaseNormal PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph Q h i).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph Q h i).axial (bandPhase D h Q Qr gap K j) x ≠ 0

theorem NavierStokes.PhysicalParticularWave.bandRaw_tangent (D : ParticularWaveAssembly.AssemblyData Parameter) {h Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (i gap : ℕ) (H : ReferenceChart D h Qr (i + gap)) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) {K : ℝ} (hK : K ≠ 0) {U : Set Parameter} (R : ReferenceODE D j U) {x : Cylinder} (hx : x ∈ bandDomain D h Q Qr gap U) : HarmonicCalculus.normalDot (HarmonicCalculus.phaseNormal PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph Q h i).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph Q h i).axial (bandPhase D h Q Qr gap K j) x) (bandRaw D h hQ hQr gap K j x) = 0

theorem NavierStokes.PhysicalParticularWave.band_physical_velocity (D : ParticularWaveAssembly.AssemblyData Parameter) {h Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (i gap : ℕ) (H : ReferenceChart D h Qr (i + gap)) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) {K : ℝ} (hK : K ≠ 0) {U : Set Parameter} (hU : IsOpen U) (R : ReferenceODE D j U) {z : ProblemStatement.SpaceTime} (hz : z ∈ (PhysicalResidualBridge.commonGraph Q h i).source (bandDomain D h Q Qr gap U)) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) (component : Fin 3) : (bandVelocity D h hQ hQr i gap K j ((PhysicalResidualBridge.commonGraph Q h i).map z) component).re = Q ^ CoordinateAlgebra.A h * ((CylindricalResidual.frame (-z.2.ofLp 1)) (physicalVelocity D h Qr (i + gap) delta j (z.1, CylindricalResidual.chart z.2))).ofLp component

Every actual transported solve is the view of the same Cartesian reference curl. The clock, source, cutoff and normal are transported before solving; no equality of solved velocities is a premise.

The pressure from the same reference solve

noncomputable def NavierStokes.PhysicalParticularWave.physicalPressureCoefficient (D : ParticularWaveAssembly.AssemblyData Parameter) (h Qr : ℝ) (I : ℕ) (j : ℤ) : ProblemStatement.SpaceTime → ℂ

Physical pressure coefficient, defined pointwise by (Qr ^ (-(2 * CoordinateAlgebra.A h)) : ℝ) • referenceRawPressure D j (nativeMap h Qr I z).

Equations

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

noncomputable def NavierStokes.PhysicalParticularWave.complexPhysicalPressure (D : ParticularWaveAssembly.AssemblyData Parameter) (h Qr : ℝ) (I : ℕ) (j : ℤ) : ProblemStatement.SpaceTime → ℂ

Complex physical pressure, given by mode (referenceFrequency D j) (physicalPhase D h Qr I j) (physicalPressureCoefficient D h Qr I j).

Equations

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

noncomputable def NavierStokes.PhysicalParticularWave.pressureVector (p : ProblemStatement.SpaceTime → ℂ) (z : ProblemStatement.SpaceTime) : HarmonicCalculus.ComplexVector

Pressure vector, given by ![0, 0, p z].

Equations

• NavierStokes.PhysicalParticularWave.pressureVector p z = ![0, 0, p z]

noncomputable def NavierStokes.PhysicalParticularWave.physicalPressure (D : ParticularWaveAssembly.AssemblyData Parameter) (h Qr : ℝ) (I : ℕ) (delta : ℝ) (j : ℤ) : ProblemStatement.PressureField

A scalar is the axial component of its Cartesian coordinate lift; the frame fixes this component, so the construction has no extra rotation.

Equations

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

noncomputable def NavierStokes.PhysicalParticularWave.bandPressureMode (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (gap : ℕ) (K : ℝ) (j : ℤ) : Cylinder → ℂ

Band pressure mode, given by mode K (bandPhase D h Q Qr gap K j) (bandRawPressure D h hQ hQr gap K j).

Equations

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

theorem NavierStokes.PhysicalParticularWave.mode_fullTurn {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {theta : E} {phi : E → ℝ} {a : E → ℂ} {K slope : ℝ} (m : ℤ) (hphi : CopyAngularInvariance.AffinePhase theta slope phi) (ha : CopyAngularInvariance.Invariant theta a) (hf : K * slope = ↑m) (x : E) : HarmonicCalculus.mode K phi a (x + (2 * Real.pi) • theta) = HarmonicCalculus.mode K phi a x

theorem NavierStokes.PhysicalParticularWave.complexPhysicalPressure_periodic (D : ParticularWaveAssembly.AssemblyData Parameter) (h Qr : ℝ) (I : ℕ) (j : ℤ) (hk : D.carrierBlock.frequency D.reference.band ≠ 0) (t r z : ℝ) : Function.Periodic (fun (theta : ℝ) => complexPhysicalPressure D h Qr I j (t, AxisymmetricResidual.pack r theta z)) (2 * Real.pi)

theorem NavierStokes.PhysicalParticularWave.physicalPressure_forward (D : ParticularWaveAssembly.AssemblyData Parameter) (h Qr : ℝ) (I : ℕ) (j : ℤ) (hk : D.carrierBlock.frequency D.reference.band ≠ 0) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) {z : ProblemStatement.SpaceTime} (hz : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) : physicalPressure D h Qr I delta j (z.1, CylindricalResidual.chart z.2) = (complexPhysicalPressure D h Qr I j z).re

theorem NavierStokes.PhysicalParticularWave.bandRawPressure_eq_lift (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (gap : ℕ) {K : ℝ} (hK : K ≠ 0) (j : ℤ) (hKr : referenceFrequency D j ≠ 0) {U : Set Parameter} (R : ReferenceODE D j U) (x : Cylinder) (hx : parameterChange h Q Qr (waveEquiv x).1.1 ∈ U) : bandRawPressure D h hQ hQr gap K j x = pressureWeight h Q Qr • referenceRawPressure D j (waveEquiv ((cylinderChange h Q Qr gap) x))

theorem NavierStokes.PhysicalParticularWave.bandPressureMode_eq_physical (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (i gap : ℕ) {K : ℝ} (hK : K ≠ 0) (j : ℤ) (hKr : referenceFrequency D j ≠ 0) {U : Set Parameter} (R : ReferenceODE D j U) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) (hp : parameterChange h Q Qr (nativeMap h Q i z).1.1 ∈ U) : bandPressureMode D h hQ hQr gap K j ((PhysicalResidualBridge.commonGraph Q h i).map z) = Q ^ (2 * CoordinateAlgebra.A h) • complexPhysicalPressure D h Qr (i + gap) j z

theorem NavierStokes.PhysicalParticularWave.band_physical_pressure (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (i gap : ℕ) {K : ℝ} (hK : K ≠ 0) (j : ℤ) (hKr : referenceFrequency D j ≠ 0) {U : Set Parameter} (R : ReferenceODE D j U) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) (hp : parameterChange h Q Qr (nativeMap h Q i z).1.1 ∈ U) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) : (bandPressureMode D h hQ hQr gap K j ((PhysicalResidualBridge.commonGraph Q h i).map z)).re = Q ^ (2 * CoordinateAlgebra.A h) * physicalPressure D h Qr (i + gap) delta j (z.1, CylindricalResidual.chart z.2)

Finite harmonic assembly uses one potential

noncomputable def NavierStokes.PhysicalParticularWave.labelBandVelocity (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (i gap : ℕ) (frequency : ℤ → ℝ) (N : ℕ) (x : Cylinder) (component : Fin 3) : ℝ

Label band velocity, given by ∑ j ∈ modes N, (bandVelocity D h hQ hQr i gap (frequency j) j x component).re.

Equations

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

noncomputable def NavierStokes.PhysicalParticularWave.labelBandPressure (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (gap : ℕ) (frequency : ℤ → ℝ) (N : ℕ) (x : Cylinder) : ℝ

Label band pressure, given by ∑ j ∈ modes N, (bandPressureMode D h hQ hQr gap (frequency j) j x).re.

Equations

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

noncomputable def NavierStokes.PhysicalParticularWave.labelPressure (D : ParticularWaveAssembly.AssemblyData Parameter) (h Qr : ℝ) (I : ℕ) (delta : ℝ) (N : ℕ) : ProblemStatement.PressureField

Label pressure, defined pointwise by ∑ j ∈ modes N, physicalPressure D h Qr I delta j z.

Equations

• NavierStokes.PhysicalParticularWave.labelPressure D h Qr I delta N z = ∑ j ∈ NavierStokes.ParticularWaveAssembly.modes N, NavierStokes.PhysicalParticularWave.physicalPressure D h Qr I delta j z

theorem NavierStokes.PhysicalParticularWave.spatialCurl_finset_sum {ι : Type} (S : Finset ι) (A : ι → ProblemStatement.VelocityField) {z : ProblemStatement.SpaceTime} (hA : ∀ i ∈ S, DifferentiableAt ℝ (A i) z) : SpatialCurl.spatialCurl (fun (w : ProblemStatement.SpaceTime) => ∑ i ∈ S, A i w) z = ∑ i ∈ S, SpatialCurl.spatialCurl (A i) z

theorem NavierStokes.PhysicalParticularWave.label_physical_velocity (D : ParticularWaveAssembly.AssemblyData Parameter) {h Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (i gap : ℕ) (H : ReferenceChart D h Qr (i + gap)) {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) (frequency : ℤ → ℝ) (hfrequency : ∀ j ∈ ParticularWaveAssembly.modes N, frequency j ≠ 0) {U : Set Parameter} (hU : IsOpen U) (R : ∀ j ∈ ParticularWaveAssembly.modes N, ReferenceODE D j U) {z : ProblemStatement.SpaceTime} (hz : z ∈ (PhysicalResidualBridge.commonGraph Q h i).source (bandDomain D h Q Qr gap U)) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) (component : Fin 3) : labelBandVelocity D h hQ hQr i gap frequency N ((PhysicalResidualBridge.commonGraph Q h i).map z) component = Q ^ CoordinateAlgebra.A h * ((CylindricalResidual.frame (-z.2.ofLp 1)) (labelVelocity D h Qr (i + gap) delta N (z.1, CylindricalResidual.chart z.2))).ofLp component

theorem NavierStokes.PhysicalParticularWave.label_physical_pressure (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (i gap : ℕ) {N : ℕ} (frequency : ℤ → ℝ) (hfrequency : ∀ j ∈ ParticularWaveAssembly.modes N, frequency j ≠ 0) (hreference : ∀ j ∈ ParticularWaveAssembly.modes N, referenceFrequency D j ≠ 0) {U : Set Parameter} (R : ∀ j ∈ ParticularWaveAssembly.modes N, ReferenceODE D j U) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) (hp : parameterChange h Q Qr (nativeMap h Q i z).1.1 ∈ U) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) : labelBandPressure D h hQ hQr gap frequency N ((PhysicalResidualBridge.commonGraph Q h i).map z) = Q ^ (2 * CoordinateAlgebra.A h) * labelPressure D h Qr (i + gap) delta N (z.1, CylindricalResidual.chart z.2)

Axis preservation follows from vanishing of the actual source

theorem NavierStokes.PhysicalParticularWave.referenceVelocity_zero_of_source (D : ParticularWaveAssembly.AssemblyData Parameter) (j : ℤ) (p : Parameter) (hf : ∀ (Y : TorusInverse.Plane), referenceSource D j (p, Y) = 0) (Y : TorusInverse.Plane) : ParticularWaveAssembly.referenceVelocity D.reference D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j (p, Y) = 0

theorem NavierStokes.PhysicalParticularWave.referencePotential_zero_of_source (D : ParticularWaveAssembly.AssemblyData Parameter) (h Qr : ℝ) (I : ℕ) (j : ℤ) (hQr : 0 < Qr) {delta : ℝ} (hf : ∀ (p : Parameter), p.1 ≤ Qr ^ (-(1 / 2)) * delta → ∀ (Y : TorusInverse.Plane), referenceSource D j (p, Y) = 0) (z : ProblemStatement.SpaceTime) (hz : z.2.ofLp 0 ≤ delta) : referencePotential D h Qr I j z = 0

theorem NavierStokes.PhysicalParticularWave.physicalVelocity_axis_zero_of_source (D : ParticularWaveAssembly.AssemblyData Parameter) (h Qr : ℝ) (I : ℕ) (j : ℤ) (hQr : 0 < Qr) {delta : ℝ} (hdelta : 0 < delta) (hf : ∀ (p : Parameter), p.1 ≤ Qr ^ (-(1 / 2)) * delta → ∀ (Y : TorusInverse.Plane), referenceSource D j (p, Y) = 0) (t : ℝ) (x : ProblemStatement.Space) (hx₀ : x.ofLp 0 = 0) (hx₁ : x.ofLp 1 = 0) : physicalVelocity D h Qr I delta j (t, x) = 0

theorem NavierStokes.PhysicalParticularWave.label_velocity_on_cover (D : ParticularWaveAssembly.AssemblyData Parameter) {h Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (i I : ℕ) (hi : i ≤ I) (H : ReferenceChart D h Qr I) {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) (frequency : ℤ → ℝ) (hfrequency : ∀ j ∈ ParticularWaveAssembly.modes N, frequency j ≠ 0) {U : Set Parameter} (hU : IsOpen U) (R : ∀ j ∈ ParticularWaveAssembly.modes N, ReferenceODE D j U) {z : ProblemStatement.SpaceTime} (hz : z ∈ (PhysicalResidualBridge.commonGraph Q h i).source (bandDomain D h Q Qr (I - i) U)) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) (component : Fin 3) : labelBandVelocity D h hQ hQr i (I - i) frequency N ((PhysicalResidualBridge.commonGraph Q h i).map z) component = Q ^ CoordinateAlgebra.A h * ((CylindricalResidual.frame (-z.2.ofLp 1)) (labelVelocity D h Qr I delta N (z.1, CylindricalResidual.chart z.2))).ofLp component

All allowed covering indices refer to one fixed reference cover. In particular i may be a native index or a common refinement.

theorem NavierStokes.PhysicalParticularWave.label_pressure_on_cover (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (i I : ℕ) (hi : i ≤ I) {N : ℕ} (frequency : ℤ → ℝ) (hfrequency : ∀ j ∈ ParticularWaveAssembly.modes N, frequency j ≠ 0) (hreference : ∀ j ∈ ParticularWaveAssembly.modes N, referenceFrequency D j ≠ 0) {U : Set Parameter} (R : ∀ j ∈ ParticularWaveAssembly.modes N, ReferenceODE D j U) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) (hp : parameterChange h Q Qr (nativeMap h Q i z).1.1 ∈ U) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) : labelBandPressure D h hQ hQr (I - i) frequency N ((PhysicalResidualBridge.commonGraph Q h i).map z) = Q ^ (2 * CoordinateAlgebra.A h) * labelPressure D h Qr I delta N (z.1, CylindricalResidual.chart z.2)

Regularity of the constructed physical fields

theorem NavierStokes.PhysicalParticularWave.referenceRawPressure_eq_common (D : ParticularWaveAssembly.AssemblyData Parameter) (H : ReferenceIdentity D) {j : ℤ} (hj : j ≠ 0) (hfrequency : ∀ (n : ℕ), D.carrierBlock.frequency n ≠ 0) : referenceRawPressure D j = (rawCommon D j).pressure D.reference.band

theorem NavierStokes.PhysicalParticularWave.physicalPotential_smoothAt (D : ParticularWaveAssembly.AssemblyData Parameter) {h Qr : ℝ} {I : ℕ} (H : ReferenceChart D h Qr I) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) (hQr : 0 < Qr) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) (hx : nativeMap h Qr I z ∈ D.strip.domain) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) : ContDiffAt ℝ (↑⊤) (physicalPotential D h Qr I delta j) (z.1, CylindricalResidual.chart z.2)

theorem NavierStokes.PhysicalParticularWave.physicalVelocity_smoothAt (D : ParticularWaveAssembly.AssemblyData Parameter) {h Qr : ℝ} {I : ℕ} (H : ReferenceChart D h Qr I) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) (hQr : 0 < Qr) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) (hx : nativeMap h Qr I z ∈ D.strip.domain) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) : ContDiffAt ℝ (↑⊤) (physicalVelocity D h Qr I delta j) (z.1, CylindricalResidual.chart z.2)

theorem NavierStokes.PhysicalParticularWave.complexPhysicalPressure_smoothAt (D : ParticularWaveAssembly.AssemblyData Parameter) {h Qr : ℝ} {I : ℕ} (H : ReferenceChart D h Qr I) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) (hQr : 0 < Qr) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) (hx : nativeMap h Qr I z ∈ D.strip.domain) : ContDiffAt ℝ (↑⊤) (complexPhysicalPressure D h Qr I j) z

theorem NavierStokes.PhysicalParticularWave.physicalPressure_smoothAt (D : ParticularWaveAssembly.AssemblyData Parameter) {h Qr : ℝ} {I : ℕ} (H : ReferenceChart D h Qr I) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) (hQr : 0 < Qr) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) (hx : nativeMap h Qr I z ∈ D.strip.domain) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) : ContDiffAt ℝ (↑⊤) (physicalPressure D h Qr I delta j) (z.1, CylindricalResidual.chart z.2)

theorem NavierStokes.PhysicalParticularWave.labelPotential_smoothAt (D : ParticularWaveAssembly.AssemblyData Parameter) {h Qr : ℝ} {I : ℕ} (H : ReferenceChart D h Qr I) {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) (hQr : 0 < Qr) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) (hx : nativeMap h Qr I z ∈ D.strip.domain) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) : ContDiffAt ℝ (↑⊤) (labelPotential D h Qr I delta N) (z.1, CylindricalResidual.chart z.2)

theorem NavierStokes.PhysicalParticularWave.labelVelocity_smoothAt (D : ParticularWaveAssembly.AssemblyData Parameter) {h Qr : ℝ} {I : ℕ} (H : ReferenceChart D h Qr I) {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) (hQr : 0 < Qr) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) (hx : nativeMap h Qr I z ∈ D.strip.domain) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) : ContDiffAt ℝ (↑⊤) (labelVelocity D h Qr I delta N) (z.1, CylindricalResidual.chart z.2)

theorem NavierStokes.PhysicalParticularWave.labelPressure_smoothAt (D : ParticularWaveAssembly.AssemblyData Parameter) {h Qr : ℝ} {I : ℕ} (H : ReferenceChart D h Qr I) {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) (hQr : 0 < Qr) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) (hx : nativeMap h Qr I z ∈ D.strip.domain) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) : ContDiffAt ℝ (↑⊤) (labelPressure D h Qr I delta N) (z.1, CylindricalResidual.chart z.2)

theorem NavierStokes.PhysicalParticularWave.labelVelocity_divergence (D : ParticularWaveAssembly.AssemblyData Parameter) {h Qr : ℝ} {I : ℕ} (H : ReferenceChart D h Qr I) {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) (hQr : 0 < Qr) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) (hx : nativeMap h Qr I z ∈ D.strip.domain) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) : ProblemStatement.spatialDivergence (labelVelocity D h Qr I delta N) z.1 (CylindricalResidual.chart z.2) = 0

Substitution of the actual target-band residual source

noncomputable def NavierStokes.PhysicalParticularWave.transportedResidualSource (D : ParticularWaveAssembly.AssemblyData Parameter) (h Q Qr : ℝ) (gap : ℕ) (j : ℤ) : Parameter × TorusInverse.Plane → HarmonicCalculus.ComplexVector

Transported residual source, constructed using ScaledTangentTransport.transportSource.

Equations

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

noncomputable def NavierStokes.PhysicalParticularWave.residualBandAmplitude (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (gap : ℕ) (K : ℝ) (j : ℤ) (n : ℕ) : Parameter × TorusInverse.Plane → HarmonicCalculus.ComplexVector

Residual band amplitude, constructed using ParticularWaveBounds.commonVelocity.

Equations

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

noncomputable def NavierStokes.PhysicalParticularWave.residualBandPressure (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (gap : ℕ) (K : ℝ) (j : ℤ) (n : ℕ) : Parameter × TorusInverse.Plane → ℂ

Residual band pressure, constructed using ParticularWaveBounds.commonPressure.

Equations

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

theorem NavierStokes.PhysicalParticularWave.residualBandAmplitude_eq (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (gap : ℕ) (K : ℝ) (j : ℤ) (n : ℕ) (hsource : ParticularWaveAssembly.residualSource D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j n = transportedResidualSource D h Q Qr gap j) : residualBandAmplitude D h hQ hQr gap K j n = bandAmplitude D h hQ hQr gap K j

theorem NavierStokes.PhysicalParticularWave.residualBandPressure_eq (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (gap : ℕ) (K : ℝ) (j : ℤ) (n : ℕ) (hsource : ParticularWaveAssembly.residualSource D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j n = transportedResidualSource D h Q Qr gap j) : residualBandPressure D h hQ hQr gap K j n = bandPressure D h hQ hQr gap K j

theorem NavierStokes.PhysicalParticularWave.transportedResidualSource_apply (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (gap : ℕ) (j : ℤ) (x : Parameter × TorusInverse.Plane) : transportedResidualSource D h Q Qr gap j x = sourceWeight h Q Qr • referenceSource D j (parameterChange h Q Qr x.1, (CommonCoverSolve.coverPower gap) x.2)

theorem NavierStokes.PhysicalParticularWave.bandPhase_eq_actualCarrier (D : ParticularWaveAssembly.AssemblyData Parameter) (h Q Qr : ℝ) (gap n : ℕ) (j : ℤ) (hj : j ≠ 0) (hfrequency : ∀ (m : ℕ), D.carrierBlock.frequency m ≠ 0) (hphase : ∀ (p : Parameter) (Y : TorusInverse.Plane), D.carrierBlock.frequency n * D.carrierBlock.phase n (p, Y) = D.carrierBlock.frequency D.reference.band * D.carrierBlock.phase D.reference.band (parameterChange h Q Qr p, (CommonCoverSolve.coverPower gap) Y)) (hangular : D.carrierBlock.angularFrequency n = D.carrierBlock.angularFrequency D.reference.band) : bandPhase D h Q Qr gap (↑j * D.carrierBlock.frequency n) j = fun (x : Cylinder) => (ParticularWaveAssembly.actualCarrier D.background D.carrierBlock j).phase n (waveEquiv x)

Equality with the target block's literal carrier follows from the primitive unmodulated phase identity and its shared integer angular label.