Coherence of the actual particular increment #
The source is the residual of the current state. Its reference value is rebased to the native cover before solving. The identities below retain the full auxiliary fibers and the differentiated copy cutoffs.
Copy transport from continuity on the anchored interval #
The actual Volterra constructor depends only on the coefficient and converted forcing paths on its finite interval. These lemmas require continuity of exactly those paths, including their endpoints. No continuation of the raw tangent data or source outside the interval is assumed.
theorem
NavierStokes.IntervalCopyTransport.anchoredSolve_hasDerivAt
{P V E : Type}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{a b : ℝ}
(d : CommonCoverSolve.LinearData P V E)
(g : CommonCoverSolve.Geometry)
(hab : a ≤ b)
(copy : TorusInverse.Frequency)
(p : P)
(Y : TorusInverse.Plane)
(hA : Continuous fun (s : ↑(Set.Icc a b)) => d.coefficientAlong g copy ((p, Y), ↑s))
(hf : Continuous fun (s : ↑(Set.Icc a b)) => d.forcingAlong g copy ((p, Y), ↑s))
(s : ↑(Set.Icc a b))
:
HasDerivAt (d.anchoredSolve g hab copy (p, Y))
((d.coefficientAlong g copy ((p, Y), ↑s)) (d.anchoredSolve g hab copy (p, Y) ↑s) + d.forcingAlong g copy ((p, Y), ↑s))
↑s
The derivative of the existing constructor needs only its two continuous input paths on the actual integration interval.
theorem
NavierStokes.IntervalCopyTransport.anchoredSolve_unique
{P V E : Type}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{a b : ℝ}
(d : CommonCoverSolve.LinearData P V E)
(g : CommonCoverSolve.Geometry)
(hab : a ≤ b)
(copy : TorusInverse.Frequency)
(p : P)
(Y : TorusInverse.Plane)
(hA : Continuous fun (s : ↑(Set.Icc a b)) => d.coefficientAlong g copy ((p, Y), ↑s))
(hf : Continuous fun (s : ↑(Set.Icc a b)) => d.forcingAlong g copy ((p, Y), ↑s))
{u : ℝ → E}
(hu0 : u a = 0)
(hu :
∀ s ∈ Set.Icc a b, HasDerivAt u ((d.coefficientAlong g copy ((p, Y), s)) (u s) + d.forcingAlong g copy ((p, Y), s)) s)
:
Uniqueness compares actual solutions on the finite interval.
theorem
NavierStokes.IntervalCopyTransport.anchoredSolve_timeData
{P V E : Type}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{a b : ℝ}
(d : CommonCoverSolve.LinearData P V E)
(g : CommonCoverSolve.Geometry)
(shift rate : ℝ)
(hrate : 0 < rate)
(hab : a ≤ b)
(copy : TorusInverse.Frequency)
(p : P)
(Y : TorusInverse.Plane)
(hA : Continuous fun (s : ↑(Set.Icc (shift + rate * a) (shift + rate * b))) => d.coefficientAlong g copy ((p, Y), ↑s))
(hf : Continuous fun (s : ↑(Set.Icc (shift + rate * a) (shift + rate * b))) => d.forcingAlong g copy ((p, Y), ↑s))
{s : ℝ}
(hs : s ∈ Set.Icc a b)
:
(CopySolveCompatibility.timeData d shift rate).anchoredSolve (CopySolveCompatibility.timeGeometry g shift rate ⋯) hab
copy (p, Y) s = d.anchoredSolve g ⋯ copy (p, Y) (shift + rate * s)
Affine clock transport of the anchored solve, with finite-path hypotheses on the reference interval alone.
theorem
NavierStokes.IntervalCopyTransport.copySolve_timeData
{P V E : Type}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{a b : ℝ}
(d : CommonCoverSolve.LinearData P V E)
(g : CommonCoverSolve.Geometry)
(shift rate : ℝ)
(hrate : 0 < rate)
(hab : a ≤ b)
(copy : TorusInverse.Frequency)
(p : P)
(Y : TorusInverse.Plane)
(hA : Continuous fun (s : ↑(Set.Icc (shift + rate * a) (shift + rate * b))) => d.coefficientAlong g copy ((p, Y), ↑s))
(hf : Continuous fun (s : ↑(Set.Icc (shift + rate * a) (shift + rate * b))) => d.forcingAlong g copy ((p, Y), ↑s))
(hs : ((CopySolveCompatibility.timeGeometry g shift rate ⋯).coordinates copy Y).2 ∈ Set.Icc a b)
:
theorem
NavierStokes.IntervalCopyTransport.copySolve_of_compatibleInputs
{P Q V E : Type}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{a b : ℝ}
(d : CommonCoverSolve.LinearData P V E)
(e : CommonCoverSolve.LinearData Q V E)
(parameter : Q → P)
(g : CommonCoverSolve.Geometry)
(hab : a ≤ b)
(gap : ℕ)
(shift rate amplitude : ℝ)
(hrate : 0 < rate)
(q : Q)
(copy : TorusInverse.Frequency)
(Y : TorusInverse.Plane)
(hA :
Continuous fun (s : ↑(Set.Icc (shift + rate * a) (shift + rate * b))) =>
d.coefficientAlong g copy ((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hf :
Continuous fun (s : ↑(Set.Icc (shift + rate * a) (shift + rate * b))) =>
d.forcingAlong g copy ((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hi :
CopySolveCompatibility.SameInputsAt e (CopySolveCompatibility.transportData d parameter gap shift rate amplitude) q)
(hslot : ((CopySolveCompatibility.transportGeometry g gap shift rate ⋯).coordinates copy Y).2 ∈ Set.Icc a b)
:
Parameter/cover/source transport and exact equality of converted inputs are algebraic. Only clock transport uses the two finite-path hypotheses.
theorem
NavierStokes.IntervalCopyTransport.copySolve_transport
{P Q H : Type}
[NormedAddCommGroup H]
[InnerProductSpace ℝ H]
[CompleteSpace H]
{a b : ℝ}
(t : CommonCoverSolve.TangentData P H)
(parameter : Q → P)
(g : CommonCoverSolve.Geometry)
(hab : a ≤ b)
(gap : ℕ)
(shift rate amplitude normalScale : ℝ)
(hrate : 0 < rate)
(hnormal : normalScale ≠ 0)
(q : Q)
(copy : TorusInverse.Frequency)
(Y : TorusInverse.Plane)
(hA :
Continuous fun (s : ↑(Set.Icc (shift + rate * a) (shift + rate * b))) =>
t.linearData.coefficientAlong g copy ((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hf :
Continuous fun (s : ↑(Set.Icc (shift + rate * a) (shift + rate * b))) =>
t.linearData.forcingAlong g copy ((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hslot : ((CopySolveCompatibility.transportGeometry g gap shift rate ⋯).coordinates copy Y).2 ∈ Set.Icc a b)
:
(ScaledTangentTransport.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.IntervalCopyTransport.copyPressureReal_transport
{P Q H : Type}
[NormedAddCommGroup H]
[InnerProductSpace ℝ H]
[CompleteSpace H]
{a b : ℝ}
(t : CommonCoverSolve.TangentData P H)
(parameter : Q → P)
(g : CommonCoverSolve.Geometry)
(hab : a ≤ b)
(gap : ℕ)
(shift rate amplitude normalScale : ℝ)
(hrate : 0 < rate)
(hnormal : normalScale ≠ 0)
(q : Q)
(copy : TorusInverse.Frequency)
(Y : TorusInverse.Plane)
(hA :
Continuous fun (s : ↑(Set.Icc (shift + rate * a) (shift + rate * b))) =>
t.linearData.coefficientAlong g copy ((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hf :
Continuous fun (s : ↑(Set.Icc (shift + rate * a) (shift + rate * b))) =>
t.linearData.forcingAlong g copy ((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hslot : ((CopySolveCompatibility.transportGeometry g gap shift rate ⋯).coordinates copy Y).2 ∈ Set.Icc a b)
:
ParticularWaveBounds.copyPressureReal
(ScaledTangentTransport.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.IntervalCopyTransport.copyPressure_transport
{P Q H : Type}
[NormedAddCommGroup H]
[InnerProductSpace ℝ H]
[CompleteSpace H]
{a b : ℝ}
(t : CommonCoverSolve.TangentData P H)
(parameter : Q → P)
(g : CommonCoverSolve.Geometry)
(hab : a ≤ b)
(gap : ℕ)
(shift rate amplitude normalScale referenceFrequency frequency : ℝ)
(hrate : 0 < rate)
(hnormal : normalScale ≠ 0)
(hreference : referenceFrequency ≠ 0)
(hfrequency : frequency ≠ 0)
(q : Q)
(copy : TorusInverse.Frequency)
(Y : TorusInverse.Plane)
(hA :
Continuous fun (s : ↑(Set.Icc (shift + rate * a) (shift + rate * b))) =>
t.linearData.coefficientAlong g copy ((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hf :
Continuous fun (s : ↑(Set.Icc (shift + rate * a) (shift + rate * b))) =>
t.linearData.forcingAlong g copy ((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hslot : ((CopySolveCompatibility.transportGeometry g gap shift rate ⋯).coordinates copy Y).2 ∈ Set.Icc a b)
:
ParticularWaveBounds.copyPressure
(ScaledTangentTransport.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)
theorem
NavierStokes.IntervalCopyTransport.copyVelocity_transport
{P Q : Type}
{a b : ℝ}
(t : CommonCoverSolve.TangentData P ProblemStatement.Space)
(parameter : Q → P)
(g : CommonCoverSolve.Geometry)
(hab : a ≤ b)
(gap : ℕ)
(shift rate amplitude normalScale : ℝ)
(hrate : 0 < rate)
(hnormal : normalScale ≠ 0)
(q : Q)
(copy : TorusInverse.Frequency)
(Y : TorusInverse.Plane)
(hA :
Continuous fun (s : ↑(Set.Icc (shift + rate * a) (shift + rate * b))) =>
t.linearData.coefficientAlong g copy ((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hf :
Continuous fun (s : ↑(Set.Icc (shift + rate * a) (shift + rate * b))) =>
t.linearData.forcingAlong g copy ((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hslot : ((CopySolveCompatibility.transportGeometry g gap shift rate ⋯).coordinates copy Y).2 ∈ Set.Icc a b)
:
ParticularWaveBounds.copyVelocity
(ScaledTangentTransport.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.IntervalCopyTransport.complexCopyVelocity_transport
{P Q : Type}
{a b : ℝ}
(t : CommonCoverSolve.TangentData P ProblemStatement.Space)
(f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector)
(parameter : Q → P)
(g : CommonCoverSolve.Geometry)
(hab : a ≤ b)
(gap : ℕ)
(shift rate amplitude normalScale : ℝ)
(hrate : 0 < rate)
(hnormal : normalScale ≠ 0)
(q : Q)
(copy : TorusInverse.Frequency)
(Y : TorusInverse.Plane)
(hA :
Continuous fun (s : ↑(Set.Icc (shift + rate * a) (shift + rate * b))) =>
t.linearData.coefficientAlong g copy ((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hReal :
Continuous fun (s : ↑(Set.Icc (shift + rate * a) (shift + rate * b))) =>
(ParticularWaveBounds.realData t f).linearData.forcingAlong g copy
((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hImag :
Continuous fun (s : ↑(Set.Icc (shift + rate * a) (shift + rate * b))) =>
(ParticularWaveBounds.imagData t f).linearData.forcingAlong g copy
((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hslot : ((CopySolveCompatibility.transportGeometry g gap shift rate ⋯).coordinates copy Y).2 ∈ Set.Icc a b)
:
ParticularWaveBounds.complexCopyVelocity
(ScaledTangentTransport.transportTangent t parameter gap shift rate amplitude normalScale)
(ScaledTangentTransport.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.IntervalCopyTransport.complexCopyPressure_transport
{P Q : Type}
{a b : ℝ}
(t : CommonCoverSolve.TangentData P ProblemStatement.Space)
(f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector)
(parameter : Q → P)
(g : CommonCoverSolve.Geometry)
(hab : a ≤ b)
(gap : ℕ)
(shift rate amplitude normalScale referenceFrequency frequency : ℝ)
(hrate : 0 < rate)
(hnormal : normalScale ≠ 0)
(hreference : referenceFrequency ≠ 0)
(hfrequency : frequency ≠ 0)
(q : Q)
(copy : TorusInverse.Frequency)
(Y : TorusInverse.Plane)
(hA :
Continuous fun (s : ↑(Set.Icc (shift + rate * a) (shift + rate * b))) =>
t.linearData.coefficientAlong g copy ((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hReal :
Continuous fun (s : ↑(Set.Icc (shift + rate * a) (shift + rate * b))) =>
(ParticularWaveBounds.realData t f).linearData.forcingAlong g copy
((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hImag :
Continuous fun (s : ↑(Set.Icc (shift + rate * a) (shift + rate * b))) =>
(ParticularWaveBounds.imagData t f).linearData.forcingAlong g copy
((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hslot : ((CopySolveCompatibility.transportGeometry g gap shift rate ⋯).coordinates copy Y).2 ∈ Set.Icc a b)
:
ParticularWaveBounds.complexCopyPressure
(ScaledTangentTransport.transportTangent t parameter gap shift rate amplitude normalScale)
(ScaledTangentTransport.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.IntervalCopyTransport.complexCopyVelocity_zeroEntry
{P Q : Type}
(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)
(q : Q)
(copy : TorusInverse.Frequency)
(Y : TorusInverse.Plane)
(hA :
Continuous fun (s : ↑(Set.Icc 0 L)) =>
t.linearData.coefficientAlong g copy ((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hReal :
Continuous fun (s : ↑(Set.Icc 0 L)) =>
(ParticularWaveBounds.realData t f).linearData.forcingAlong g copy
((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hImag :
Continuous fun (s : ↑(Set.Icc 0 L)) =>
(ParticularWaveBounds.imagData t f).linearData.forcingAlong g copy
((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hslot : ((CopySolveCompatibility.transportGeometry g gap 0 rate ⋯).coordinates copy Y).2 ∈ Set.Icc 0 (L / rate))
:
ParticularWaveBounds.complexCopyVelocity
(ScaledTangentTransport.transportTangent t parameter gap 0 rate amplitude normalScale)
(ScaledTangentTransport.transportSource f parameter gap rate amplitude)
(CopySolveCompatibility.transportGeometry g gap 0 rate ⋯) ⋯ copy (q, Y) = amplitude • ParticularWaveBounds.complexCopyVelocity t f g ⋯ copy (parameter q, (CommonCoverSolve.coverPower gap) Y)
Exact zero-entry velocity transport from the reference interval [0,L].
The coefficient and the two converted forcing paths are the only analytic
inputs, all restricted to that finite interval.
theorem
NavierStokes.IntervalCopyTransport.complexCopyPressure_zeroEntry
{P Q : Type}
(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)
(q : Q)
(copy : TorusInverse.Frequency)
(Y : TorusInverse.Plane)
(hA :
Continuous fun (s : ↑(Set.Icc 0 L)) =>
t.linearData.coefficientAlong g copy ((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hReal :
Continuous fun (s : ↑(Set.Icc 0 L)) =>
(ParticularWaveBounds.realData t f).linearData.forcingAlong g copy
((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hImag :
Continuous fun (s : ↑(Set.Icc 0 L)) =>
(ParticularWaveBounds.imagData t f).linearData.forcingAlong g copy
((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hslot : ((CopySolveCompatibility.transportGeometry g gap 0 rate ⋯).coordinates copy Y).2 ∈ Set.Icc 0 (L / rate))
:
ParticularWaveBounds.complexCopyPressure
(ScaledTangentTransport.transportTangent t parameter gap 0 rate amplitude normalScale)
(ScaledTangentTransport.transportSource f parameter gap rate amplitude)
(CopySolveCompatibility.transportGeometry g gap 0 rate ⋯) ⋯ copy frequency (q, Y) = (rate * amplitude / normalScale * (referenceFrequency / frequency)) • ParticularWaveBounds.complexCopyPressure t f g ⋯ copy referenceFrequency
(parameter q, (CommonCoverSolve.coverPower gap) Y)
The actual pressure retains both the clock/normal factor and the ratio of reference to current frequency.
theorem
NavierStokes.IntervalCopyTransport.forcingAlong_continuous
{P V E : Type}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a b : ℝ}
(d : CommonCoverSolve.LinearData P V E)
(g : CommonCoverSolve.Geometry)
(copy : TorusInverse.Frequency)
(p : P)
(Y : TorusInverse.Plane)
(hB : Continuous fun (s : ↑(Set.Icc a b)) => d.forcingMap (p, (g.coordinates copy Y).1, ↑s))
(hf : Continuous fun (s : ↑(Set.Icc a b)) => d.source (p, g.path copy Y ↑s))
:
Continuous fun (s : ↑(Set.Icc a b)) => d.forcingAlong g copy ((p, Y), ↑s)
Continuity of the converted forcing can be checked on the finite native coefficient segment and the corresponding finite common-coordinate path.
theorem
NavierStokes.IntervalCopyTransport.real_forcingAlong_continuous
{P : Type}
{a b : ℝ}
(t : CommonCoverSolve.TangentData P ProblemStatement.Space)
(f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector)
(g : CommonCoverSolve.Geometry)
(copy : TorusInverse.Frequency)
(p : P)
(Y : TorusInverse.Plane)
(hB : Continuous fun (s : ↑(Set.Icc a b)) => t.linearData.forcingMap (p, (g.coordinates copy Y).1, ↑s))
(hf : Continuous fun (s : ↑(Set.Icc a b)) => f (p, g.path copy Y ↑s))
:
Continuous fun (s : ↑(Set.Icc a b)) => (ParticularWaveBounds.realData t f).linearData.forcingAlong g copy ((p, Y), ↑s)
theorem
NavierStokes.IntervalCopyTransport.imag_forcingAlong_continuous
{P : Type}
{a b : ℝ}
(t : CommonCoverSolve.TangentData P ProblemStatement.Space)
(f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector)
(g : CommonCoverSolve.Geometry)
(copy : TorusInverse.Frequency)
(p : P)
(Y : TorusInverse.Plane)
(hB : Continuous fun (s : ↑(Set.Icc a b)) => t.linearData.forcingMap (p, (g.coordinates copy Y).1, ↑s))
(hf : Continuous fun (s : ↑(Set.Icc a b)) => f (p, g.path copy Y ↑s))
:
Continuous fun (s : ↑(Set.Icc a b)) => (ParticularWaveBounds.imagData t f).linearData.forcingAlong g copy ((p, Y), ↑s)
theorem
NavierStokes.IntervalCopyTransport.commonVelocity_zeroEntry
{P Q : Type}
(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)
(cutoff : TorusInverse.Plane → ℝ)
(hcutoff : Function.support cutoff ⊆ Set.univ ×ˢ Set.Icc 0 L)
(q : Q)
(Y : TorusInverse.Plane)
(hA :
∀ (copy : TorusInverse.Frequency),
cutoff (g.coordinates copy ((CommonCoverSolve.coverPower gap) Y)) ≠ 0 →
Continuous fun (s : ↑(Set.Icc 0 L)) =>
t.linearData.coefficientAlong g copy ((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hReal :
∀ (copy : TorusInverse.Frequency),
cutoff (g.coordinates copy ((CommonCoverSolve.coverPower gap) Y)) ≠ 0 →
Continuous fun (s : ↑(Set.Icc 0 L)) =>
(ParticularWaveBounds.realData t f).linearData.forcingAlong g copy
((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hImag :
∀ (copy : TorusInverse.Frequency),
cutoff (g.coordinates copy ((CommonCoverSolve.coverPower gap) Y)) ≠ 0 →
Continuous fun (s : ↑(Set.Icc 0 L)) =>
(ParticularWaveBounds.imagData t f).linearData.forcingAlong g copy
((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
:
ParticularWaveBounds.commonVelocity
(ScaledTangentTransport.transportTangent t parameter gap 0 rate amplitude normalScale)
(ScaledTangentTransport.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)
Equality of the literal periodized velocities. Only active copies need
continuous reference paths, and only on the interval [0,L].
theorem
NavierStokes.IntervalCopyTransport.commonPressure_zeroEntry
{P Q : Type}
(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)
(cutoff : TorusInverse.Plane → ℝ)
(hcutoff : Function.support cutoff ⊆ Set.univ ×ˢ Set.Icc 0 L)
(q : Q)
(Y : TorusInverse.Plane)
(hA :
∀ (copy : TorusInverse.Frequency),
cutoff (g.coordinates copy ((CommonCoverSolve.coverPower gap) Y)) ≠ 0 →
Continuous fun (s : ↑(Set.Icc 0 L)) =>
t.linearData.coefficientAlong g copy ((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hReal :
∀ (copy : TorusInverse.Frequency),
cutoff (g.coordinates copy ((CommonCoverSolve.coverPower gap) Y)) ≠ 0 →
Continuous fun (s : ↑(Set.Icc 0 L)) =>
(ParticularWaveBounds.realData t f).linearData.forcingAlong g copy
((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
(hImag :
∀ (copy : TorusInverse.Frequency),
cutoff (g.coordinates copy ((CommonCoverSolve.coverPower gap) Y)) ≠ 0 →
Continuous fun (s : ↑(Set.Icc 0 L)) =>
(ParticularWaveBounds.imagData t f).linearData.forcingAlong g copy
((parameter q, (CommonCoverSolve.coverPower gap) Y), ↑s))
:
ParticularWaveBounds.commonPressure
(ScaledTangentTransport.transportTangent t parameter gap 0 rate amplitude normalScale)
(ScaledTangentTransport.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)
Equality of the literal periodized pressures, with the same finite reference paths and the actual inverse-frequency scaling.
Naturality of the actual Gaussian cutoff error #
The error is the sum of differentiated-cutoff terms and the uncovered source. Both terms are transported from their primitive data before the copy sum is taken.
theorem
NavierStokes.GaussianErrorNaturality.fast_cutoff_transport
{D E I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(Γ : D →L[ℝ] E)
(d : LinearWaveBounds.GraphDirections D)
(dr : LinearWaveBounds.GraphDirections E)
(a : PeriodizedWaveBounds.CopyData D I)
(b : PeriodizedWaveBounds.CopyData E I)
(n nr : ℕ)
(rate : ℝ)
(i : I)
(x : D)
(hcutoff : a.cutoff n i = fun (y : D) => b.cutoff nr i (Γ y))
(hfast : Γ (d.fastField n x) = rate • dr.fastField nr (Γ x))
(hdiff : DifferentiableAt ℝ (b.cutoff nr i) (Γ x))
:
theorem
NavierStokes.GaussianErrorNaturality.cutoffSum_transport
{D E I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(Γ : D →L[ℝ] E)
(a : PeriodizedWaveBounds.CopyData D I)
(b : PeriodizedWaveBounds.CopyData E I)
(n nr : ℕ)
(x : D)
(hcutoff : ∀ (i : I), a.cutoff n i x = b.cutoff nr i (Γ x))
:
theorem
NavierStokes.GaussianErrorNaturality.localTail_transport
{D E I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(Γ : D →L[ℝ] E)
(d : LinearWaveBounds.GraphDirections D)
(dr : LinearWaveBounds.GraphDirections E)
(a : PeriodizedWaveBounds.CopyData D I)
(b : PeriodizedWaveBounds.CopyData E I)
(n nr : ℕ)
(rate c : ℝ)
(i : I)
(x : D)
(hcutoff : a.cutoff n i = fun (y : D) => b.cutoff nr i (Γ y))
(hfast : Γ (d.fastField n x) = rate • dr.fastField nr (Γ x))
(hdiff : DifferentiableAt ℝ (b.cutoff nr i) (Γ x))
(hamplitude : dr.Dfast (fun (m : ℕ) => b.cutoff m i) nr (Γ x) ≠ 0 → a.amplitude n i x = c • b.amplitude nr i (Γ x))
:
theorem
NavierStokes.GaussianErrorNaturality.globalTail_transport
{D E I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(Γ : D →L[ℝ] E)
(d : LinearWaveBounds.GraphDirections D)
(dr : LinearWaveBounds.GraphDirections E)
(a : PeriodizedWaveBounds.CopyData D I)
(b : PeriodizedWaveBounds.CopyData E I)
(n nr : ℕ)
(rate c : ℝ)
(x : D)
(hcutoff : ∀ (i : I), a.cutoff n i = fun (y : D) => b.cutoff nr i (Γ y))
(hfast : Γ (d.fastField n x) = rate • dr.fastField nr (Γ x))
(hdiff : ∀ (i : I), DifferentiableAt ℝ (b.cutoff nr i) (Γ x))
(hamplitude :
∀ (i : I), dr.Dfast (fun (m : ℕ) => b.cutoff m i) nr (Γ x) ≠ 0 → a.amplitude n i x = c • b.amplitude nr i (Γ x))
:
Only copies with a nonzero differentiated reference cutoff need an amplitude comparison. No exterior continuation of a Volterra solve is assumed.
theorem
NavierStokes.GaussianErrorNaturality.globalGaussian_transport
{D E I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(Γ : D →L[ℝ] E)
(d : LinearWaveBounds.GraphDirections D)
(dr : LinearWaveBounds.GraphDirections E)
(a : PeriodizedWaveBounds.CopyData D I)
(b : PeriodizedWaveBounds.CopyData E I)
(n nr : ℕ)
(rate c : ℝ)
(x : D)
(hcutoff : ∀ (i : I), a.cutoff n i = fun (y : D) => b.cutoff nr i (Γ y))
(hfast : Γ (d.fastField n x) = rate • dr.fastField nr (Γ x))
(hdiff : ∀ (i : I), DifferentiableAt ℝ (b.cutoff nr i) (Γ x))
(hamplitude :
∀ (i : I), dr.Dfast (fun (m : ℕ) => b.cutoff m i) nr (Γ x) ≠ 0 → a.amplitude n i x = c • b.amplitude nr i (Γ x))
(hsource : a.source n x = (rate * c) • b.source nr (Γ x))
:
Full transport of the actual Gaussian error, including the source on the part of the domain uncovered by native cutoffs.
@[reducible, inline]
Parameter: an abbreviation for PhysicalParticularWave.Parameter.
Equations
Instances For
@[reducible, inline]
Wave space: an abbreviation for PhysicalParticularWave.WaveSpace.
Equations
Instances For
@[reducible, inline]
Cylinder: an abbreviation for PhysicalParticularWave.Cylinder.
Equations
Instances For
The full native change of variables, conjugate to the actual cylindrical change of band and common cover.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
NavierStokes.GaussianErrorNaturality.waveChange_apply
(h Q Qr : ℝ)
(gap : ℕ)
(x : WaveSpace)
:
(waveChange h Q Qr gap) x = ((PhysicalParticularWave.parameterChange h Q Qr x.1.1, x.1.2), (CommonCoverSolve.coverPower gap) x.2)
theorem
NavierStokes.GaussianErrorNaturality.waveChange_waveEquiv
(h Q Qr : ℝ)
(gap : ℕ)
(x : Cylinder)
:
(waveChange h Q Qr gap) (PhysicalParticularWave.waveEquiv x) = PhysicalParticularWave.waveEquiv ((PhysicalParticularWave.cylinderChange h Q Qr gap) x)
noncomputable def
NavierStokes.GaussianErrorNaturality.referenceParameters
(D : ParticularWaveAssembly.AssemblyData Parameter)
:
The actual untransported reference data, evaluated at its own band.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.GaussianErrorNaturality.nativeData
(D : ParticularWaveAssembly.AssemblyData Parameter)
(h : ℝ)
(gap : ℕ → ℕ)
(j : ℤ)
:
Native data as an element of PeriodizedWaveBounds.CopyData WaveSpace Frequency.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.GaussianErrorNaturality.referenceData
(D : ParticularWaveAssembly.AssemblyData Parameter)
(j : ℤ)
:
Reference data, given by (referenceParameters D).copyData D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j.
Equations
Instances For
theorem
NavierStokes.GaussianErrorNaturality.copyData_amplitude
(p : CorrectionStep.ParticularParameters Parameter)
(C : CorrectionState.Context (Parameter × TorusInverse.Plane))
(u : CorrectionState.State (Parameter × TorusInverse.Plane))
(b : CorrectionState.HarmonicBlock (Parameter × TorusInverse.Plane))
(G A : HarmonicResidual.BlockCoefficients (Parameter × TorusInverse.Plane))
(j : ℤ)
(n : ℕ)
(copy : TorusInverse.Frequency)
(x : WaveSpace)
:
(p.copyData C u b G A j).amplitude n copy x = ParticularWaveBounds.complexCopyVelocity (p.tangent j n) (ParticularWaveAssembly.residualSource C u b G A j n)
(p.geometry n) ⋯ copy (x.1.1, x.2)
theorem
NavierStokes.GaussianErrorNaturality.native_cutoff_transport
(D : ParticularWaveAssembly.AssemblyData Parameter)
(h : ℝ)
(gap : ℕ → ℕ)
(j : ℤ)
(n : ℕ)
(copy : TorusInverse.Frequency)
:
(nativeData D h gap j).cutoff n copy = fun (x : WaveSpace) =>
(referenceData D j).cutoff D.reference.band copy
((waveChange h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n)) x)
theorem
NavierStokes.GaussianErrorNaturality.reference_cutoff_differentiable
(D : ParticularWaveAssembly.AssemblyData Parameter)
(j : ℤ)
(hcutoff : ContDiff ℝ (↑⊤) D.reference.cutoff)
(copy : TorusInverse.Frequency)
(x : WaveSpace)
:
DifferentiableAt ℝ ((referenceData D j).cutoff D.reference.band copy) x
theorem
NavierStokes.GaussianErrorNaturality.along_ne_zero_mem_closed
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : E → ℝ}
{K : Set E}
(hK : IsClosed K)
(hf : Function.support f ⊆ K)
(V : E → E)
{x : E}
(hx : HarmonicCalculus.along V f x ≠ 0)
:
A nonzero actual directional derivative is supported in any closed set supporting the original cutoff.
theorem
NavierStokes.GaussianErrorNaturality.reference_derivative_mem_slot
(D : ParticularWaveAssembly.AssemblyData Parameter)
(j : ℤ)
{U : Set Parameter}
(R : PhysicalParticularWave.ReferenceODE D j U)
(copy : TorusInverse.Frequency)
{x : WaveSpace}
(hx : D.directions.Dfast (fun (m : ℕ) => (referenceData D j).cutoff m copy) D.reference.band x ≠ 0)
:
theorem
NavierStokes.GaussianErrorNaturality.current_slot_of_reference_derivative
(D : ParticularWaveAssembly.AssemblyData Parameter)
(h : ℝ)
(gap : ℕ → ℕ)
(j : ℤ)
(n : ℕ)
{U : Set Parameter}
(R : PhysicalParticularWave.ReferenceODE D j U)
(copy : TorusInverse.Frequency)
(x : WaveSpace)
(hx :
D.directions.Dfast (fun (m : ℕ) => (referenceData D j).cutoff m copy) D.reference.band
((waveChange h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n)) x) ≠ 0)
:
(((CorrectionStep.ParticularParameters.fromReference D h gap).geometry n).coordinates copy x.2).2 ∈ Set.Icc 0 ((CorrectionStep.ParticularParameters.fromReference D h gap).length n)
theorem
NavierStokes.GaussianErrorNaturality.complexCopyVelocity_zeroEntry
(t : CommonCoverSolve.TangentData Parameter ProblemStatement.Space)
(f : Parameter × TorusInverse.Plane → HarmonicCalculus.ComplexVector)
(parameter : Parameter → Parameter)
(g : CommonCoverSolve.Geometry)
(gap : ℕ)
(L rate amplitude normalScale : ℝ)
(hL : 0 < L)
(hrate : 0 < rate)
(hnormal : normalScale ≠ 0)
{U : Set Parameter}
(hA : ContinuousOn t.linearData.coefficient (U ×ˢ Set.univ))
(hB : ContinuousOn t.linearData.forcingMap (U ×ˢ Set.univ))
(hf : ContinuousOn f (U ×ˢ Set.univ))
(q : Parameter)
(hq : parameter q ∈ U)
(copy : TorusInverse.Frequency)
(Y : TorusInverse.Plane)
(hslot : ((CopySolveCompatibility.transportGeometry g gap 0 rate ⋯).coordinates copy Y).2 ∈ Set.Icc 0 (L / rate))
:
ParticularWaveBounds.complexCopyVelocity
(ScaledTangentTransport.transportTangent t parameter gap 0 rate amplitude normalScale)
(ScaledTangentTransport.transportSource f parameter gap rate amplitude)
(CopySolveCompatibility.transportGeometry g gap 0 rate ⋯) ⋯ copy (q, Y) = amplitude • ParticularWaveBounds.complexCopyVelocity t f g ⋯ copy (parameter q, (CommonCoverSolve.coverPower gap) Y)
theorem
NavierStokes.GaussianErrorNaturality.native_source_transport
(D : ParticularWaveAssembly.AssemblyData Parameter)
(h : ℝ)
(gap : ℕ → ℕ)
(j : ℤ)
(n i : ℕ)
(H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n)
(hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n)
(hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band)
(x : WaveSpace)
:
(nativeData D h gap j).source n x = (PhysicalParticularWave.clockWeight h (ChartScales.Q n) (ChartScales.Q D.reference.band) * PhysicalParticularWave.velocityWeight h (ChartScales.Q n) (ChartScales.Q D.reference.band)) • (referenceData D j).source D.reference.band
((waveChange h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n)) x)
theorem
NavierStokes.GaussianErrorNaturality.native_amplitude_transport
(D : ParticularWaveAssembly.AssemblyData Parameter)
(h : ℝ)
(gap : ℕ → ℕ)
(j : ℤ)
(n i : ℕ)
(H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n)
(hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n)
(hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band)
{U : Set Parameter}
(R : PhysicalParticularWave.ReferenceODE D j U)
(hK : ↑j * D.carrierBlock.frequency n ≠ 0)
(hKr : PhysicalParticularWave.referenceFrequency D j ≠ 0)
(copy : TorusInverse.Frequency)
(x : WaveSpace)
(hx : PhysicalParticularWave.parameterChange h (ChartScales.Q n) (ChartScales.Q D.reference.band) x.1.1 ∈ U)
(hslot :
(((CorrectionStep.ParticularParameters.fromReference D h gap).geometry n).coordinates copy x.2).2 ∈ Set.Icc 0 ((CorrectionStep.ParticularParameters.fromReference D h gap).length n))
:
(nativeData D h gap j).amplitude n copy x = PhysicalParticularWave.velocityWeight h (ChartScales.Q n) (ChartScales.Q D.reference.band) • (referenceData D j).amplitude D.reference.band copy
((waveChange h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n)) x)
theorem
NavierStokes.GaussianErrorNaturality.fast_transport_of_slotDirections
(D : ParticularWaveAssembly.AssemblyData Parameter)
(h : ℝ)
(gap : ℕ → ℕ)
(n : ℕ)
(hn :
D.directions.fastScale n • D.directions.fast = (0, ParticularWaveBounds.slotDirection ((CorrectionStep.ParticularParameters.fromReference D h gap).geometry n)))
(hr :
D.directions.fastScale D.reference.band • D.directions.fast = (0, ParticularWaveBounds.slotDirection D.reference.geometry))
:
(waveChange h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n))
(D.directions.fastScale n • D.directions.fast) = PhysicalParticularWave.clockWeight h (ChartScales.Q n) (ChartScales.Q D.reference.band) • D.directions.fastScale D.reference.band • D.directions.fast
The fast transport hypothesis follows from the actual slot-direction identities stored by the primitive copy geometry.
theorem
NavierStokes.GaussianErrorNaturality.fromReference_globalGaussian
(D : ParticularWaveAssembly.AssemblyData Parameter)
(h : ℝ)
(gap : ℕ → ℕ)
(j : ℤ)
(n i : ℕ)
(H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n)
(hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n)
(hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band)
{U : Set Parameter}
(R : PhysicalParticularWave.ReferenceODE D j U)
(hcutoff : ContDiff ℝ (↑⊤) D.reference.cutoff)
(hK : ↑j * D.carrierBlock.frequency n ≠ 0)
(hKr : PhysicalParticularWave.referenceFrequency D j ≠ 0)
(hfast :
(waveChange h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n))
(D.directions.fastScale n • D.directions.fast) = PhysicalParticularWave.clockWeight h (ChartScales.Q n) (ChartScales.Q D.reference.band) • D.directions.fastScale D.reference.band • D.directions.fast)
(x : WaveSpace)
(hx : PhysicalParticularWave.parameterChange h (ChartScales.Q n) (ChartScales.Q D.reference.band) x.1.1 ∈ U)
:
(nativeData D h gap j).globalGaussian D.directions n x = PhysicalParticularWave.sourceWeight h (ChartScales.Q n) (ChartScales.Q D.reference.band) • (referenceData D j).globalGaussian D.directions D.reference.band
((waveChange h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n)) x)
The actual transported reference solve has the derived Gaussian source weight on the full native cylinder, including uncovered points.
theorem
NavierStokes.GaussianErrorNaturality.fromReference_globalGaussian_cylinder
(D : ParticularWaveAssembly.AssemblyData Parameter)
(h : ℝ)
(gap : ℕ → ℕ)
(j : ℤ)
(n i : ℕ)
(H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n)
(hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n)
(hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band)
{U : Set Parameter}
(R : PhysicalParticularWave.ReferenceODE D j U)
(hcutoff : ContDiff ℝ (↑⊤) D.reference.cutoff)
(hK : ↑j * D.carrierBlock.frequency n ≠ 0)
(hKr : PhysicalParticularWave.referenceFrequency D j ≠ 0)
(hfast :
(waveChange h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n))
(D.directions.fastScale n • D.directions.fast) = PhysicalParticularWave.clockWeight h (ChartScales.Q n) (ChartScales.Q D.reference.band) • D.directions.fastScale D.reference.band • D.directions.fast)
(x : Cylinder)
(hx :
PhysicalParticularWave.parameterChange h (ChartScales.Q n) (ChartScales.Q D.reference.band)
(PhysicalParticularWave.waveEquiv x).1.1 ∈ U)
:
(nativeData D h gap j).globalGaussian D.directions n (PhysicalParticularWave.waveEquiv x) = (PhysicalParticularWave.velocityWeight h (ChartScales.Q n) (ChartScales.Q D.reference.band) ^ 2 * PhysicalParticularWave.ratioPower (ChartScales.Q n) (ChartScales.Q D.reference.band) (1 / 2)) • (referenceData D j).globalGaussian D.directions D.reference.band
(PhysicalParticularWave.waveEquiv
((PhysicalParticularWave.cylinderChange h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n)) x))
theorem
NavierStokes.GaussianErrorNaturality.fromReference_gaussian_character
(D : ParticularWaveAssembly.AssemblyData Parameter)
(h : ℝ)
(gap : ℕ → ℕ)
(j : ℤ)
(n i : ℕ)
(H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n)
(hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n)
(hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band)
{U : Set Parameter}
(R : PhysicalParticularWave.ReferenceODE D j U)
(hcutoff : ContDiff ℝ (↑⊤) D.reference.cutoff)
(hK : ↑j * D.carrierBlock.frequency n ≠ 0)
(hKr : PhysicalParticularWave.referenceFrequency D j ≠ 0)
(hfast :
(waveChange h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n))
(D.directions.fastScale n • D.directions.fast) = PhysicalParticularWave.clockWeight h (ChartScales.Q n) (ChartScales.Q D.reference.band) • D.directions.fastScale D.reference.band • D.directions.fast)
(x : Parameter × TorusInverse.Plane)
(hxpos : 0 < x.1.1)
(hx : PhysicalParticularWave.parameterChange h (ChartScales.Q n) (ChartScales.Q D.reference.band) x.1 ∈ U)
(θ : ℝ)
(k : Fin 3)
:
((nativeData D h gap j).globalGaussian D.directions n (ParticularWaveAssembly.angleShuffle (x, 0)) k * HarmonicFields.character j
(D.carrierBlock.frequency n * D.carrierBlock.phase n x + ↑(D.carrierBlock.angularFrequency n) * θ)).re = PhysicalParticularWave.sourceWeight h (ChartScales.Q n) (ChartScales.Q D.reference.band) * ((referenceData D j).globalGaussian D.directions D.reference.band
(ParticularWaveAssembly.angleShuffle ((PhysicalResidualNaturality.associatedChart h ⋯ ⋯ (gap n)) x, 0)) k * HarmonicFields.character j
(D.carrierBlock.frequency D.reference.band * D.carrierBlock.phase D.reference.band ((PhysicalResidualNaturality.associatedChart h ⋯ ⋯ (gap n)) x) + ↑(D.carrierBlock.angularFrequency D.reference.band) * θ)).re
A single actual Gaussian Fourier contribution transports with its full angular carrier. The reference phase relation is primitive block coherence; the Gaussian coefficient relation is proved from the solve.
theorem
NavierStokes.GaussianErrorNaturality.fromReference_gaussianBlock
(D : ParticularWaveAssembly.AssemblyData Parameter)
(h : ℝ)
(gap : ℕ → ℕ)
(N n i : ℕ)
(H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n)
(hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n)
(hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band)
{U : Set Parameter}
(R : ∀ j ∈ ParticularWaveAssembly.modes N, PhysicalParticularWave.ReferenceODE D j U)
(hcutoff : ContDiff ℝ (↑⊤) D.reference.cutoff)
(hfrequency : ∀ (m : ℕ), D.carrierBlock.frequency m ≠ 0)
(hfast :
(waveChange h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n))
(D.directions.fastScale n • D.directions.fast) = PhysicalParticularWave.clockWeight h (ChartScales.Q n) (ChartScales.Q D.reference.band) • D.directions.fastScale D.reference.band • D.directions.fast)
(x : Parameter × TorusInverse.Plane)
(hxpos : 0 < x.1.1)
(hx : PhysicalParticularWave.parameterChange h (ChartScales.Q n) (ChartScales.Q D.reference.band) x.1 ∈ U)
(θ : ℝ)
(k : Fin 3)
:
((CorrectionStep.ParticularParameters.fromReference D h gap).gaussianBlock D.context D.state D.carrierBlock
D.gaussianInput D.aliasInput N).oscillation
n (x, θ) k = PhysicalParticularWave.sourceWeight h (ChartScales.Q n) (ChartScales.Q D.reference.band) * ((referenceParameters D).gaussianBlock D.context D.state D.carrierBlock D.gaussianInput D.aliasInput N).oscillation
D.reference.band ((PhysicalResidualNaturality.associatedChart h ⋯ ⋯ (gap n)) x, θ) k
Naturality of the actual finite Gaussian harmonic block, with all angular variables retained. No equality of Gaussian outputs is assumed.
theorem
NavierStokes.GaussianErrorNaturality.fromReference_gaussianBlock_cylinder
(D : ParticularWaveAssembly.AssemblyData Parameter)
(h : ℝ)
(gap : ℕ → ℕ)
(N n i : ℕ)
(H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n)
(hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n)
(hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band)
{U : Set Parameter}
(R : ∀ j ∈ ParticularWaveAssembly.modes N, PhysicalParticularWave.ReferenceODE D j U)
(hcutoff : ContDiff ℝ (↑⊤) D.reference.cutoff)
(hfrequency : ∀ (m : ℕ), D.carrierBlock.frequency m ≠ 0)
(hfast :
(waveChange h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n))
(D.directions.fastScale n • D.directions.fast) = PhysicalParticularWave.clockWeight h (ChartScales.Q n) (ChartScales.Q D.reference.band) • D.directions.fastScale D.reference.band • D.directions.fast)
(x : Cylinder)
(hxpos : 0 < x.1.1)
(hx :
PhysicalParticularWave.parameterChange h (ChartScales.Q n) (ChartScales.Q D.reference.band)
(PhysicalParticularWave.waveEquiv x).1.1 ∈ U)
(k : Fin 3)
:
((CorrectionStep.ParticularParameters.fromReference D h gap).gaussianBlock D.context D.state D.carrierBlock
D.gaussianInput D.aliasInput N).oscillation
n (ParticularWaveAssembly.angleShuffle.symm (PhysicalParticularWave.waveEquiv x)) k = PhysicalParticularWave.velocityWeight h (ChartScales.Q n) (ChartScales.Q D.reference.band) ^ 2 * PhysicalParticularWave.ratioPower (ChartScales.Q n) (ChartScales.Q D.reference.band) (1 / 2) * ((referenceParameters D).gaussianBlock D.context D.state D.carrierBlock D.gaussianInput D.aliasInput N).oscillation
D.reference.band
(ParticularWaveAssembly.angleShuffle.symm
(PhysicalParticularWave.waveEquiv
((PhysicalParticularWave.cylinderChange h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n)) x)))
k
The same finite-block statement on the original full cylindrical
coordinates, with the source weight explicitly written as c^2 * l.
Continuity on the actual finite tangent-copy intervals #
The projected operator is built from the selected frame's normal, normal motion, base action, and damping. Only the native slow point and finite clock interval enter its regularity; the transverse coordinate is free.
@[reducible, inline]
Parameter: an abbreviation for PhysicalParticularWave.Parameter.
Equations
Instances For
theorem
NavierStokes.ActualCopySliceRegularity.negativeProjection_continuousOn
{X : Type u_1}
[TopologicalSpace X]
{U : Set X}
{N : X → Space}
(hN : ContinuousOn N U)
(hne : ∀ x ∈ U, N x ≠ 0)
:
ContinuousOn (fun (x : X) => CommonCoverSolve.negativeTangentProjection (N x)) U
theorem
NavierStokes.ActualCopySliceRegularity.frame_slices
{ι : Type}
{D : PhaseJetBounds.Domain ι PhaseCalculus.Slow}
(F : PrimaryPulseBounds.PhaseConstruction D)
(i : ι)
(j : ℤ)
(p : PhaseCalculus.Slow)
(hp : p ∈ D.carrier i)
:
(Continuous fun (s : ↑(Set.Icc 0 (F.L i))) =>
TangentODE.projectedOperator ((F.frame i).normal (p, ↑s)) ((F.frame i).normalMotion (p, ↑s))
(PrimaryCopyBridge.baseOperator ((F.frame i).F (p, ↑s)) ((F.frame i).shear (p, ↑s)))
((F.frame i).damping j (p, ↑s))) ∧ Continuous fun (s : ↑(Set.Icc 0 (F.L i))) => CommonCoverSolve.negativeTangentProjection ((F.frame i).normal (p, ↑s))
The actual ambient projected operator and forcing projection of the selected frame are continuous on the entire closed slot.
theorem
NavierStokes.ActualCopySliceRegularity.transported_coefficient
{P Q : Type}
(t : CommonCoverSolve.TangentData P Space)
(φ : Q → P)
(gap : ℕ)
(rate amplitude normal : ℝ)
(hn : normal ≠ 0)
(q : Q)
(Y : Plane)
:
(ScaledTangentTransport.transportTangent t φ gap 0 rate amplitude normal).linearData.coefficient (q, Y) = rate • t.linearData.coefficient (φ q, CopySolveCompatibility.nativeTimeMap 0 rate Y)
theorem
NavierStokes.ActualCopySliceRegularity.transported_forcingMap
{P Q : Type}
(t : CommonCoverSolve.TangentData P Space)
(φ : Q → P)
(gap : ℕ)
(rate amplitude normal : ℝ)
(hn : normal ≠ 0)
(q : Q)
(Y : Plane)
:
(ScaledTangentTransport.transportTangent t φ gap 0 rate amplitude normal).linearData.forcingMap (q, Y) = t.linearData.forcingMap (φ q, CopySolveCompatibility.nativeTimeMap 0 rate Y)
theorem
NavierStokes.ActualCopySliceRegularity.transported_slices
{P Q : Type}
(t : CommonCoverSolve.TangentData P Space)
(φ : Q → P)
(gap : ℕ)
(rate amplitude normal L : ℝ)
(hrate : 0 < rate)
(hn : normal ≠ 0)
(q : Q)
(xi : ℝ)
(hA : Continuous fun (s : ↑(Set.Icc 0 L)) => t.linearData.coefficient (φ q, xi, ↑s))
(hB : Continuous fun (s : ↑(Set.Icc 0 L)) => t.linearData.forcingMap (φ q, xi, ↑s))
:
(Continuous fun (s : ↑(Set.Icc 0 (L / rate))) =>
(ScaledTangentTransport.transportTangent t φ gap 0 rate amplitude normal).linearData.coefficient (q, xi, ↑s)) ∧ Continuous fun (s : ↑(Set.Icc 0 (L / rate))) =>
(ScaledTangentTransport.transportTangent t φ gap 0 rate amplitude normal).linearData.forcingMap (q, xi, ↑s)
theorem
NavierStokes.ActualCopySliceRegularity.reference_slices
{B N0 : ℕ}
(l : Label B N0)
(j : ℤ)
(p : Parameter)
(hp :
ActualSignedGeometry.swapParameter p ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal
(CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier
l.2)
(xi : ℝ)
:
(Continuous fun (s : ↑(Set.Icc 0 (ActualParticularStageControls.reference l).length)) =>
((ActualParticularStageControls.reference l).tangent j).linearData.coefficient (p, xi, ↑s)) ∧ Continuous fun (s : ↑(Set.Icc 0 (ActualParticularStageControls.reference l).length)) =>
((ActualParticularStageControls.reference l).tangent j).linearData.forcingMap (p, xi, ↑s)
theorem
NavierStokes.ActualCopySliceRegularity.normalWeight_ne
{B N0 : ℕ}
(l : Label B N0)
(j : ℤ)
(hj : j ≠ 0)
(n : ℕ)
:
PhysicalParticularWave.normalWeight (ChartScales.Q n) (ChartScales.Q (ActualParticularStageControls.reference l).band)
(↑j * ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n))
(↑j * ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h
(ActualParticularStageControls.reference l).band)) ≠ 0
theorem
NavierStokes.ActualCopySliceRegularity.canonical_slices
{B N0 : ℕ}
(l : Label B N0)
(j : ℤ)
(hj : j ≠ 0)
(n : ℕ)
(p : Parameter)
(hp :
ActualSignedGeometry.swapParameter
(PhysicalParticularWave.parameterChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n)
(ChartScales.Q (ActualParticularStageControls.reference l).band) p) ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal
(CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier
l.2)
(xi : ℝ)
:
(Continuous fun (s : ↑(Set.Icc 0 ((ActualParticularStageControls.canonicalParameters l).length n))) =>
((ActualParticularStageControls.canonicalParameters l).tangent j n).linearData.coefficient (p, xi, ↑s)) ∧ Continuous fun (s : ↑(Set.Icc 0 ((ActualParticularStageControls.canonicalParameters l).length n))) =>
((ActualParticularStageControls.canonicalParameters l).tangent j n).linearData.forcingMap (p, xi, ↑s)
No transverse or copy restriction occurs in these two primitive slice continuities. The only spatial hypothesis is the actual native phase cell.
theorem
NavierStokes.ActualCopySliceRegularity.actual_slices
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(hfrequency :
∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n))
(j : ℤ)
(hj : j ≠ 0)
(n : ℕ)
(p : Parameter)
(hp :
ActualSignedGeometry.swapParameter
(PhysicalParticularWave.parameterChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n)
(ChartScales.Q (ActualParticularStageControls.reference l).band) p) ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal
(CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier
l.2)
(xi : ℝ)
:
(Continuous fun (s : ↑(Set.Icc 0 ((ActualParticularStageControls.parameters x l).length n))) =>
((ActualParticularStageControls.parameters x l).tangent j n).linearData.coefficient (p, xi, ↑s)) ∧ Continuous fun (s : ↑(Set.Icc 0 ((ActualParticularStageControls.parameters x l).length n))) =>
((ActualParticularStageControls.parameters x l).tangent j n).linearData.forcingMap (p, xi, ↑s)
theorem
NavierStokes.ActualCopySliceRegularity.actual_copy_slices
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(hfrequency :
∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n))
(j : ℤ)
(hj : j ≠ 0)
(n : ℕ)
(p : Parameter)
(hp :
ActualSignedGeometry.swapParameter
(PhysicalParticularWave.parameterChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n)
(ChartScales.Q (ActualParticularStageControls.reference l).band) p) ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal
(CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier
l.2)
(Y : Plane)
(k : TorusInverse.Frequency)
:
(Continuous fun (s : ↑(Set.Icc 0 ((ActualParticularStageControls.parameters x l).length n))) =>
((ActualParticularStageControls.parameters x l).tangent j n).linearData.coefficientAlong
((ActualParticularStageControls.parameters x l).geometry n) k ((p, Y), ↑s)) ∧ Continuous fun (s : ↑(Set.Icc 0 ((ActualParticularStageControls.parameters x l).length n))) =>
((ActualParticularStageControls.parameters x l).tangent j n).linearData.forcingMap
(p, (((ActualParticularStageControls.parameters x l).geometry n).coordinates k Y).1, ↑s)
theorem
NavierStokes.ActualCopySliceRegularity.native_cell_of_refinedCarrier
{B N0 : ℕ}
(l : Label B N0)
(n : ℕ)
(p : Parameter)
(hT : 0 < p.2.1)
{Y : Plane}
(hY : (p.1, p.2, Y) ∈ ActualCoreSupport.refinedCarrier (l.2, l.1) n)
:
ActualSignedGeometry.swapParameter
(PhysicalParticularWave.parameterChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n)
(ChartScales.Q (ActualParticularStageControls.reference l).band) p) ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal
(CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier
l.2
theorem
NavierStokes.ActualCopySliceRegularity.actual_copy_slices_of_refinedFiber
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(hfrequency :
∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n))
(j : ℤ)
(hj : j ≠ 0)
(n : ℕ)
(p : Parameter)
(hT : 0 < p.2.1)
(hs : ∃ (Z : Plane), (p.1, p.2, Z) ∈ ActualCoreSupport.refinedCarrier (l.2, l.1) n)
(Y : Plane)
(k : TorusInverse.Frequency)
:
(Continuous fun (s : ↑(Set.Icc 0 ((ActualParticularStageControls.parameters x l).length n))) =>
((ActualParticularStageControls.parameters x l).tangent j n).linearData.coefficientAlong
((ActualParticularStageControls.parameters x l).geometry n) k ((p, Y), ↑s)) ∧ Continuous fun (s : ↑(Set.Icc 0 ((ActualParticularStageControls.parameters x l).length n))) =>
((ActualParticularStageControls.parameters x l).tangent j n).linearData.forcingMap
(p, (((ActualParticularStageControls.parameters x l).geometry n).coordinates k Y).1, ↑s)
A nonempty refined source fiber supplies the native phase-cell hypothesis. All copies and every transverse coordinate are then covered.
@[reducible, inline]
Label: an abbreviation for ActualParticularStageControls.Label.
Equations
Instances For
noncomputable def
NavierStokes.ActualParticularCoherence.copyData
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(j : ℤ)
:
The unchanged current-state copy construction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.ActualParticularCoherence.corrected
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(j : ℤ)
:
Corrected, constructed using ActualParticularRealization.corrected.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.ActualParticularCoherence.cylinderParameter
(z : PhysicalParticularWave.Cylinder)
:
Cylinder parameter, given by (waveEquiv z).1.1.
Equations
Instances For
noncomputable def
NavierStokes.ActualParticularCoherence.cylinderDomain
(V : Set TorusInverse.Plane)
:
Cylinder domain, given by {z | (cylinderParameter z).2 ∈ V}.
Equations
Instances For
theorem
NavierStokes.ActualParticularCoherence.cylinderDomain_open
{V : Set TorusInverse.Plane}
(hV : IsOpen V)
:
IsOpen (cylinderDomain V)
theorem
NavierStokes.ActualParticularCoherence.targetChart
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(n : ℕ)
:
The target operator is the literal common-cover graph at the target band. This identification is independent of the current source.
theorem
NavierStokes.ActualParticularCoherence.corrected_amplitude_chart
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(j : ℤ)
(n : ℕ)
:
(fun (z : PhysicalParticularWave.Cylinder) => (corrected x l j).amplitude n (PhysicalParticularWave.waveEquiv z)) = CurlClassBounds.realizedCoefficient (↑j * (x.coefficients.blocks l).frequency n)
PhysicalResidualBridge.ScaledGraph.radius
(PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h
(CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).radial
PhysicalResidualBridge.ScaledGraph.angular
(PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h
(CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).axial
(fun (z : PhysicalResidualBridge.Cylinder) =>
(ActualReferenceRebase.actualCoefficients x l j).phase n (PhysicalParticularWave.waveEquiv z))
fun (z : PhysicalResidualBridge.Cylinder) =>
(ActualReferenceRebase.actualCoefficients x l j).amplitude n (PhysicalParticularWave.waveEquiv z)
theorem
NavierStokes.ActualParticularCoherence.corrected_eq_band_of_germs
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(j : ℤ)
(n : ℕ)
(z : PhysicalParticularWave.Cylinder)
(ha :
(fun (y : PhysicalParticularWave.Cylinder) =>
(ActualReferenceRebase.actualCoefficients x l j).amplitude n (PhysicalParticularWave.waveEquiv y)) =ᶠ[nhds z] PhysicalParticularWave.bandRaw (ActualReferenceRebase.nativeAssembly x l) CorrectionInitialization.ActualPrimary.h ⋯
⋯ (ActualParticularStageControls.gap l n) (↑j * (x.coefficients.blocks l).frequency n) j)
(hphi :
(fun (y : PhysicalParticularWave.Cylinder) =>
(ActualReferenceRebase.actualCoefficients x l j).phase n (PhysicalParticularWave.waveEquiv y)) =ᶠ[nhds z] PhysicalParticularWave.bandPhase (ActualReferenceRebase.nativeAssembly x l) CorrectionInitialization.ActualPrimary.h
(ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand l.2)) (ActualParticularStageControls.gap l n)
(↑j * (x.coefficients.blocks l).frequency n) j)
:
HarmonicCalculus.vectorMode ((corrected x l j).frequency n) ((corrected x l j).phase n) ((corrected x l j).amplitude n)
(PhysicalParticularWave.waveEquiv z) = PhysicalParticularWave.bandVelocity (ActualReferenceRebase.nativeAssembly x l)
CorrectionInitialization.ActualPrimary.h ⋯ ⋯
(CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)
(ActualParticularStageControls.gap l n) (↑j * (x.coefficients.blocks l).frequency n) j z
Local agreement of the two primitive inputs propagates through the entire curl correction, including all cutoff derivatives.
theorem
NavierStokes.ActualParticularCoherence.corrected_forward
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
{V : Set TorusInverse.Plane}
(hV : IsOpen V)
(htime : ∀ s ∈ V, 0 < s.1)
(n k : ℕ)
(hi :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2))
(HS : ActualReferenceRebase.StateComparison x V n (BaseChartJets.cellBand l.2) k)
(HB : ActualReferenceRebase.BlockComparison x l V n (BaseChartJets.cellBand l.2) k)
(j : ℤ)
(hj : j ≠ 0)
(hn : (x.coefficients.blocks l).frequency n ≠ 0)
(hm : (x.coefficients.blocks l).frequency (BaseChartJets.cellBand l.2) ≠ 0)
(z : PhysicalParticularWave.Cylinder)
(hz : z ∈ cylinderDomain V)
:
HarmonicCalculus.vectorMode ((corrected x l j).frequency n) ((corrected x l j).phase n) ((corrected x l j).amplitude n)
(PhysicalParticularWave.waveEquiv z) = PhysicalParticularWave.bandVelocity (ActualReferenceRebase.nativeAssembly x l)
CorrectionInitialization.ActualPrimary.h ⋯ ⋯
(CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)
(ActualParticularStageControls.gap l n) (↑j * (x.coefficients.blocks l).frequency n) j z
Forward cover order: the germ inputs are consequences of the current state and coefficient identities, not assumptions about the solved wave.
Composition of the actual primitive copy data #
These identities allow two current bands to be compared directly. In particular, they do not require extending a current reference-band state outside the slow overlap on which state coherence was proved.
theorem
NavierStokes.ActualParticularCoherence.ratioPower_comp
{Q Qm Qr : ℝ}
(hQm : 0 < Qm)
(a : ℝ)
:
PhysicalParticularWave.ratioPower Q Qm a * PhysicalParticularWave.ratioPower Qm Qr a = PhysicalParticularWave.ratioPower Q Qr a
theorem
NavierStokes.ActualParticularCoherence.parameterChange_comp
(h Q Qm Qr : ℝ)
(hQm : 0 < Qm)
(p : PhysicalParticularWave.Parameter)
:
PhysicalParticularWave.parameterChange h Qm Qr (PhysicalParticularWave.parameterChange h Q Qm p) = PhysicalParticularWave.parameterChange h Q Qr p
theorem
NavierStokes.ActualParticularCoherence.normalWeight_comp
{Q Qm Qr K Km Kr : ℝ}
(hQm : 0 < Qm)
(hKm : Km ≠ 0)
:
PhysicalParticularWave.normalWeight Q Qm K Km * PhysicalParticularWave.normalWeight Qm Qr Km Kr = PhysicalParticularWave.normalWeight Q Qr K Kr
theorem
NavierStokes.ActualParticularCoherence.nativeTimeMap_comp
(r s : ℝ)
(z : TorusInverse.Plane)
:
theorem
NavierStokes.ActualParticularCoherence.scaledBasis_comp
(e : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane)
(r s : ℝ)
(hr : r ≠ 0)
(hs : s ≠ 0)
:
CommonCoverClass.scaledBasis (CommonCoverClass.scaledBasis e r hr) s hs = CommonCoverClass.scaledBasis e (r * s) ⋯
theorem
NavierStokes.ActualParticularCoherence.transportGeometry_comp
(g : CommonCoverSolve.Geometry)
(k d : ℕ)
(r s : ℝ)
(hr : r ≠ 0)
(hs : s ≠ 0)
:
CopySolveCompatibility.transportGeometry (CopySolveCompatibility.transportGeometry g k 0 r hr) d 0 s hs = CopySolveCompatibility.transportGeometry g (k + d) 0 (r * s) ⋯
theorem
NavierStokes.ActualParticularCoherence.transportTangent_comp
(t : CommonCoverSolve.TangentData PhysicalParticularWave.Parameter ProblemStatement.Space)
(f g : PhysicalParticularWave.Parameter → PhysicalParticularWave.Parameter)
(k d : ℕ)
(r s a b v w : ℝ)
:
ScaledTangentTransport.transportTangent (ScaledTangentTransport.transportTangent t f k 0 r a v) g d 0 s b w = ScaledTangentTransport.transportTangent t (fun (p : PhysicalParticularWave.Parameter) => f (g p)) (k + d) 0 (r * s)
(a * b) (v * w)
theorem
NavierStokes.ActualParticularCoherence.gap_comp
{B N0 : ℕ}
(l : Label B N0)
(n m k : ℕ)
(hi :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m)
(hm :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2))
:
theorem
NavierStokes.ActualParticularCoherence.parameters_geometry
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(n m k : ℕ)
(hi :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m)
(hm :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2))
:
theorem
NavierStokes.ActualParticularCoherence.parameters_length
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(n m : ℕ)
:
theorem
NavierStokes.ActualParticularCoherence.parameters_cutoff
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(n m : ℕ)
:
theorem
NavierStokes.ActualParticularCoherence.parameters_tangent
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(j : ℤ)
(n m k : ℕ)
(hi :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m)
(hm :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2))
(hKm : ↑j * (x.coefficients.blocks l).frequency m ≠ 0)
:
ScaledTangentTransport.transportTangent ((ActualParticularStageControls.parameters x l).tangent j m)
(PhysicalParticularWave.parameterChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n)
(ChartScales.Q m))
k 0
(PhysicalParticularWave.clockWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m))
(PhysicalParticularWave.velocityWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m))
(PhysicalParticularWave.normalWeight (ChartScales.Q n) (ChartScales.Q m)
(↑j * (x.coefficients.blocks l).frequency n) (↑j * (x.coefficients.blocks l).frequency m)) = (ActualParticularStageControls.parameters x l).tangent j n
theorem
NavierStokes.ActualParticularCoherence.source_band
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
{V : Set TorusInverse.Plane}
(hV : IsOpen V)
(htime : ∀ s ∈ V, 0 < s.1)
(n m k : ℕ)
(hi :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m)
(HS : ActualReferenceRebase.StateComparison x V n m k)
(HB : ActualReferenceRebase.BlockComparison x l V n m k)
(j : ℤ)
(p : PhysicalParticularWave.Parameter)
(hp : p.2 ∈ V)
(Y : TorusInverse.Plane)
:
ParticularWaveAssembly.residualSource (ActualParticularStageControls.assembly x l).context
(ActualParticularStageControls.assembly x l).state (ActualParticularStageControls.assembly x l).carrierBlock
(ActualParticularStageControls.assembly x l).gaussianInput (ActualParticularStageControls.assembly x l).aliasInput j
n (p, Y) = ScaledTangentTransport.transportSource
(ParticularWaveAssembly.residualSource (ActualParticularStageControls.assembly x l).context
(ActualParticularStageControls.assembly x l).state (ActualParticularStageControls.assembly x l).carrierBlock
(ActualParticularStageControls.assembly x l).gaussianInput (ActualParticularStageControls.assembly x l).aliasInput
j m)
(PhysicalParticularWave.parameterChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n)
(ChartScales.Q m))
k (PhysicalParticularWave.clockWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m))
(PhysicalParticularWave.velocityWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m))
(p, Y)
Actual source transport on the two-band overlap. All fast variables remain free, and all excluded residual terms are retained.
The global linear map and its actual spatial directions #
Absolute map, given by
ActualParticularStageControls.nativeToFull.toContinuousLinearEquiv.trans (ActualPrimaryCoherence.absoluteChart n).
Equations
Instances For
Band map, given by (absoluteMap n).trans (absoluteMap m).symm.
Equations
Instances For
theorem
NavierStokes.ActualParticularCoherence.absoluteMap_band
(n m : ℕ)
(z : PhysicalParticularWave.WaveSpace)
:
theorem
NavierStokes.ActualParticularCoherence.bandMap_apply
(n m k : ℕ)
(hi :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m)
(z : PhysicalParticularWave.WaveSpace)
:
(bandMap n m) z = ((PhysicalParticularWave.parameterChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m)
z.1.1, z.1.2), (CommonCoverSolve.coverPower k) z.2)
theorem
NavierStokes.ActualParticularCoherence.absoluteMap_radius
(n : ℕ)
(z : PhysicalParticularWave.WaveSpace)
:
theorem
NavierStokes.ActualParticularCoherence.absoluteMap_fast
(B n : ℕ)
(z : PhysicalParticularWave.WaveSpace)
:
theorem
NavierStokes.ActualParticularCoherence.between_direction
{E F : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
(e f : E ≃L[ℝ] F)
(a b : ℝ)
(hb : b ≠ 0)
(U V : E → E)
(W : F → F)
(he : ∀ (z : E), e (U z) = a • W (e z))
(hf : ∀ (z : E), f (V z) = b • W (f z))
(z : E)
:
theorem
NavierStokes.ActualParticularCoherence.bandMap_fast
(B n m : ℕ)
(z : PhysicalParticularWave.WaveSpace)
:
theorem
NavierStokes.ActualParticularCoherence.absoluteMap_axial
(B n : ℕ)
(z : PhysicalParticularWave.WaveSpace)
:
theorem
NavierStokes.ActualParticularCoherence.bandMap_radial
(B n m : ℕ)
(z : PhysicalParticularWave.WaveSpace)
:
(bandMap n m) (ActualParticularStageControls.directions.radialField n z) = PhysicalParticularWave.ratioPower (ChartScales.Q n) (ChartScales.Q m) (1 / 2) • ActualParticularStageControls.directions.radialField m ((bandMap n m) z)
theorem
NavierStokes.ActualParticularCoherence.bandMap_axial
(B n m : ℕ)
(z : PhysicalParticularWave.WaveSpace)
:
(bandMap n m)
(ActualParticularStageControls.directions.axialField
(CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) n z) = PhysicalParticularWave.ratioPower (ChartScales.Q n) (ChartScales.Q m) (1 / 2) • ActualParticularStageControls.directions.axialField
(CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) m
((bandMap n m) z)
theorem
NavierStokes.ActualParticularCoherence.bandMap_radius
(n m : ℕ)
(z : PhysicalParticularWave.WaveSpace)
:
((bandMap n m) z).1.1.1 = PhysicalParticularWave.ratioPower (ChartScales.Q n) (ChartScales.Q m) (1 / 2) * z.1.1.1
theorem
NavierStokes.ActualParticularCoherence.reference_cutoff_smooth
{B N0 : ℕ}
(l : Label B N0)
:
theorem
NavierStokes.ActualParticularCoherence.reference_cutoff_support
{B N0 : ℕ}
(l : Label B N0)
:
theorem
NavierStokes.ActualParticularCoherence.parameter_cutoff_smooth
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(n : ℕ)
:
ContDiff ℝ (↑⊤) ((ActualParticularStageControls.parameters x l).cutoff n)
theorem
NavierStokes.ActualParticularCoherence.parameter_cutoff_support
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(n : ℕ)
:
noncomputable def
NavierStokes.ActualParticularCoherence.source
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(j : ℤ)
(n : ℕ)
:
Source, constructed using ParticularWaveAssembly.residualSource.
Equations
- One or more equations did not get rendered due to their size.
Instances For
structure
NavierStokes.ActualParticularCoherence.PathRegular
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(j : ℤ)
(n : ℕ)
(p : PhysicalParticularWave.Parameter)
(Y : TorusInverse.Plane)
(copy : TorusInverse.Frequency)
:
Only finite path continuity of the actual input equation is required. There is no continuation in the clock variable in this record.
- coefficient : Continuous fun (s : ↑(Set.Icc 0 ((ActualParticularStageControls.parameters x l).length n))) => ((ActualParticularStageControls.parameters x l).tangent j n).linearData.coefficientAlong ((ActualParticularStageControls.parameters x l).geometry n) copy ((p, Y), ↑s)
- realForcing : Continuous fun (s : ↑(Set.Icc 0 ((ActualParticularStageControls.parameters x l).length n))) => (ParticularWaveBounds.realData ((ActualParticularStageControls.parameters x l).tangent j n) (source x l j n)).linearData.forcingAlong ((ActualParticularStageControls.parameters x l).geometry n) copy ((p, Y), ↑s)
- imagForcing : Continuous fun (s : ↑(Set.Icc 0 ((ActualParticularStageControls.parameters x l).length n))) => (ParticularWaveBounds.imagData ((ActualParticularStageControls.parameters x l).tangent j n) (source x l j n)).linearData.forcingAlong ((ActualParticularStageControls.parameters x l).geometry n) copy ((p, Y), ↑s)
Instances For
theorem
NavierStokes.ActualParticularCoherence.copy_amplitude_band
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
{V : Set TorusInverse.Plane}
(hV : IsOpen V)
(htime : ∀ s ∈ V, 0 < s.1)
(n m k : ℕ)
(hi :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m)
(hm :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2))
(HS : ActualReferenceRebase.StateComparison x V n m k)
(HB : ActualReferenceRebase.BlockComparison x l V n m k)
(j : ℤ)
(hKn : ↑j * (x.coefficients.blocks l).frequency n ≠ 0)
(hKm : ↑j * (x.coefficients.blocks l).frequency m ≠ 0)
(p : PhysicalParticularWave.Parameter)
(hp : p.2 ∈ V)
(Y : TorusInverse.Plane)
(copy : TorusInverse.Frequency)
(H :
PathRegular x l j m
(PhysicalParticularWave.parameterChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m)
p)
((CommonCoverSolve.coverPower k) Y) copy)
(hslot :
(((ActualParticularStageControls.parameters x l).geometry n).coordinates copy Y).2 ∈ Set.Icc 0 ((ActualParticularStageControls.parameters x l).length n))
:
ParticularWaveBounds.complexCopyVelocity ((ActualParticularStageControls.parameters x l).tangent j n) (source x l j n)
((ActualParticularStageControls.parameters x l).geometry n) ⋯ copy (p, Y) = PhysicalParticularWave.velocityWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m) • ParticularWaveBounds.complexCopyVelocity ((ActualParticularStageControls.parameters x l).tangent j m)
(source x l j m) ((ActualParticularStageControls.parameters x l).geometry m) ⋯ copy
(PhysicalParticularWave.parameterChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n)
(ChartScales.Q m) p, (CommonCoverSolve.coverPower k) Y)
theorem
NavierStokes.ActualParticularCoherence.common_amplitude_band
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
{V : Set TorusInverse.Plane}
(hV : IsOpen V)
(htime : ∀ s ∈ V, 0 < s.1)
(n m k : ℕ)
(hi :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m)
(hm :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2))
(HS : ActualReferenceRebase.StateComparison x V n m k)
(HB : ActualReferenceRebase.BlockComparison x l V n m k)
(j : ℤ)
(hKn : ↑j * (x.coefficients.blocks l).frequency n ≠ 0)
(hKm : ↑j * (x.coefficients.blocks l).frequency m ≠ 0)
(p : PhysicalParticularWave.Parameter)
(hp : p.2 ∈ V)
(Y : TorusInverse.Plane)
(H :
∀ (copy : TorusInverse.Frequency),
PathRegular x l j m
(PhysicalParticularWave.parameterChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n)
(ChartScales.Q m) p)
((CommonCoverSolve.coverPower k) Y) copy)
:
ParticularWaveBounds.commonVelocity ((ActualParticularStageControls.parameters x l).tangent j n) (source x l j n)
((ActualParticularStageControls.parameters x l).geometry n) ⋯
((ActualParticularStageControls.parameters x l).cutoff n) (p, Y) = PhysicalParticularWave.velocityWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m) • ParticularWaveBounds.commonVelocity ((ActualParticularStageControls.parameters x l).tangent j m) (source x l j m)
((ActualParticularStageControls.parameters x l).geometry m) ⋯
((ActualParticularStageControls.parameters x l).cutoff m)
(PhysicalParticularWave.parameterChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n)
(ChartScales.Q m) p, (CommonCoverSolve.coverPower k) Y)
theorem
NavierStokes.ActualParticularCoherence.common_pressure_band
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
{V : Set TorusInverse.Plane}
(hV : IsOpen V)
(htime : ∀ s ∈ V, 0 < s.1)
(n m k : ℕ)
(hi :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m)
(hm :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2))
(HS : ActualReferenceRebase.StateComparison x V n m k)
(HB : ActualReferenceRebase.BlockComparison x l V n m k)
(j : ℤ)
(hKn : ↑j * (x.coefficients.blocks l).frequency n ≠ 0)
(hKm : ↑j * (x.coefficients.blocks l).frequency m ≠ 0)
(p : PhysicalParticularWave.Parameter)
(hp : p.2 ∈ V)
(Y : TorusInverse.Plane)
(H :
∀ (copy : TorusInverse.Frequency),
PathRegular x l j m
(PhysicalParticularWave.parameterChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n)
(ChartScales.Q m) p)
((CommonCoverSolve.coverPower k) Y) copy)
:
ParticularWaveBounds.commonPressure ((ActualParticularStageControls.parameters x l).tangent j n) (source x l j n)
((ActualParticularStageControls.parameters x l).geometry n) ⋯
((ActualParticularStageControls.parameters x l).cutoff n) (↑j * (x.coefficients.blocks l).frequency n) (p, Y) = PhysicalParticularWave.pressureWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m) • ParticularWaveBounds.commonPressure ((ActualParticularStageControls.parameters x l).tangent j m) (source x l j m)
((ActualParticularStageControls.parameters x l).geometry m) ⋯
((ActualParticularStageControls.parameters x l).cutoff m) (↑j * (x.coefficients.blocks l).frequency m)
(PhysicalParticularWave.parameterChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n)
(ChartScales.Q m) p, (CommonCoverSolve.coverPower k) Y)
theorem
NavierStokes.ActualParticularCoherence.copy_cutoff_band
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(j : ℤ)
(n m k : ℕ)
(hi :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m)
(hm :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2))
(copy : TorusInverse.Frequency)
:
theorem
NavierStokes.ActualParticularCoherence.copy_cutoff_smooth
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(j : ℤ)
(n : ℕ)
(copy : TorusInverse.Frequency)
:
theorem
NavierStokes.ActualParticularCoherence.copy_derivative_slot
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(j : ℤ)
(n : ℕ)
(copy : TorusInverse.Frequency)
{z : PhysicalParticularWave.WaveSpace}
(hz : ActualParticularStageControls.directions.Dfast (fun (n : ℕ) => (copyData x l j).cutoff n copy) n z ≠ 0)
:
(((ActualParticularStageControls.parameters x l).geometry n).coordinates copy z.2).2 ∈ Set.Icc 0 ((ActualParticularStageControls.parameters x l).length n)
theorem
NavierStokes.ActualParticularCoherence.gaussian_band
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
{V : Set TorusInverse.Plane}
(hV : IsOpen V)
(htime : ∀ s ∈ V, 0 < s.1)
(n m k : ℕ)
(hi :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m)
(hm :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2))
(HS : ActualReferenceRebase.StateComparison x V n m k)
(HB : ActualReferenceRebase.BlockComparison x l V n m k)
(j : ℤ)
(hKn : ↑j * (x.coefficients.blocks l).frequency n ≠ 0)
(hKm : ↑j * (x.coefficients.blocks l).frequency m ≠ 0)
(z : PhysicalParticularWave.WaveSpace)
(hz : z.1.1.2 ∈ V)
(H :
∀ (copy : TorusInverse.Frequency),
PathRegular x l j m
(PhysicalParticularWave.parameterChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n)
(ChartScales.Q m) z.1.1)
((CommonCoverSolve.coverPower k) z.2) copy)
:
Actual finite-path inputs and zero source fibers #
structure
NavierStokes.ActualParticularCoherence.SourceInputs
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
:
Source inputs data, collecting continuous, supported, ordered.
- continuous (j : ℤ) (n : ℕ) (p : PhysicalParticularWave.Parameter) : p.2 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier → Continuous fun (Y : TorusInverse.Plane) => source x l j n (p, Y)
- ordered (j : ℤ) (n : ℕ) (p : PhysicalParticularWave.Parameter) : p.2 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier → ∀ (Y : TorusInverse.Plane), source x l j n (p, Y) ≠ 0 → CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2)
Instances For
theorem
NavierStokes.ActualParticularCoherence.SourceInputs.pathRegular
{B N0 : ℕ}
{x : CorrectionStep.CycleState (Label B N0)}
{l : Label B N0}
(I : SourceInputs x l)
(hfrequency :
∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n))
(j : ℤ)
(hj : j ≠ 0)
(n : ℕ)
(p : PhysicalParticularWave.Parameter)
(hp : p.2 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier)
(hne : ∃ (Y : TorusInverse.Plane), source x l j n (p, Y) ≠ 0)
(Y : TorusInverse.Plane)
(copy : TorusInverse.Frequency)
:
PathRegular x l j n p Y copy
theorem
NavierStokes.ActualParticularCoherence.copy_amplitude_zero
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(j : ℤ)
(n : ℕ)
(p : PhysicalParticularWave.Parameter)
(hz : ∀ (Y : TorusInverse.Plane), source x l j n (p, Y) = 0)
(theta : ℝ)
(Y : TorusInverse.Plane)
(copy : TorusInverse.Frequency)
:
theorem
NavierStokes.ActualParticularCoherence.raw_amplitude_zero
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(j : ℤ)
(n : ℕ)
(p : PhysicalParticularWave.Parameter)
(hz : ∀ (Y : TorusInverse.Plane), source x l j n (p, Y) = 0)
(theta : ℝ)
(Y : TorusInverse.Plane)
:
theorem
NavierStokes.ActualParticularCoherence.raw_pressure_zero
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(j : ℤ)
(n : ℕ)
(hKn : ↑j * (x.coefficients.blocks l).frequency n ≠ 0)
(p : PhysicalParticularWave.Parameter)
(hz : ∀ (Y : TorusInverse.Plane), source x l j n (p, Y) = 0)
(theta : ℝ)
(Y : TorusInverse.Plane)
:
theorem
NavierStokes.ActualParticularCoherence.gaussian_zero
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(j : ℤ)
(n : ℕ)
(p : PhysicalParticularWave.Parameter)
(hz : ∀ (Y : TorusInverse.Plane), source x l j n (p, Y) = 0)
(theta : ℝ)
(Y : TorusInverse.Plane)
:
theorem
NavierStokes.ActualParticularCoherence.raw_amplitude_band
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
{V : Set TorusInverse.Plane}
(hV : IsOpen V)
(htime : ∀ s ∈ V, 0 < s.1)
(n m k : ℕ)
(hi :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m)
(hm :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2))
(HS : ActualReferenceRebase.StateComparison x V n m k)
(HB : ActualReferenceRebase.BlockComparison x l V n m k)
(j : ℤ)
(hKn : ↑j * (x.coefficients.blocks l).frequency n ≠ 0)
(hKm : ↑j * (x.coefficients.blocks l).frequency m ≠ 0)
(z : PhysicalParticularWave.WaveSpace)
(hz : z.1.1.2 ∈ V)
(H :
∀ (copy : TorusInverse.Frequency),
PathRegular x l j m
(PhysicalParticularWave.parameterChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n)
(ChartScales.Q m) z.1.1)
((CommonCoverSolve.coverPower k) z.2) copy)
:
theorem
NavierStokes.ActualParticularCoherence.raw_pressure_band
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
{V : Set TorusInverse.Plane}
(hV : IsOpen V)
(htime : ∀ s ∈ V, 0 < s.1)
(n m k : ℕ)
(hi :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m)
(hm :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2))
(HS : ActualReferenceRebase.StateComparison x V n m k)
(HB : ActualReferenceRebase.BlockComparison x l V n m k)
(j : ℤ)
(hKn : ↑j * (x.coefficients.blocks l).frequency n ≠ 0)
(hKm : ↑j * (x.coefficients.blocks l).frequency m ≠ 0)
(z : PhysicalParticularWave.WaveSpace)
(hz : z.1.1.2 ∈ V)
(H :
∀ (copy : TorusInverse.Frequency),
PathRegular x l j m
(PhysicalParticularWave.parameterChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n)
(ChartScales.Q m) z.1.1)
((CommonCoverSolve.coverPower k) z.2) copy)
:
theorem
NavierStokes.ActualParticularCoherence.raw_outputs
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(I : SourceInputs x l)
(hfrequency :
∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n))
{V : Set TorusInverse.Plane}
(hV : IsOpen V)
(htime : ∀ s ∈ V, 0 < s.1)
(n m k : ℕ)
(hi :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m)
(HS : ActualReferenceRebase.StateComparison x V n m k)
(HB : ActualReferenceRebase.BlockComparison x l V n m k)
(j : ℤ)
(hj : j ≠ 0)
(z : PhysicalParticularWave.WaveSpace)
(hz : z.1.1.2 ∈ V)
(hmap :
(PhysicalParticularWave.parameterChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m)
z.1.1).2 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier)
:
(ActualReferenceRebase.actualCoefficients x l j).amplitude n z = PhysicalParticularWave.velocityWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m) • (ActualReferenceRebase.actualCoefficients x l j).amplitude m ((bandMap n m) z) ∧ (ActualReferenceRebase.actualCoefficients x l j).pressure n z = PhysicalParticularWave.pressureWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n)
(ChartScales.Q m) • (ActualReferenceRebase.actualCoefficients x l j).pressure m ((bandMap n m) z) ∧ (copyData x l j).globalGaussian ActualParticularStageControls.directions n z = PhysicalParticularWave.sourceWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m) • (copyData x l j).globalGaussian ActualParticularStageControls.directions m ((bandMap n m) z)
All three raw output identities are derived from the current source. A zero source fiber needs no ODE regularity or ordering premise.
Wave domain, given by {z | z.1.1.2 ∈ V}.
Equations
Instances For
theorem
NavierStokes.ActualParticularCoherence.waveDomain_open
{V : Set TorusInverse.Plane}
(hV : IsOpen V)
:
IsOpen (waveDomain V)
theorem
NavierStokes.ActualParticularCoherence.parameterChange_slow
(n m : ℕ)
(p : PhysicalParticularWave.Parameter)
:
theorem
NavierStokes.ActualParticularCoherence.phase_band
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
{V : Set TorusInverse.Plane}
(n m k : ℕ)
(hi :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m)
(HB : ActualReferenceRebase.BlockComparison x l V n m k)
(j : ℤ)
(hj : j ≠ 0)
(hn : (x.coefficients.blocks l).frequency n ≠ 0)
(hm : (x.coefficients.blocks l).frequency m ≠ 0)
(z : PhysicalParticularWave.WaveSpace)
(hz : z ∈ waveDomain V)
:
(ActualReferenceRebase.actualCoefficients x l j).phase n z = ↑j * (x.coefficients.blocks l).frequency m / (↑j * (x.coefficients.blocks l).frequency n) * (ActualReferenceRebase.actualCoefficients x l j).phase m ((bandMap n m) z)
theorem
NavierStokes.ActualParticularCoherence.corrected_amplitude_of_germs
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(j : ℤ)
(n m : ℕ)
(hKn : ↑j * (x.coefficients.blocks l).frequency n ≠ 0)
(hKm : ↑j * (x.coefficients.blocks l).frequency m ≠ 0)
(z : PhysicalParticularWave.WaveSpace)
(ha :
(ActualReferenceRebase.actualCoefficients x l j).amplitude n =ᶠ[nhds z] fun (y : PhysicalParticularWave.WaveSpace) =>
PhysicalParticularWave.velocityWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m) • (ActualReferenceRebase.actualCoefficients x l j).amplitude m ((bandMap n m) y))
(hp :
(ActualReferenceRebase.actualCoefficients x l j).phase n =ᶠ[nhds z] fun (y : PhysicalParticularWave.WaveSpace) =>
↑j * (x.coefficients.blocks l).frequency m / (↑j * (x.coefficients.blocks l).frequency n) * (ActualReferenceRebase.actualCoefficients x l j).phase m ((bandMap n m) y))
:
(corrected x l j).amplitude n z = PhysicalParticularWave.velocityWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m) • (corrected x l j).amplitude m ((bandMap n m) z)
theorem
NavierStokes.ActualParticularCoherence.corrected_amplitude_on
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Label B N0))
(l : Label B N0)
(I : SourceInputs x l)
(hfrequency :
∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n))
{V : Set TorusInverse.Plane}
(hV : IsOpen V)
(htime : ∀ s ∈ V, 0 < s.1)
(n m k : ℕ)
(hi :
CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m)
(hmap :
Set.MapsTo (⇑(GaugeStateCoherence.bandSlowEquiv CorrectionInitialization.ActualPrimary.h n m)) V
CorrectionInitialization.ActualPrimary.standardRegion.carrier)
(HS : ActualReferenceRebase.StateComparison x V n m k)
(HB : ActualReferenceRebase.BlockComparison x l V n m k)
(j : ℤ)
(hj : j ≠ 0)
(z : PhysicalParticularWave.WaveSpace)
(hz : z ∈ waveDomain V)
:
(corrected x l j).amplitude n z = PhysicalParticularWave.velocityWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m) • (corrected x l j).amplitude m ((bandMap n m) z)