Normal and clock transport of the actual tangent inverse

The native clock, its zero-entry anchor, the normal and the source are transported together. Velocity and pressure below are outputs of the actual copy-path Volterra inverse, with no output compatibility hypothesis.

theorem NavierStokes.ScaledTangentTransport.coordinates_transport (g : CommonCoverSolve.Geometry) (gap : ℕ) (shift rate : ℝ) (hrate : rate ≠ 0) (copy : TorusInverse.Frequency) (Y : TorusInverse.Plane) : CopySolveCompatibility.nativeTimeMap shift rate ((CopySolveCompatibility.transportGeometry g gap shift rate hrate).coordinates copy Y) = g.coordinates copy ((CommonCoverSolve.coverPower gap) Y)

theorem NavierStokes.ScaledTangentTransport.path_transport (g : CommonCoverSolve.Geometry) (gap : ℕ) (shift rate : ℝ) (hrate : rate ≠ 0) (copy : TorusInverse.Frequency) (Y : TorusInverse.Plane) (t : ℝ) : (CommonCoverSolve.coverPower gap) ((CopySolveCompatibility.transportGeometry g gap shift rate hrate).path copy Y t) = g.path copy ((CommonCoverSolve.coverPower gap) Y) (shift + rate * t)

theorem NavierStokes.ScaledTangentTransport.slotDirection_transport (g : CommonCoverSolve.Geometry) (gap : ℕ) (shift rate : ℝ) (hrate : rate ≠ 0) : (CommonCoverSolve.coverPower gap) (ParticularWaveBounds.slotDirection (CopySolveCompatibility.transportGeometry g gap shift rate hrate)) = rate • ParticularWaveBounds.slotDirection g

theorem NavierStokes.ScaledTangentTransport.current_slot_iff (g : CommonCoverSolve.Geometry) (gap : ℕ) (shift rate : ℝ) (hrate : 0 < rate) (copy : TorusInverse.Frequency) (Y : TorusInverse.Plane) (a b : ℝ) : ((CopySolveCompatibility.transportGeometry g gap shift rate ⋯).coordinates copy Y).2 ∈ Set.Icc a b ↔ (g.coordinates copy ((CommonCoverSolve.coverPower gap) Y)).2 ∈ Set.Icc (shift + rate * a) (shift + rate * b)

theorem NavierStokes.ScaledTangentTransport.finite_transported_copy_cutoffs (g : CommonCoverSolve.Geometry) (gap : ℕ) (shift rate : ℝ) (hrate : rate ≠ 0) {cutoff : TorusInverse.Plane → ℝ} (hcutoff : HasCompactSupport cutoff) (R : ℝ) : ∃ (I : Finset TorusInverse.Frequency), ∀ (Y : TorusInverse.Plane), ‖Y‖ ≤ R → ∀ copy ∉ I, (cutoff ∘ CopySolveCompatibility.nativeTimeMap shift rate) ((CopySolveCompatibility.transportGeometry g gap shift rate hrate).coordinates copy Y) = 0

A compact reference cutoff still has only finitely many active transported copies, uniformly on each common-coordinate ball.

noncomputable def NavierStokes.ScaledTangentTransport.transportTangent {P Q H : Type} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (t : CommonCoverSolve.TangentData P H) (parameter : Q → P) (gap : ℕ) (shift rate amplitude normalScale : ℝ) : CommonCoverSolve.TangentData Q H

The velocity scale is amplitude. The actual source scale is rate * amplitude, and the moving normal acquires both normal and clock scales in its slot derivative.

Equations

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

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

The ambient complex source undergoes the same rate and velocity scalings as the real tangent source.

Equations

• NavierStokes.ScaledTangentTransport.transportSource f parameter gap rate amplitude z = (rate * amplitude) • f (parameter z.1, (NavierStokes.CommonCoverSolve.coverPower gap) z.2)

theorem NavierStokes.ScaledTangentTransport.normal_slot_derivative {P Q H : Type} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (t : CommonCoverSolve.TangentData P H) (parameter : Q → P) (gap : ℕ) (shift rate amplitude normalScale : ℝ) (q : Q) (xi eta : ℝ) (hn : HasDerivAt (fun (s : ℝ) => t.normal (parameter q, xi, s)) (t.normalDot (parameter q, xi, shift + rate * eta)) (shift + rate * eta)) : HasDerivAt (fun (s : ℝ) => (transportTangent t parameter gap shift rate amplitude normalScale).normal (q, xi, s)) ((transportTangent t parameter gap shift rate amplitude normalScale).normalDot (q, xi, eta)) eta

theorem NavierStokes.ScaledTangentTransport.copySolve_of_compatibleInputs {P Q V H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup H] [NormedSpace ℝ H] [CompleteSpace H] (d : CommonCoverSolve.LinearData P V H) (e : CommonCoverSolve.LinearData Q V H) (parameter : Q → P) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (gap : ℕ) (shift rate amplitude : ℝ) (hrate : 0 < rate) {U : Set P} (hA : ContinuousOn d.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn d.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn d.source (U ×ˢ Set.univ)) (q : Q) (hq : parameter q ∈ U) (hi : CopySolveCompatibility.SameInputsAt e (CopySolveCompatibility.transportData d parameter gap shift rate amplitude) q) (copy : TorusInverse.Frequency) (Y : TorusInverse.Plane) (hslot : ((CopySolveCompatibility.transportGeometry g gap shift rate ⋯).coordinates copy Y).2 ∈ Set.Icc a b) : e.copySolve (CopySolveCompatibility.transportGeometry g gap shift rate ⋯) hab copy (q, Y) = amplitude • d.copySolve g ⋯ copy (parameter q, (CommonCoverSolve.coverPower gap) Y)

Copy-level counterpart of CopySolveCompatibility.commonSolve_of_compatibleInputs. The condition compares only native coefficients and converted sources.

theorem NavierStokes.ScaledTangentTransport.transportTangent_sameInputs {P Q H : Type} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (t : CommonCoverSolve.TangentData P H) (parameter : Q → P) (gap : ℕ) (shift rate amplitude normalScale : ℝ) (hnormal : normalScale ≠ 0) (q : Q) : CopySolveCompatibility.SameInputsAt (transportTangent t parameter gap shift rate amplitude normalScale).linearData (CopySolveCompatibility.transportData t.linearData parameter gap shift rate amplitude) q

Normal scaling changes neither tangent projection nor the resulting ODE. Moving the clock factor from the forcing map into the source preserves its actual converted forcing.

theorem NavierStokes.ScaledTangentTransport.copySolve_transport {P Q H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (t : CommonCoverSolve.TangentData P H) (parameter : Q → P) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (gap : ℕ) (shift rate amplitude normalScale : ℝ) (hrate : 0 < rate) (hnormal : normalScale ≠ 0) {U : Set P} (hA : ContinuousOn t.linearData.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn t.linearData.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn t.source (U ×ˢ Set.univ)) (q : Q) (hq : parameter q ∈ U) (copy : TorusInverse.Frequency) (Y : TorusInverse.Plane) (hslot : ((CopySolveCompatibility.transportGeometry g gap shift rate ⋯).coordinates copy Y).2 ∈ Set.Icc a b) : (transportTangent t parameter gap shift rate amplitude normalScale).linearData.copySolve (CopySolveCompatibility.transportGeometry g gap shift rate ⋯) hab copy (q, Y) = amplitude • t.linearData.copySolve g ⋯ copy (parameter q, (CommonCoverSolve.coverPower gap) Y)

theorem NavierStokes.ScaledTangentTransport.commonSolve_transport {P Q H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (t : CommonCoverSolve.TangentData P H) (parameter : Q → P) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (gap : ℕ) (shift rate amplitude normalScale : ℝ) (hrate : 0 < rate) (hnormal : normalScale ≠ 0) {U : Set P} (hA : ContinuousOn t.linearData.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn t.linearData.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn t.source (U ×ˢ Set.univ)) (cutoff : TorusInverse.Plane → ℝ) (hcutoff : Function.support cutoff ⊆ Set.univ ×ˢ Set.Icc (shift + rate * a) (shift + rate * b)) (q : Q) (hq : parameter q ∈ U) (Y : TorusInverse.Plane) : (transportTangent t parameter gap shift rate amplitude normalScale).linearData.commonSolve (CopySolveCompatibility.transportGeometry g gap shift rate ⋯) hab (cutoff ∘ CopySolveCompatibility.nativeTimeMap shift rate) (q, Y) = amplitude • t.linearData.commonSolve g ⋯ cutoff (parameter q, (CommonCoverSolve.coverPower gap) Y)

The common output uses the transported cutoff, so the clock identity is needed only at points inside the reference integration interval.

theorem NavierStokes.ScaledTangentTransport.copyPressureReal_transport {P Q H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (t : CommonCoverSolve.TangentData P H) (parameter : Q → P) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (gap : ℕ) (shift rate amplitude normalScale : ℝ) (hrate : 0 < rate) (hnormal : normalScale ≠ 0) {U : Set P} (hA : ContinuousOn t.linearData.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn t.linearData.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn t.source (U ×ˢ Set.univ)) (q : Q) (hq : parameter q ∈ U) (copy : TorusInverse.Frequency) (Y : TorusInverse.Plane) (hslot : ((CopySolveCompatibility.transportGeometry g gap shift rate ⋯).coordinates copy Y).2 ∈ Set.Icc a b) : ParticularWaveBounds.copyPressureReal (transportTangent t parameter gap shift rate amplitude normalScale) (CopySolveCompatibility.transportGeometry g gap shift rate ⋯) hab copy (q, Y) = rate * amplitude / normalScale * ParticularWaveBounds.copyPressureReal t g ⋯ copy (parameter q, (CommonCoverSolve.coverPower gap) Y)

theorem NavierStokes.ScaledTangentTransport.copyPressure_transport {P Q H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (t : CommonCoverSolve.TangentData P H) (parameter : Q → P) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (gap : ℕ) (shift rate amplitude normalScale referenceFrequency frequency : ℝ) (hrate : 0 < rate) (hnormal : normalScale ≠ 0) (hreference : referenceFrequency ≠ 0) (hfrequency : frequency ≠ 0) {U : Set P} (hA : ContinuousOn t.linearData.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn t.linearData.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn t.source (U ×ˢ Set.univ)) (q : Q) (hq : parameter q ∈ U) (copy : TorusInverse.Frequency) (Y : TorusInverse.Plane) (hslot : ((CopySolveCompatibility.transportGeometry g gap shift rate ⋯).coordinates copy Y).2 ∈ Set.Icc a b) : ParticularWaveBounds.copyPressure (transportTangent t parameter gap shift rate amplitude normalScale) (CopySolveCompatibility.transportGeometry g gap shift rate ⋯) hab copy frequency (q, Y) = (rate * amplitude / normalScale * (referenceFrequency / frequency)) • ParticularWaveBounds.copyPressure t g ⋯ copy referenceFrequency (parameter q, (CommonCoverSolve.coverPower gap) Y)

Pressure includes the inverse frequency of the band in which it is realized, in addition to the derived clock/normal factor.

theorem NavierStokes.ScaledTangentTransport.transported_periodization_finite {Q E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : CommonCoverSolve.Geometry) (gap : ℕ) (shift rate : ℝ) (hrate : rate ≠ 0) {cutoff : TorusInverse.Plane → ℝ} (hcutoff : HasCompactSupport cutoff) (F : TorusInverse.Frequency → Q × TorusInverse.Plane → E) (q : Q) (Y : TorusInverse.Plane) : ∃ (I : Finset TorusInverse.Frequency), ParticularWaveBounds.periodizedCopies (CopySolveCompatibility.transportGeometry g gap shift rate hrate) (cutoff ∘ CopySolveCompatibility.nativeTimeMap shift rate) F (q, Y) = ∑ copy ∈ I, (cutoff ∘ CopySolveCompatibility.nativeTimeMap shift rate) ((CopySolveCompatibility.transportGeometry g gap shift rate hrate).coordinates copy Y) • F copy (q, Y)

The actual transported series is finite when the reference cutoff is compact; the transport identities do not rely on a divergent-series value.

theorem NavierStokes.ScaledTangentTransport.periodizedCopies_transport_of_active {P Q E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : CommonCoverSolve.Geometry) (parameter : Q → P) {a b : ℝ} (gap : ℕ) (shift rate scale : ℝ) (hrate : 0 < rate) (cutoff : TorusInverse.Plane → ℝ) (hcutoff : Function.support cutoff ⊆ Set.univ ×ˢ Set.Icc (shift + rate * a) (shift + rate * b)) (F : TorusInverse.Frequency → Q × TorusInverse.Plane → E) (G : TorusInverse.Frequency → P × TorusInverse.Plane → E) (q : Q) (Y : TorusInverse.Plane) (hcopy : ∀ (copy : TorusInverse.Frequency), ((CopySolveCompatibility.transportGeometry g gap shift rate ⋯).coordinates copy Y).2 ∈ Set.Icc a b → F copy (q, Y) = scale • G copy (parameter q, (CommonCoverSolve.coverPower gap) Y)) : ParticularWaveBounds.periodizedCopies (CopySolveCompatibility.transportGeometry g gap shift rate ⋯) (cutoff ∘ CopySolveCompatibility.nativeTimeMap shift rate) F (q, Y) = scale • ParticularWaveBounds.periodizedCopies g cutoff G (parameter q, (CommonCoverSolve.coverPower gap) Y)

A transported periodization only uses copy identities on the active native interval. In particular no equality of extended solves outside that interval is required.

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

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

theorem NavierStokes.ScaledTangentTransport.copyVelocity_transport {P Q : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (parameter : Q → P) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (gap : ℕ) (shift rate amplitude normalScale : ℝ) (hrate : 0 < rate) (hnormal : normalScale ≠ 0) {U : Set P} (hA : ContinuousOn t.linearData.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn t.linearData.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn t.source (U ×ˢ Set.univ)) (q : Q) (hq : parameter q ∈ U) (copy : TorusInverse.Frequency) (Y : TorusInverse.Plane) (hslot : ((CopySolveCompatibility.transportGeometry g gap shift rate ⋯).coordinates copy Y).2 ∈ Set.Icc a b) : ParticularWaveBounds.copyVelocity (transportTangent t parameter gap shift rate amplitude normalScale) (CopySolveCompatibility.transportGeometry g gap shift rate ⋯) hab copy (q, Y) = amplitude • ParticularWaveBounds.copyVelocity t g ⋯ copy (parameter q, (CommonCoverSolve.coverPower gap) Y)

theorem NavierStokes.ScaledTangentTransport.complexCopyVelocity_transport {P Q : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (parameter : Q → P) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (gap : ℕ) (shift rate amplitude normalScale : ℝ) (hrate : 0 < rate) (hnormal : normalScale ≠ 0) {U : Set P} (hA : ContinuousOn t.linearData.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn t.linearData.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn f (U ×ˢ Set.univ)) (q : Q) (hq : parameter q ∈ U) (copy : TorusInverse.Frequency) (Y : TorusInverse.Plane) (hslot : ((CopySolveCompatibility.transportGeometry g gap shift rate ⋯).coordinates copy Y).2 ∈ Set.Icc a b) : ParticularWaveBounds.complexCopyVelocity (transportTangent t parameter gap shift rate amplitude normalScale) (transportSource f parameter gap rate amplitude) (CopySolveCompatibility.transportGeometry g gap shift rate ⋯) hab copy (q, Y) = amplitude • ParticularWaveBounds.complexCopyVelocity t f g ⋯ copy (parameter q, (CommonCoverSolve.coverPower gap) Y)

theorem NavierStokes.ScaledTangentTransport.complexCopyPressure_transport {P Q : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (parameter : Q → P) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (gap : ℕ) (shift rate amplitude normalScale referenceFrequency frequency : ℝ) (hrate : 0 < rate) (hnormal : normalScale ≠ 0) (hreference : referenceFrequency ≠ 0) (hfrequency : frequency ≠ 0) {U : Set P} (hA : ContinuousOn t.linearData.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn t.linearData.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn f (U ×ˢ Set.univ)) (q : Q) (hq : parameter q ∈ U) (copy : TorusInverse.Frequency) (Y : TorusInverse.Plane) (hslot : ((CopySolveCompatibility.transportGeometry g gap shift rate ⋯).coordinates copy Y).2 ∈ Set.Icc a b) : ParticularWaveBounds.complexCopyPressure (transportTangent t parameter gap shift rate amplitude normalScale) (transportSource f parameter gap rate amplitude) (CopySolveCompatibility.transportGeometry g gap shift rate ⋯) hab copy frequency (q, Y) = (rate * amplitude / normalScale * (referenceFrequency / frequency)) • ParticularWaveBounds.complexCopyPressure t f g ⋯ copy referenceFrequency (parameter q, (CommonCoverSolve.coverPower gap) Y)

theorem NavierStokes.ScaledTangentTransport.commonVelocity_transport {P Q : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (parameter : Q → P) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (gap : ℕ) (shift rate amplitude normalScale : ℝ) (hrate : 0 < rate) (hnormal : normalScale ≠ 0) {U : Set P} (hA : ContinuousOn t.linearData.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn t.linearData.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn f (U ×ˢ Set.univ)) (cutoff : TorusInverse.Plane → ℝ) (hcutoff : Function.support cutoff ⊆ Set.univ ×ˢ Set.Icc (shift + rate * a) (shift + rate * b)) (q : Q) (hq : parameter q ∈ U) (Y : TorusInverse.Plane) : ParticularWaveBounds.commonVelocity (transportTangent t parameter gap shift rate amplitude normalScale) (transportSource f parameter gap rate amplitude) (CopySolveCompatibility.transportGeometry g gap shift rate ⋯) hab (cutoff ∘ CopySolveCompatibility.nativeTimeMap shift rate) (q, Y) = amplitude • ParticularWaveBounds.commonVelocity t f g ⋯ cutoff (parameter q, (CommonCoverSolve.coverPower gap) Y)

One actual reference velocity supplies every transported band view.

theorem NavierStokes.ScaledTangentTransport.commonPressure_transport {P Q : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (parameter : Q → P) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (gap : ℕ) (shift rate amplitude normalScale referenceFrequency frequency : ℝ) (hrate : 0 < rate) (hnormal : normalScale ≠ 0) (hreference : referenceFrequency ≠ 0) (hfrequency : frequency ≠ 0) {U : Set P} (hA : ContinuousOn t.linearData.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn t.linearData.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn f (U ×ˢ Set.univ)) (cutoff : TorusInverse.Plane → ℝ) (hcutoff : Function.support cutoff ⊆ Set.univ ×ˢ Set.Icc (shift + rate * a) (shift + rate * b)) (q : Q) (hq : parameter q ∈ U) (Y : TorusInverse.Plane) : ParticularWaveBounds.commonPressure (transportTangent t parameter gap shift rate amplitude normalScale) (transportSource f parameter gap rate amplitude) (CopySolveCompatibility.transportGeometry g gap shift rate ⋯) hab (cutoff ∘ CopySolveCompatibility.nativeTimeMap shift rate) frequency (q, Y) = (rate * amplitude / normalScale * (referenceFrequency / frequency)) • ParticularWaveBounds.commonPressure t f g ⋯ cutoff referenceFrequency (parameter q, (CommonCoverSolve.coverPower gap) Y)

The actual common pressure has the derived clock, normal and carrier frequency factors. It is not assigned the velocity's scaling weight.

theorem NavierStokes.ScaledTangentTransport.commonVelocity_zeroEntry {P Q : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (parameter : Q → P) (g : CommonCoverSolve.Geometry) (gap : ℕ) (L rate amplitude normalScale : ℝ) (hL : 0 < L) (hrate : 0 < rate) (hnormal : normalScale ≠ 0) {U : Set P} (hA : ContinuousOn t.linearData.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn t.linearData.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn f (U ×ˢ Set.univ)) (cutoff : TorusInverse.Plane → ℝ) (hcutoff : Function.support cutoff ⊆ Set.univ ×ˢ Set.Icc 0 L) (q : Q) (hq : parameter q ∈ U) (Y : TorusInverse.Plane) : ParticularWaveBounds.commonVelocity (transportTangent t parameter gap 0 rate amplitude normalScale) (transportSource f parameter gap rate amplitude) (CopySolveCompatibility.transportGeometry g gap 0 rate ⋯) ⋯ (cutoff ∘ CopySolveCompatibility.nativeTimeMap 0 rate) (q, Y) = amplitude • ParticularWaveBounds.commonVelocity t f g ⋯ cutoff (parameter q, (CommonCoverSolve.coverPower gap) Y)

A reference interval [0,L] corresponds to the band interval [0,L/rate]. Keeping the same numerical length would change the anchor problem; this specialization retains the actual common reference solve.

theorem NavierStokes.ScaledTangentTransport.commonPressure_zeroEntry {P Q : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (parameter : Q → P) (g : CommonCoverSolve.Geometry) (gap : ℕ) (L rate amplitude normalScale referenceFrequency frequency : ℝ) (hL : 0 < L) (hrate : 0 < rate) (hnormal : normalScale ≠ 0) (hreference : referenceFrequency ≠ 0) (hfrequency : frequency ≠ 0) {U : Set P} (hA : ContinuousOn t.linearData.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn t.linearData.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn f (U ×ˢ Set.univ)) (cutoff : TorusInverse.Plane → ℝ) (hcutoff : Function.support cutoff ⊆ Set.univ ×ˢ Set.Icc 0 L) (q : Q) (hq : parameter q ∈ U) (Y : TorusInverse.Plane) : ParticularWaveBounds.commonPressure (transportTangent t parameter gap 0 rate amplitude normalScale) (transportSource f parameter gap rate amplitude) (CopySolveCompatibility.transportGeometry g gap 0 rate ⋯) ⋯ (cutoff ∘ CopySolveCompatibility.nativeTimeMap 0 rate) frequency (q, Y) = (rate * amplitude / normalScale * (referenceFrequency / frequency)) • ParticularWaveBounds.commonPressure t f g ⋯ cutoff referenceFrequency (parameter q, (CommonCoverSolve.coverPower gap) Y)