Curl realization on native phase patches #
The geometric and tangency hypotheses are imposed only where the raw wave is used. The cutoff coefficient has a zero germ elsewhere in its copy cell. The actual common potential and corrected wave inherit the local curl and divergence identities through those germs.
theorem
NavierStokes.LocalizedCurlRealization.geometry_restrict
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{U V : Set D}
{R : D → ℝ}
{Vr Vθ Vz : D → D}
(G : CurlClassBounds.CylindricalGeometry U R Vr Vθ Vz)
(hV : IsOpen V)
(hVU : V ⊆ U)
:
CurlClassBounds.CylindricalGeometry V R Vr Vθ Vz
theorem
NavierStokes.LocalizedCurlRealization.normalDot_real_smul
(N : ProblemStatement.Space)
(r : ℝ)
(a : HarmonicCalculus.ComplexVector)
:
structure
NavierStokes.LocalizedCurlRealization.RawData
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(a : PeriodizedWaveBounds.CopyData D I)
(s : WeightedClasses.StripData D)
(d : LinearWaveBounds.GraphDirections D)
(C : ℕ → I → Set D)
:
Primitive smoothness, cylindrical geometry, and raw tangency on the genuine native phase patch. No corrected-wave equation is an input.
- geometry (n : ℕ) (i : I) : CurlClassBounds.CylindricalGeometry (s.domain ∩ C n i) (a.background.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n)
- tangent (n : ℕ) (i : I) (x : D) : x ∈ s.domain ∩ C n i → HarmonicCalculus.normalDot (a.background.normal s d n x) (a.amplitude n i x) = 0
Instances For
theorem
NavierStokes.LocalizedCurlRealization.RawData.of_localClasses
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : PeriodizedWaveBounds.CopyData D I}
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{C : ℕ → I → Set D}
{wa wψ : ℕ → I → D → ℝ}
{α β : ℝ}
(hG :
∀ (n : ℕ) (i : I),
CurlClassBounds.CylindricalGeometry (s.domain ∩ C n i) (a.background.radius n) (d.radialField n)
(fun (x : D) => d.angular) (d.axialField s n))
(hΦ : ∀ (n : ℕ) (i : I), ContDiffOn ℝ (↑⊤) (a.background.phase n) (s.domain ∩ C n i))
(ha : LocalizedWaveBounds.LocalClass s C wa α a.amplitude)
(hψ : LocalizedWaveBounds.LocalClass s C wψ β a.cutoff)
(hK : ∀ (n : ℕ), a.background.frequency n ≠ 0)
(hn : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain ∩ C n i, a.background.normal s d n x ≠ 0)
(ht :
∀ (n : ℕ) (i : I),
∀ x ∈ s.domain ∩ C n i, HarmonicCalculus.normalDot (a.background.normal s d n x) (a.amplitude n i x) = 0)
:
RawData a s d C
theorem
NavierStokes.LocalizedCurlRealization.RawData.localized_smooth
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : PeriodizedWaveBounds.CopyData D I}
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{C : ℕ → I → Set D}
(h : RawData a s d C)
(n : ℕ)
(i : I)
:
theorem
NavierStokes.LocalizedCurlRealization.RawData.localized_tangent
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : PeriodizedWaveBounds.CopyData D I}
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{C : ℕ → I → Set D}
(h : RawData a s d C)
(n : ℕ)
(i : I)
{x : D}
(hx : x ∈ s.domain ∩ C n i)
:
theorem
NavierStokes.LocalizedCurlRealization.RawData.native_potential_smooth
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : PeriodizedWaveBounds.CopyData D I}
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{C : ℕ → I → Set D}
(h : RawData a s d C)
(n : ℕ)
(i : I)
:
ContDiffOn ℝ (↑⊤) ((a.localized i).curlPotential s d n) (s.domain ∩ C n i)
theorem
NavierStokes.LocalizedCurlRealization.RawData.native_realizes_curl
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : PeriodizedWaveBounds.CopyData D I}
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{C : ℕ → I → Set D}
(h : RawData a s d C)
(n : ℕ)
(i : I)
{x : D}
(hx : x ∈ s.domain ∩ C n i)
:
CurlClassBounds.cylindricalCurl (a.background.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n)
((a.localized i).curlPotential s d n) x = HarmonicCalculus.vectorMode (a.background.frequency n) (a.background.phase n) ((a.corrected s d i).amplitude n) x
theorem
NavierStokes.LocalizedCurlRealization.RawData.native_divergence_zero
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : PeriodizedWaveBounds.CopyData D I}
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{C : ℕ → I → Set D}
(h : RawData a s d C)
(n : ℕ)
(i : I)
{x : D}
(hx : x ∈ s.domain ∩ C n i)
:
HarmonicCalculus.cylindricalDivergence (a.background.radius n) (d.radialField n) (fun (x : D) => d.angular)
(d.axialField s n)
(HarmonicCalculus.vectorMode (a.background.frequency n) (a.background.phase n) ((a.corrected s d i).amplitude n))
x = 0
theorem
NavierStokes.LocalizedCurlRealization.RawData.native_velocity_smooth
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : PeriodizedWaveBounds.CopyData D I}
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{C : ℕ → I → Set D}
(h : RawData a s d C)
(n : ℕ)
(i : I)
:
ContDiffOn ℝ (↑⊤)
(HarmonicCalculus.vectorMode (a.background.frequency n) (a.background.phase n) ((a.corrected s d i).amplitude n))
(s.domain ∩ C n i)
theorem
NavierStokes.LocalizedCurlRealization.native_zero_germs
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(a : PeriodizedWaveBounds.CopyData D I)
(s : WeightedClasses.StripData D)
(d : LinearWaveBounds.GraphDirections D)
{n : ℕ}
{i : I}
{x : D}
(ha : (a.localized i).amplitude n =ᶠ[nhds x] fun (x : D) => 0)
:
The whole native corrected field and its potential vanish as germs whenever the cutoff amplitude does. No background regularity is needed.
theorem
NavierStokes.LocalizedCurlRealization.native_identities_of_zero_germ
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(a : PeriodizedWaveBounds.CopyData D I)
(s : WeightedClasses.StripData D)
(d : LinearWaveBounds.GraphDirections D)
{n : ℕ}
{i : I}
{x : D}
(ha : (a.localized i).amplitude n =ᶠ[nhds x] fun (x : D) => 0)
:
CurlClassBounds.cylindricalCurl (a.background.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n)
((a.localized i).curlPotential s d n) x = HarmonicCalculus.vectorMode (a.background.frequency n) (a.background.phase n) ((a.corrected s d i).amplitude n) x ∧ HarmonicCalculus.cylindricalDivergence (a.background.radius n) (d.radialField n) (fun (x : D) => d.angular)
(d.axialField s n)
(HarmonicCalculus.vectorMode (a.background.frequency n) (a.background.phase n) ((a.corrected s d i).amplitude n))
x = 0
theorem
NavierStokes.LocalizedCurlRealization.RawData.common_realizes_curl
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : PeriodizedWaveBounds.CopyData D I}
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{C : ℕ → I → Set D}
(h : RawData a s d C)
(K : PeriodizedWaveBounds.Cells D I)
(hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i)
(hcover :
∀ (n : ℕ) (i : I),
∀ x ∈ s.domain, x ∈ K.carrier n i → x ∈ C n i ∨ (a.localized i).amplitude n =ᶠ[nhds x] fun (x : D) => 0)
(n : ℕ)
{x : D}
(hx : x ∈ s.domain)
:
CurlClassBounds.cylindricalCurl (a.background.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n)
(a.common.curlPotential s d n) x = HarmonicCalculus.vectorMode (a.background.frequency n) (a.background.phase n) ((a.commonCorrected s d).amplitude n) x
theorem
NavierStokes.LocalizedCurlRealization.RawData.common_divergence_zero
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : PeriodizedWaveBounds.CopyData D I}
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{C : ℕ → I → Set D}
(h : RawData a s d C)
(K : PeriodizedWaveBounds.Cells D I)
(hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i)
(hcover :
∀ (n : ℕ) (i : I),
∀ x ∈ s.domain, x ∈ K.carrier n i → x ∈ C n i ∨ (a.localized i).amplitude n =ᶠ[nhds x] fun (x : D) => 0)
(n : ℕ)
{x : D}
(hx : x ∈ s.domain)
:
HarmonicCalculus.cylindricalDivergence (a.background.radius n) (d.radialField n) (fun (x : D) => d.angular)
(d.axialField s n)
(HarmonicCalculus.vectorMode (a.background.frequency n) (a.background.phase n)
((a.commonCorrected s d).amplitude n))
x = 0
theorem
NavierStokes.LocalizedCurlRealization.RawData.common_potential_smooth
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : PeriodizedWaveBounds.CopyData D I}
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{C : ℕ → I → Set D}
(h : RawData a s d C)
(K : PeriodizedWaveBounds.Cells D I)
(hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i)
(hcover :
∀ (n : ℕ) (i : I),
∀ x ∈ s.domain, x ∈ K.carrier n i → x ∈ C n i ∨ (a.localized i).amplitude n =ᶠ[nhds x] fun (x : D) => 0)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) (a.common.curlPotential s d n) s.domain
theorem
NavierStokes.LocalizedCurlRealization.RawData.common_velocity_smooth
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : PeriodizedWaveBounds.CopyData D I}
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{C : ℕ → I → Set D}
(h : RawData a s d C)
(K : PeriodizedWaveBounds.Cells D I)
(hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i)
(hcover :
∀ (n : ℕ) (i : I),
∀ x ∈ s.domain, x ∈ K.carrier n i → x ∈ C n i ∨ (a.localized i).amplitude n =ᶠ[nhds x] fun (x : D) => 0)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤)
(HarmonicCalculus.vectorMode (a.background.frequency n) (a.background.phase n) ((a.commonCorrected s d).amplitude n))
s.domain
Tangency of the actual raw coefficients #
theorem
NavierStokes.LocalizedCurlRealization.signed_coefficients_tangent_at
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
(a : LinearWaveBounds.WaveCoefficients D)
(H : ℕ → D → SignedWaveUpdate.Mat2)
(T R : ℕ → D → SignedWaveUpdate.Vec2)
(mask : ℕ → D → ℝ)
(v Ndot : ℕ → D → ProblemStatement.Space)
(A : ℕ → D → ProblemStatement.Space →L[ℝ] ProblemStatement.Space)
(j : Fin 2)
(n : ℕ)
{x : D}
(ht : inner ℝ (a.normal s d n x) (v n x) = 0)
:
HarmonicCalculus.normalDot ((SignedWaveUpdate.coefficients a s d H T R mask v Ndot A j).normal s d n x)
((SignedWaveUpdate.coefficients a s d H T R mask v Ndot A j).amplitude n x) = 0
theorem
NavierStokes.LocalizedCurlRealization.complexCopyCoefficients_tangent_at
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{s : WeightedClasses.StripData (P × TorusInverse.Plane)}
{α : ℝ}
{dirs : LinearWaveBounds.GraphDirections (P × TorusInverse.Plane)}
{frame : ℕ → PrimaryODE.FrameData (P × ℝ)}
{t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space}
{source : ℕ → P × TorusInverse.Plane → HarmonicCalculus.ComplexVector}
{harmonic : ℤ}
{g : ℕ → CommonCoverSolve.Geometry}
{L : ℕ → ℝ}
{envelope : ℕ → ℝ → ℝ}
{C : ℕ → TorusInverse.Frequency → Set (P × TorusInverse.Plane)}
(base : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane))
(hL : ∀ (n : ℕ), 0 < L n)
(hr :
ParticularCopyBounds.ModalControl s α frame (fun (n : ℕ) => ParticularWaveBounds.realData (t n) (source n)) harmonic g
L envelope C)
(hi :
ParticularCopyBounds.ModalControl s α frame (fun (n : ℕ) => ParticularWaveBounds.imagData (t n) (source n)) harmonic g
L envelope C)
(n : ℕ)
(k : TorusInverse.Frequency)
{x : P × TorusInverse.Plane}
(hx : x ∈ s.domain)
(hk : x ∈ C n k)
(hN : base.normal s dirs n x = (t n).normal (ParticularWaveBounds.nativePoint (g n) k x))
:
HarmonicCalculus.normalDot (base.normal s dirs n x)
((ParticularWaveBounds.complexCopyCoefficients base t source g (fun (x : ℕ) => k) L hL).amplitude n x) = 0
The particular coefficient is tangent because each actual finite-path modal solve reconstructs into the tangent plane. Its two modal neighborhoods need not coincide, and no global modal control is used.