Concrete qualitative data for the actual correction waves #
All native data below use the initializer's existing choice. A common-band translation is interpreted on a native cover only when the common index is at most the native index. The inactive bands are handled using actual zero germs; no periodicity of an unused unmasked phase is imposed on those bands.
Qualitative regularity of the actual finite wave updates #
All regularity statements below use the full open slow domain. The quantitative strip is used only for its fixed differential operators. Native smoothness and genuine zero germs, rather than estimates on a smaller strip, supply the continuation away from the active phase patches.
noncomputable def
NavierStokes.ActualWaveRegularity.onDomain
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(s : WeightedClasses.StripData D)
(Ω : Set D)
(hΩ : IsOpen Ω)
:
A qualitative domain for the same operators. No quantitative bound is extended from the original strip.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ActualWaveRegularity.commonCorrected_onDomain
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(a : PeriodizedWaveBounds.CopyData D I)
(s : WeightedClasses.StripData D)
(d : LinearWaveBounds.GraphDirections D)
(Ω : Set D)
(hΩ : IsOpen Ω)
:
structure
NavierStokes.ActualWaveRegularity.NativeData
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(a : PeriodizedWaveBounds.CopyData D I)
(s : WeightedClasses.StripData D)
(d : LinearWaveBounds.GraphDirections D)
(Ω : Set D)
(hΩ : IsOpen Ω)
:
These are native, uncorrected data. In particular the smoothness of the common corrected velocity is a conclusion, not a field of this record.
- cells : PeriodizedWaveBounds.Cells D I
Cells of
NativeData, of typeCells D I. Patch of
NativeData, of typeℕ → I → Set D.- raw : LocalizedCurlRealization.RawData a (onDomain s Ω hΩ) d self.patch
Instances For
theorem
NavierStokes.ActualWaveRegularity.NativeData.common_velocity_smooth
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : PeriodizedWaveBounds.CopyData D I}
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{Ω : Set D}
{hΩ : IsOpen Ω}
(h : NativeData a s d Ω hΩ)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤)
(HarmonicCalculus.vectorMode (a.background.frequency n) (a.background.phase n) ((a.commonCorrected s d).amplitude n))
Ω
theorem
NavierStokes.ActualWaveRegularity.NativeData.common_potential_smooth
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : PeriodizedWaveBounds.CopyData D I}
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{Ω : Set D}
{hΩ : IsOpen Ω}
(h : NativeData a s d Ω hΩ)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) (a.common.curlPotential s d n) Ω
theorem
NavierStokes.ActualWaveRegularity.NativeData.glue_smooth
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : PeriodizedWaveBounds.CopyData D I}
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{Ω : Set D}
{hΩ : IsOpen Ω}
(h : NativeData a s d Ω hΩ)
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(F : ℕ → D → E)
(f : ℕ → I → D → E)
(hg : ∀ (n : ℕ) (i : I), ∀ x ∈ h.cells.carrier n i, F n =ᶠ[nhds x] f n i)
(hz : ∀ (n : ℕ) (x : D), (∀ (i : I), x ∉ h.cells.carrier n i) → F n =ᶠ[nhds x] fun (x : D) => 0)
(hs : ∀ (n : ℕ) (i : I), ContDiffOn ℝ (↑⊤) (f n i) (Ω ∩ h.patch n i))
(hflat :
∀ (n : ℕ) (i : I) (x : D),
((a.localized i).amplitude n =ᶠ[nhds x] fun (x : D) => 0) → f n i =ᶠ[nhds x] fun (x : D) => 0)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) (F n) Ω
theorem
NavierStokes.ActualWaveRegularity.NativeData.common_raw_smooth
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : PeriodizedWaveBounds.CopyData D I}
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{Ω : Set D}
{hΩ : IsOpen Ω}
(h : NativeData a s d Ω hΩ)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) (a.common.amplitude n) Ω
theorem
NavierStokes.ActualWaveRegularity.NativeData.native_normal_smooth
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : PeriodizedWaveBounds.CopyData D I}
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{Ω : Set D}
{hΩ : IsOpen Ω}
(h : NativeData a s d Ω hΩ)
(n : ℕ)
(i : I)
:
ContDiffOn ℝ (↑⊤)
(CurlClassBounds.coefficient (a.background.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n)
(a.background.phase n) ((a.localized i).amplitude n))
(Ω ∩ h.patch n i)
theorem
NavierStokes.ActualWaveRegularity.NativeData.common_normal_smooth
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : PeriodizedWaveBounds.CopyData D I}
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{Ω : Set D}
{hΩ : IsOpen Ω}
(h : NativeData a s d Ω hΩ)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤)
(CurlClassBounds.coefficient (a.background.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n)
(a.background.phase n) (a.common.amplitude n))
Ω
The actual normalized vector-potential coefficient has a smooth zero extension too; smoothness of the bare phase normal off support is not used.
theorem
NavierStokes.ActualWaveRegularity.NativeData.native_corrected_smooth
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : PeriodizedWaveBounds.CopyData D I}
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{Ω : Set D}
{hΩ : IsOpen Ω}
(h : NativeData a s d Ω hΩ)
(n : ℕ)
(i : I)
:
theorem
NavierStokes.ActualWaveRegularity.NativeData.common_corrected_smooth
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : PeriodizedWaveBounds.CopyData D I}
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{Ω : Set D}
{hΩ : IsOpen Ω}
(h : NativeData a s d Ω hΩ)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) ((a.commonCorrected s d).amplitude n) Ω
theorem
NavierStokes.ActualWaveRegularity.NativeData.common_zero_germ
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : PeriodizedWaveBounds.CopyData D I}
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{Ω : Set D}
{hΩ : IsOpen Ω}
(h : NativeData a s d Ω hΩ)
{n : ℕ}
{x : D}
(hz : ∀ (i : I), x ∈ h.cells.carrier n i → (a.localized i).amplitude n =ᶠ[nhds x] fun (x : D) => 0)
:
Locally finite native zero germs give a zero germ for the common corrected amplitude, even if the phase or normal is singular at this point.
theorem
NavierStokes.ActualWaveRegularity.NativeData.common_velocity_zero_germ
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : PeriodizedWaveBounds.CopyData D I}
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{Ω : Set D}
{hΩ : IsOpen Ω}
(h : NativeData a s d Ω hΩ)
{n : ℕ}
{x : D}
(hz : ∀ (i : I), x ∈ h.cells.carrier n i → (a.localized i).amplitude n =ᶠ[nhds x] fun (x : D) => 0)
:
HarmonicCalculus.vectorMode (a.background.frequency n) (a.background.phase n)
((a.commonCorrected s d).amplitude n) =ᶠ[nhds x] fun (x : D) => 0
Discrete translations on an open domain #
Unlike global translation identities, these statements only require the actual fields on the physical slow domain. Derivatives are genuine Fréchet derivatives, transferred through an open neighborhood.
noncomputable def
NavierStokes.ActualWaveRegularity.TranslationOn
{D : Type}
[NormedAddCommGroup D]
{E : Type}
(Ω : Set D)
(z : D)
(f : D → E)
:
Translation on, given by ∀ x ∈ Ω, f (x + z) = f x.
Equations
- NavierStokes.ActualWaveRegularity.TranslationOn Ω z f = ∀ x ∈ Ω, f (x + z) = f x
Instances For
theorem
NavierStokes.ActualWaveRegularity.TranslationOn.const
{D : Type}
[NormedAddCommGroup D]
{E : Type}
{Ω : Set D}
{z : D}
(c : E)
:
TranslationOn Ω z fun (x : D) => c
theorem
NavierStokes.ActualWaveRegularity.TranslationOn.map
{D : Type}
[NormedAddCommGroup D]
{E F : Type}
{Ω : Set D}
{z : D}
{f : D → E}
(hf : TranslationOn Ω z f)
(T : E → F)
:
TranslationOn Ω z fun (x : D) => T (f x)
theorem
NavierStokes.ActualWaveRegularity.TranslationOn.map₂
{D : Type}
[NormedAddCommGroup D]
{E F G : Type}
{Ω : Set D}
{z : D}
{f : D → E}
{g : D → F}
(hf : TranslationOn Ω z f)
(hg : TranslationOn Ω z g)
(T : E → F → G)
:
TranslationOn Ω z fun (x : D) => T (f x) (g x)
theorem
NavierStokes.ActualWaveRegularity.TranslationOn.component
{D : Type}
[NormedAddCommGroup D]
{Ω : Set D}
{z : D}
{ι : Type}
{F : ι → Type}
{f : D → (i : ι) → F i}
(hf : TranslationOn Ω z f)
(i : ι)
:
TranslationOn Ω z fun (x : D) => f x i
theorem
NavierStokes.ActualWaveRegularity.TranslationOn.fderiv
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{E : Type}
{Ω : Set D}
{z : D}
{f : D → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(hf : TranslationOn Ω z f)
(hΩ : IsOpen Ω)
:
TranslationOn Ω z (_root_.fderiv ℝ f)
theorem
NavierStokes.ActualWaveRegularity.TranslationOn.along
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{E : Type}
{Ω : Set D}
{z : D}
{f : D → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{V : D → D}
(hf : TranslationOn Ω z f)
(hV : TranslationOn Ω z V)
(hΩ : IsOpen Ω)
:
TranslationOn Ω z (HarmonicCalculus.along V f)
theorem
NavierStokes.ActualWaveRegularity.phaseNormal_translation
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{Ω : Set D}
{z : D}
(hΩ : IsOpen Ω)
{R Φ : D → ℝ}
{Vr Vθ Vz : D → D}
(hR : TranslationOn Ω z R)
(hr : TranslationOn Ω z Vr)
(hθ : TranslationOn Ω z Vθ)
(hz : TranslationOn Ω z Vz)
(hΦ : TranslationOn Ω z Φ)
:
TranslationOn Ω z (HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ)
theorem
NavierStokes.ActualWaveRegularity.cylindricalCurl_translation
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{Ω : Set D}
{z : D}
(hΩ : IsOpen Ω)
{R : D → ℝ}
{Vr Vθ Vz : D → D}
{a : D → HarmonicCalculus.ComplexVector}
(hR : TranslationOn Ω z R)
(hr : TranslationOn Ω z Vr)
(hθ : TranslationOn Ω z Vθ)
(hz : TranslationOn Ω z Vz)
(ha : TranslationOn Ω z a)
:
TranslationOn Ω z (CurlClassBounds.cylindricalCurl R Vr Vθ Vz a)
theorem
NavierStokes.ActualWaveRegularity.common_amplitude_translation
{D I : Type}
[NormedAddCommGroup D]
(a : PeriodizedWaveBounds.CopyData D I)
{Ω : Set D}
{z : D}
(n : ℕ)
(e : I ≃ I)
(hψ : ∀ (i : I), ∀ x ∈ Ω, a.cutoff n (e i) (x + z) = a.cutoff n i x)
(ha : ∀ (i : I), ∀ x ∈ Ω, a.amplitude n (e i) (x + z) = a.amplitude n i x)
:
TranslationOn Ω z (a.common.amplitude n)
theorem
NavierStokes.ActualWaveRegularity.commonCorrected_translation
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(a : PeriodizedWaveBounds.CopyData D I)
(s : WeightedClasses.StripData D)
(d : LinearWaveBounds.GraphDirections D)
{Ω : Set D}
{z : D}
(hΩ : IsOpen Ω)
(n : ℕ)
(hR : TranslationOn Ω z (a.background.radius n))
(hr : TranslationOn Ω z (d.radialField n))
(hΦ : TranslationOn Ω z (a.background.phase n))
(ha : TranslationOn Ω z (a.common.amplitude n))
:
TranslationOn Ω z ((a.commonCorrected s d).amplitude n)
theorem
NavierStokes.ActualWaveRegularity.common_velocity_translation
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(a : PeriodizedWaveBounds.CopyData D I)
(s : WeightedClasses.StripData D)
(d : LinearWaveBounds.GraphDirections D)
{Ω : Set D}
{z : D}
(hΩ : IsOpen Ω)
(n : ℕ)
(hR : TranslationOn Ω z (a.background.radius n))
(hr : TranslationOn Ω z (d.radialField n))
(hΦ : TranslationOn Ω z (a.background.phase n))
(ha : TranslationOn Ω z (a.common.amplitude n))
:
TranslationOn Ω z
(HarmonicCalculus.vectorMode (a.background.frequency n) (a.background.phase n) ((a.commonCorrected s d).amplitude n))
Qualitative regularity of the literal native solves #
structure
NavierStokes.ActualWaveRegularity.ModalSmooth
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
(t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space)
(harmonic : ℤ)
(g : ℕ → CommonCoverSolve.Geometry)
(L : ℕ → ℝ)
(Ω : Set (P × TorusInverse.Plane))
(C : ℕ → TorusInverse.Frequency → Set (P × TorusInverse.Plane))
:
Primitive smooth coefficient, forcing, and synthesis columns on a neighborhood of each entire Volterra path. No solved field occurs here.
- frame : ℕ → PrimaryODE.FrameData (P × ℝ)
Frame of
ModalSmooth, of typeℕ → PrimaryODE.FrameData (P × ℝ). - neighborhood : ℕ → TorusInverse.Frequency → Set (P × TorusInverse.Plane)
Neighborhood of
ModalSmooth, of typeℕ → Frequency → Set (P × Plane). Interval of
ModalSmooth, of typeℕ → Set ℝ.- bridge (n : ℕ) (k : PrimaryCopyBridge.Frequency) : PrimaryCopyBridge.Inputs (self.frame n) (t n) harmonic (g n) k (self.neighborhood n k) 0 (L n)
- coefficient (n : ℕ) (k : PrimaryCopyBridge.Frequency) : ContDiffOn ℝ (↑⊤) ((PrimaryCopyBridge.copyFrame (self.frame n) (g n) k).coefficient harmonic) (self.neighborhood n k ×ˢ self.interval n)
- forcing (n : ℕ) (k : PrimaryCopyBridge.Frequency) : ContDiffOn ℝ (↑⊤) ((PrimaryCopyBridge.copyFrame (self.frame n) (g n) k).forcing (PrimaryCopyBridge.copySource (t n).source (g n) k)) (self.neighborhood n k ×ˢ self.interval n)
- columns (n : ℕ) (k : PrimaryCopyBridge.Frequency) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (PrimaryPulseBounds.synthesisColumn (PrimaryCopyBridge.copyFrame (self.frame n) (g n) k) i) (self.neighborhood n k ×ˢ self.interval n)
- current_slot (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) : x ∈ self.neighborhood n k → ((g n).coordinates k x.2).2 ∈ Set.Ioo 0 (L n)
Instances For
theorem
NavierStokes.ActualWaveRegularity.ModalSmooth.copySolve_smooth
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space}
{harmonic : ℤ}
{g : ℕ → CommonCoverSolve.Geometry}
{L : ℕ → ℝ}
{Ω : Set (P × TorusInverse.Plane)}
{C : ℕ → TorusInverse.Frequency → Set (P × TorusInverse.Plane)}
(h : ModalSmooth t harmonic g L Ω C)
(hL : ∀ (n : ℕ), 0 < L n)
(n : ℕ)
(k : TorusInverse.Frequency)
:
ContDiffOn ℝ (↑⊤) ((t n).linearData.copySolve (g n) ⋯ k) (Ω ∩ C n k)
theorem
NavierStokes.ActualWaveRegularity.complexCopy_smooth
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space}
{source : ℕ → P × TorusInverse.Plane → HarmonicCalculus.ComplexVector}
{harmonic : ℤ}
{g : ℕ → CommonCoverSolve.Geometry}
{L : ℕ → ℝ}
{Ω : Set (P × TorusInverse.Plane)}
{C : ℕ → TorusInverse.Frequency → Set (P × TorusInverse.Plane)}
(hr : ModalSmooth (fun (n : ℕ) => ParticularWaveBounds.realData (t n) (source n)) harmonic g L Ω C)
(hi : ModalSmooth (fun (n : ℕ) => ParticularWaveBounds.imagData (t n) (source n)) harmonic g L Ω C)
(hL : ∀ (n : ℕ), 0 < L n)
(n : ℕ)
(k : TorusInverse.Frequency)
:
ContDiffOn ℝ (↑⊤) (ParticularWaveBounds.complexCopyVelocity (t n) (source n) (g n) ⋯ k) (Ω ∩ C n k)
theorem
NavierStokes.ActualWaveRegularity.signed_coefficients_smooth
{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 : ℕ)
{Ω : Set D}
(hH : ∀ (i j : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : D) => H n x i j) Ω)
(hT : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : D) => T n x i) Ω)
(hR : ∀ (i : Fin 2), ContDiffOn ℝ (↑⊤) (fun (x : D) => R n x i) Ω)
(hm : ContDiffOn ℝ (↑⊤) (mask n) Ω)
(hv : ContDiffOn ℝ (↑⊤) (v n) Ω)
(hc : ∀ x ∈ Ω, SmoothCovariance.StrictCone (H n x) (T n x))
:
ContDiffOn ℝ (↑⊤) ((SignedWaveUpdate.coefficients a s d H T R mask v Ndot A j).amplitude n) Ω
The actual signed quotient is smooth from its matrix, target, request, mask and homogeneous fundamental, on the strict covariance cone.
One actual mode on the full physical slow domain #
@[reducible, inline]
Point: an abbreviation for CorrectionStep.CyclePoint.
Instances For
noncomputable def
NavierStokes.ActualWaveRegularity.fullDomain
{coord : ℝ}
(U : LocalSignedRequest.SlowRegion coord)
:
Full domain, given by HarmonicResidual.liftDomain (PhysicalMeanDomain.slowDomain U.carrier).
Equations
Instances For
theorem
NavierStokes.ActualWaveRegularity.fullDomain_open
{coord : ℝ}
(U : LocalSignedRequest.SlowRegion coord)
:
IsOpen (fullDomain U)
noncomputable def
NavierStokes.ActualWaveRegularity.nativeDomain
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{coord : ℝ}
(e : Cylinder ≃ₗᵢ[ℝ] D)
(U : LocalSignedRequest.SlowRegion coord)
:
Set D
Native domain, given by e.symm ⁻¹' fullDomain U.
Equations
Instances For
theorem
NavierStokes.ActualWaveRegularity.nativeDomain_open
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{coord : ℝ}
(e : Cylinder ≃ₗᵢ[ℝ] D)
(U : LocalSignedRequest.SlowRegion coord)
:
IsOpen (nativeDomain e U)
Deck shift, given by ((0, (0, ((k.1 : ℝ), (k.2 : ℝ)))), 0).
Instances For
noncomputable def
NavierStokes.ActualWaveRegularity.modeOscillation
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(a : PeriodizedWaveBounds.CopyData D I)
(s : WeightedClasses.StripData D)
(d : LinearWaveBounds.GraphDirections D)
(e : Cylinder ≃ₗᵢ[ℝ] D)
:
Mode oscillation, defined pointwise by (vectorMode (a.background.frequency n) (a.background.phase n) ((a.commonCorrected s d).amplitude n) (e x) i).re.
Equations
- One or more equations did not get rendered due to their size.
Instances For
structure
NavierStokes.ActualWaveRegularity.ModeData
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(a : PeriodizedWaveBounds.CopyData D I)
(s : WeightedClasses.StripData D)
(d : LinearWaveBounds.GraphDirections D)
(e : Cylinder ≃ₗᵢ[ℝ] D)
{coord : ℝ}
(U : LocalSignedRequest.SlowRegion coord)
(r₀ r₁ : ℝ)
:
Primitive continuation and deck identities for one mode. All spatial smoothness is confined to the genuine native patches. Radial support is proved using localized raw-amplitude zero germs.
- native : NativeData a s d (nativeDomain e U) ⋯
Native of
ModeData, of typeNativeData a s d (nativeDomain e U) (nativeDomain_open e U). - reindex : ℕ → TorusInverse.Frequency → I ≃ I
Reindex of
ModeData, of typeℕ → TorusInverse.Frequency → I ≃ I. - cutoff_deck (n : ℕ) (k : TorusInverse.Frequency) (i : I) (x : D) : x ∈ nativeDomain e U → a.cutoff n ((self.reindex n k) i) (x + e (deckShift k)) = a.cutoff n i x
- amplitude_deck (n : ℕ) (k : TorusInverse.Frequency) (i : I) (x : D) : x ∈ nativeDomain e U → a.amplitude n ((self.reindex n k) i) (x + e (deckShift k)) = a.amplitude n i x
- radius_deck (n : ℕ) (k : TorusInverse.Frequency) : TranslationOn (nativeDomain e U) (e (deckShift k)) (a.background.radius n)
- radial_deck (n : ℕ) (k : TorusInverse.Frequency) : TranslationOn (nativeDomain e U) (e (deckShift k)) (d.radialField n)
- phase_deck (n : ℕ) (k : TorusInverse.Frequency) : TranslationOn (nativeDomain e U) (e (deckShift k)) (a.background.phase n)
Instances For
theorem
NavierStokes.ActualWaveRegularity.ModeData.smooth
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : PeriodizedWaveBounds.CopyData D I}
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{e : Cylinder ≃ₗᵢ[ℝ] D}
{coord r₀ r₁ : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
(h : ModeData a s d e U r₀ r₁)
:
theorem
NavierStokes.ActualWaveRegularity.ModeData.periodic
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : PeriodizedWaveBounds.CopyData D I}
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{e : Cylinder ≃ₗᵢ[ℝ] D}
{coord r₀ r₁ : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
(h : ModeData a s d e U r₀ r₁)
:
CorrectionStep.OscillationPeriodic U.carrier (modeOscillation a s d e)
theorem
NavierStokes.ActualWaveRegularity.ModeData.support
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : PeriodizedWaveBounds.CopyData D I}
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{e : Cylinder ≃ₗᵢ[ℝ] D}
{coord r₀ r₁ : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
(h : ModeData a s d e U r₀ r₁)
:
WaveStateRegularity.WaveSupport U r₀ r₁ (modeOscillation a s d e)
theorem
NavierStokes.ActualWaveRegularity.ModeData.regular
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : PeriodizedWaveBounds.CopyData D I}
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{e : Cylinder ≃ₗᵢ[ℝ] D}
{coord r₀ r₁ : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
(h : ModeData a s d e U r₀ r₁)
:
WaveStateRegularity.AngularSmooth (PhysicalMeanDomain.slowDomain U.carrier) (modeOscillation a s d e) ∧ CorrectionStep.OscillationPeriodic U.carrier (modeOscillation a s d e) ∧ WaveStateRegularity.WaveSupport U r₀ r₁ (modeOscillation a s d e)
Finite sums retain the whole-domain conclusions #
theorem
NavierStokes.ActualWaveRegularity.finite_smooth
{ι : Type}
{Ω : Set Point}
(labels : ℕ → Finset ι)
(u : ι → CorrectionState.Oscillation Point)
(hs : ∀ (l : ι), WaveStateRegularity.AngularSmooth Ω (u l))
:
WaveStateRegularity.AngularSmooth Ω (LabelSumBounds.fieldSum labels u)
theorem
NavierStokes.ActualWaveRegularity.finite_periodic
{ι : Type}
{U : Set TorusInverse.Plane}
(labels : ℕ → Finset ι)
(u : ι → CorrectionState.Oscillation Point)
(hp : ∀ (l : ι), CorrectionStep.OscillationPeriodic U (u l))
:
theorem
NavierStokes.ActualWaveRegularity.finite_support
{ι : Type}
{coord r₀ r₁ : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
(labels : ℕ → Finset ι)
(u : ι → CorrectionState.Oscillation Point)
(hs : ∀ (l : ι), WaveStateRegularity.WaveSupport U r₀ r₁ (u l))
:
WaveStateRegularity.WaveSupport U r₀ r₁ (LabelSumBounds.fieldSum labels u)
theorem
NavierStokes.ActualWaveRegularity.finset_regular
{ι : Type}
{coord r₀ r₁ : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
(t : Finset ι)
(u : ι → CorrectionState.Oscillation Point)
(h :
∀ l ∈ t,
WaveStateRegularity.AngularSmooth (PhysicalMeanDomain.slowDomain U.carrier) (u l) ∧ CorrectionStep.OscillationPeriodic U.carrier (u l) ∧ WaveStateRegularity.WaveSupport U r₀ r₁ (u l))
:
WaveStateRegularity.AngularSmooth (PhysicalMeanDomain.slowDomain U.carrier)
(LabelSumBounds.fieldSum (fun (x : ℕ) => t) u) ∧ CorrectionStep.OscillationPeriodic U.carrier (LabelSumBounds.fieldSum (fun (x : ℕ) => t) u) ∧ WaveStateRegularity.WaveSupport U r₀ r₁ (LabelSumBounds.fieldSum (fun (x : ℕ) => t) u)
The literal particular update of the cycle #
@[reducible, inline]
Particular space: an abbreviation for (CycleSlow × ℝ) × TorusInverse.Plane.
Equations
Instances For
Particular chart, given by (StateReindex.cylinder cycleAssoc).trans angleShuffle.
Equations
Instances For
noncomputable def
NavierStokes.ActualWaveRegularity.particularStrip
{ι : Type}
(p : CorrectionStep.CycleParameters ι)
:
Particular strip, given by ParticularParameters.nativeStrip (reindexStrip cycleAssoc.symm p.strip).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.ActualWaveRegularity.particularCopyData
{ι : Type}
(p : CorrectionStep.CycleParameters ι)
(v : CorrectionStep.CycleCoefficients ι)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(l : ι)
(j : ℤ)
:
Particular copy data as an element of CopyData ParticularSpace TorusInverse.Frequency.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ActualWaveRegularity.particular_amplitude_deck
{ι : Type}
(p : CorrectionStep.CycleParameters ι)
(v : CorrectionStep.CycleCoefficients ι)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(l : ι)
(j : ℤ)
(n : ℕ)
(k m : TorusInverse.Frequency)
(x : ParticularSpace)
(hp : CommonCoverSolve.PeriodicAt ((particularCopyData p v c u l j).source n) x.1)
:
(particularCopyData p v c u l j).amplitude n (k + CommonCoverSolve.coverIndex ((p.particular l).geometry n).gap m)
(x.1, x.2 + TorusAverages.latticePoint m) = (particularCopyData p v c u l j).amplitude n k x
Deck covariance of the actual Volterra coefficient follows from periodicity of its incoming residual coefficient, with the same anchor.
theorem
NavierStokes.ActualWaveRegularity.particular_cutoff_deck
{ι : Type}
(p : CorrectionStep.CycleParameters ι)
(v : CorrectionStep.CycleCoefficients ι)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(l : ι)
(j : ℤ)
(n : ℕ)
(k m : TorusInverse.Frequency)
(x : ParticularSpace)
:
(particularCopyData p v c u l j).cutoff n (k + CommonCoverSolve.coverIndex ((p.particular l).geometry n).gap m)
(x.1, x.2 + TorusAverages.latticePoint m) = (particularCopyData p v c u l j).cutoff n k x
theorem
NavierStokes.ActualWaveRegularity.particularBlock_eq_modes
{ι : Type}
(p : CorrectionStep.CycleParameters ι)
(v : CorrectionStep.CycleCoefficients ι)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(l : ι)
(hR : ∀ (n : ℕ), CopyAngularInvariance.Invariant ((0, 1), 0) ((p.particular l).background.radius n))
(hr : ∀ (n : ℕ), CopyAngularInvariance.Invariant ((0, 1), 0) ((p.particular l).directions.radialField n))
(hf : ∀ (n : ℕ), (v.blocks l).frequency n ≠ 0)
:
(p.particularBlock v c u l).oscillation = LabelSumBounds.fieldSum (fun (x : ℕ) => ParticularWaveAssembly.modes v.residualBand) fun (j : ℤ) =>
modeOscillation (particularCopyData p v c u l j) (particularStrip p) (p.particular l).directions particularChart
This representation is derived from the actual angle-lifted Volterra solve and the original carrier. No equality of completed output fields is an assumption.
structure
NavierStokes.ActualWaveRegularity.ParticularData
{ι : Type}
(p : CorrectionStep.CycleParameters ι)
(v : CorrectionStep.CycleCoefficients ι)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
{coord : ℝ}
(U : LocalSignedRequest.SlowRegion coord)
(r₀ r₁ : ℝ)
:
Full-domain native inputs for the same particular copies and the same
incoming residual data used by CycleParameters.particularBlock.
- mode (l : ι) (j : ℤ) : j ∈ ParticularWaveAssembly.modes v.residualBand → ModeData (particularCopyData p v c u l j) (particularStrip p) (p.particular l).directions particularChart U r₀ r₁
Mode supplied by
ParticularData. - radius_angular (l : ι) (n : ℕ) : CopyAngularInvariance.Invariant ((0, 1), 0) ((p.particular l).background.radius n)
- radial_angular (l : ι) (n : ℕ) : CopyAngularInvariance.Invariant ((0, 1), 0) ((p.particular l).directions.radialField n)
Instances For
theorem
NavierStokes.ActualWaveRegularity.ParticularData.block_regular
{ι : Type}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
{coord r₀ r₁ : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
(h : ParticularData p v c u U r₀ r₁)
(l : ι)
:
WaveStateRegularity.AngularSmooth (PhysicalMeanDomain.slowDomain U.carrier) (p.particularBlock v c u l).oscillation ∧ CorrectionStep.OscillationPeriodic U.carrier (p.particularBlock v c u l).oscillation ∧ WaveStateRegularity.WaveSupport U r₀ r₁ (p.particularBlock v c u l).oscillation
theorem
NavierStokes.ActualWaveRegularity.ParticularData.regular
{ι : Type}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
{coord r₀ r₁ : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
(h : ParticularData p v c u U r₀ r₁)
:
WaveStateRegularity.AngularSmooth (PhysicalMeanDomain.slowDomain U.carrier) (p.particularVelocity v c u) ∧ CorrectionStep.OscillationPeriodic U.carrier (p.particularVelocity v c u) ∧ WaveStateRegularity.WaveSupport U r₀ r₁ (p.particularVelocity v c u)
The literal signed update, using the post-particular request #
theorem
NavierStokes.ActualWaveRegularity.signed_amplitude_deck
{I : Type}
(p : CorrectionStep.PeriodizedSignedParameters Point I)
(s : WeightedClasses.StripData Point)
(request : ℕ → Cylinder → SignedWaveUpdate.Vec2)
(n : ℕ)
(i j : I)
(x z : Cylinder)
(hH : p.matrix j n (x + z) = p.matrix i n x)
(hT : p.target j n (x + z) = p.target i n x)
(hR : request n (x + z) = request n x)
(hm : p.mask j n (x + z) = p.mask i n x)
(hv : p.fundamental j n (x + z) = p.fundamental i n x)
:
The native signed coefficient inherits a deck identity from the literal matrix, targets, mask, and homogeneous fundamental.
structure
NavierStokes.ActualWaveRegularity.SignedAngles
{I : Type}
(p : CorrectionStep.PeriodizedSignedParameters Point I)
(s : WeightedClasses.StripData Point)
(request : ℕ → Cylinder → SignedWaveUpdate.Vec2)
:
Angular identities of the primitive signed inputs. No identity of the corrected field, and no regularity away from the native support, is assumed.
Slope of
SignedAngles, of typeℕ → ℝ.- radial (n : ℕ) : CopyAngularInvariance.Invariant (0, 1) (p.directions.radialField n)
- request (n : ℕ) : CopyAngularInvariance.Invariant (0, 1) (request n)
Instances For
theorem
NavierStokes.ActualWaveRegularity.SignedAngles.raw_invariant
{I : Type}
{p : CorrectionStep.PeriodizedSignedParameters Point I}
{s : WeightedClasses.StripData Point}
{request : ℕ → Cylinder → SignedWaveUpdate.Vec2}
(h : SignedAngles p s request)
(n : ℕ)
(i : I)
:
theorem
NavierStokes.ActualWaveRegularity.SignedAngles.corrected_invariant
{I : Type}
{p : CorrectionStep.PeriodizedSignedParameters Point I}
{s : WeightedClasses.StripData Point}
{request : ℕ → Cylinder → SignedWaveUpdate.Vec2}
(h : SignedAngles p s request)
(n : ℕ)
:
CopyAngularInvariance.Invariant (0, 1)
(((p.copyData s request).commonCorrected (HarmonicWaveInteraction.productStrip s) p.directions).amplitude n)
theorem
NavierStokes.ActualWaveRegularity.SignedAngles.block_eq_mode
{I : Type}
{p : CorrectionStep.PeriodizedSignedParameters Point I}
{s : WeightedClasses.StripData Point}
{request : ℕ → Cylinder → SignedWaveUpdate.Vec2}
(h : SignedAngles p s request)
:
(p.exactBlock s request).oscillation = modeOscillation (p.copyData s request) (HarmonicWaveInteraction.productStrip s) p.directions
(LinearIsometryEquiv.refl ℝ Cylinder)
noncomputable def
NavierStokes.ActualWaveRegularity.signedAnglesOfInputs
{I : Type}
(p : CorrectionStep.PeriodizedSignedParameters Point I)
(s : WeightedClasses.StripData Point)
(request : ℕ → Cylinder → SignedWaveUpdate.Vec2)
(m : ℕ → ℝ)
(i₀ : I)
(hθ : p.directions.angular = (0, 1))
(hf : ∀ (n : ℕ), p.base.frequency n * m n = ↑(p.angularFrequency n))
(h :
∀ (i : I),
SignedWaveUpdate.AngularInputs (HarmonicWaveInteraction.productStrip s) p.directions p.base (p.matrix i)
(p.target i) request (p.mask i) (p.fundamental i) (p.normalMotion i) (p.action i) (p.cutoff i) m)
:
SignedAngles p s request
The existing native angular inputs imply the smaller qualitative record. Their quantitative-domain smoothness field is not extended or used.
Equations
- One or more equations did not get rendered due to their size.
Instances For
structure
NavierStokes.ActualWaveRegularity.SignedData
{ι : Type}
(p : CorrectionStep.CycleParameters ι)
(v : CorrectionStep.CycleCoefficients ι)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
{coord : ℝ}
(U : LocalSignedRequest.SlowRegion coord)
(r₀ r₁ : ℝ)
:
All fields use the literal post-particular request. The old state, profile, and native data are not reselected.
- mode (l : ι) : ModeData ((p.signed l).copyData p.strip (p.signedRequest v c u)) (HarmonicWaveInteraction.productStrip p.strip) (p.signed l).directions (LinearIsometryEquiv.refl ℝ Cylinder) U r₀ r₁
Mode supplied by
SignedData. - angles (l : ι) : SignedAngles (p.signed l) p.strip (p.signedRequest v c u)
Angles of
SignedData, of type∀ l, SignedAngles (p.signed l) p.strip (p.signedRequest v c u).
Instances For
theorem
NavierStokes.ActualWaveRegularity.SignedData.block_regular
{ι : Type}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
{coord r₀ r₁ : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
(h : SignedData p v c u U r₀ r₁)
(l : ι)
:
WaveStateRegularity.AngularSmooth (PhysicalMeanDomain.slowDomain U.carrier) (p.signedBlock v c u l).oscillation ∧ CorrectionStep.OscillationPeriodic U.carrier (p.signedBlock v c u l).oscillation ∧ WaveStateRegularity.WaveSupport U r₀ r₁ (p.signedBlock v c u l).oscillation
theorem
NavierStokes.ActualWaveRegularity.SignedData.regular
{ι : Type}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
{coord r₀ r₁ : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
(h : SignedData p v c u U r₀ r₁)
:
WaveStateRegularity.AngularSmooth (PhysicalMeanDomain.slowDomain U.carrier) (p.signedVelocity v c u) ∧ CorrectionStep.OscillationPeriodic U.carrier (p.signedVelocity v c u) ∧ WaveStateRegularity.WaveSupport U r₀ r₁ (p.signedVelocity v c u)
theorem
NavierStokes.ActualWaveRegularity.next_regular
{ι : Type}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
{coord r₀ r₁ : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
(hp : ParticularData p v c u U r₀ r₁)
(hs : SignedData p v c u U r₀ r₁)
(hu : WaveStateRegularity.AngularSmooth (PhysicalMeanDomain.slowDomain U.carrier) u.oscillation)
(hper : CorrectionStep.OscillationPeriodic U.carrier u.oscillation)
(hsup : WaveStateRegularity.WaveSupport U r₀ r₁ u.oscillation)
:
WaveStateRegularity.AngularSmooth (PhysicalMeanDomain.slowDomain U.carrier) (p.next v c u).oscillation ∧ CorrectionStep.OscillationPeriodic U.carrier (p.next v c u).oscillation ∧ WaveStateRegularity.WaveSupport U r₀ r₁ (p.next v c u).oscillation
The qualitative oscillation fields of the actual next cycle state. The intervening temporal, rank, and pressure-refresh operations preserve the same oscillation by the literal recurrence.
Moving radial edges of the literal coefficients #
At a flat radial boundary the coefficient need not have a zero germ. Instead, its actual interior tensor bounds prove smoothness across that boundary. The conclusions concern the original coefficient, whose exterior zero values identify it with the constructed extension.
theorem
NavierStokes.ActualWaveRegularity.literal_extension_eqOn
{D E : Type}
[NormedAddCommGroup E]
{Ω : Set D}
{ρ : D → ℝ}
{a b : ℝ}
{f : D → E}
(hz : ∀ x ∈ Ω, x ∉ WaveEdgeExtension.window ρ a b → f x = 0)
:
Set.EqOn (WaveEdgeExtension.extension ρ a b f) f Ω
theorem
NavierStokes.ActualWaveRegularity.literal_moving_regular
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{Ω : Set D}
(hΩ : IsOpen Ω)
{ρ : D → ℝ}
(hρ : ContDiffOn ℝ (↑⊤) ρ Ω)
{a b cL cR : ℝ}
(ha : 0 < a)
(hab : a < b)
(hcL : 0 < cL)
(hcR : 0 < cR)
{f : D → E}
(hf : ContDiffOn ℝ (↑⊤) f (WaveEdgeExtension.windowDomain Ω ρ a b))
(hB : WaveEdgeExtension.BoundaryControls Ω ρ a b cL cR f)
(hz : ∀ x ∈ Ω, x ∉ WaveEdgeExtension.window ρ a b → f x = 0)
:
The original, totalized coefficient has all zero edge tensors, from its actual interior derivatives and its actual exterior values.
theorem
NavierStokes.ActualWaveRegularity.literal_native_regular
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{J : Type}
{V : PrimaryCopyBounds.JetDomain J D}
{Ω : Set D}
(hΩ : IsOpen Ω)
{ρ : D → ℝ}
(hρ : ContDiffOn ℝ (↑⊤) ρ Ω)
{a b cL cR : ℝ}
(ha : 0 < a)
(hab : a < b)
(hcL : 0 < cL)
(hcR : 0 < cR)
{A S : J → ℝ}
{P : J → D → ℝ}
{f : J → D → E}
(hf :
PrimaryCopyBounds.NativeJets V (fun (i : J) (x : D) => A i * √(WaveEdgeExtension.flatWeight ρ a b cL cR x) * P i x) f)
(hA : ∀ (i : J), 0 ≤ A i)
(hS : ∀ (i : J), 1 ≤ S i)
(hP : ∀ (i : J), ContinuousOn (P i) Ω)
(hP0 : ∀ (i : J), ∀ x ∈ Ω, 0 ≤ P i x)
(hdom : ∀ (i : J), WaveEdgeExtension.windowDomain Ω ρ a b ⊆ V.carrier i)
(q : ℕ)
(hG :
∀ (i : J),
∀ x ∈ WaveEdgeExtension.windowDomain Ω ρ a b, V.growth i x ≤ S i * WaveEdgeExtension.edgeGrowth ρ a b x ^ q)
(hz : ∀ (i : J), ∀ x ∈ Ω, x ∉ WaveEdgeExtension.window ρ a b → f i x = 0)
(i : J)
:
Apply the already proved native Gaussian derivative estimates to the same literal coefficient. The constants are those in the native estimates; no full-domain estimate or output smoothness is assumed.
@[reducible, inline]
Index: an abbreviation for ActualSignedStageControls.SignedLabel B N0.
Equations
Instances For
noncomputable def
NavierStokes.ActualWaveRegularityData.Ordered
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
:
Ordered, given by CommonWindow.index ActualPrimary.h n ≤ ChartScales.nativeIndex ActualPrimary.h (BaseChartJets.cellBand l.1).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.ActualWaveRegularityData.deckIndex
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(m : TorusInverse.Frequency)
:
Deck index, given by coverIndex ((ActualPrimary.chartGeometry n l.2 l.1).gap) m.
Equations
Instances For
noncomputable def
NavierStokes.ActualWaveRegularityData.deckPermutation
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(m : TorusInverse.Frequency)
:
Deck permutation, given by Equiv.addRight (deckIndex l n m).
Equations
Instances For
theorem
NavierStokes.ActualWaveRegularityData.nativePoint_ordered
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(hn : Ordered l n)
(k : TorusInverse.Frequency)
(x : FullPoint)
:
theorem
NavierStokes.ActualWaveRegularityData.nativePoint_deck
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(hn : Ordered l n)
(k m : TorusInverse.Frequency)
(x : FullPoint)
:
ActualSignedStageControls.nativePoint l n ((deckPermutation l n m) k) (x + ActualWaveRegularity.deckShift m) = ActualSignedStageControls.nativePoint l n k x
theorem
NavierStokes.ActualWaveRegularityData.cutoff_deck
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(hn : Ordered l n)
(k m : TorusInverse.Frequency)
(x : FullPoint)
:
ActualSignedStageControls.cutoff l ((deckPermutation l n m) k) n (x + ActualWaveRegularity.deckShift m) = ActualSignedStageControls.cutoff l k n x
theorem
NavierStokes.ActualWaveRegularityData.signed_amplitude_deck
{B N0 : ℕ}
(l : Index B N0)
(s : WeightedClasses.StripData Point)
(request : ℕ → FullPoint → SignedWaveUpdate.Vec2)
(n : ℕ)
(hn : Ordered l n)
(k m : TorusInverse.Frequency)
(x : FullPoint)
(hR : request n (x + ActualWaveRegularity.deckShift m) = request n x)
:
((ActualSignedStageControls.parameters l).copyData s request).amplitude n ((deckPermutation l n m) k)
(x + ActualWaveRegularity.deckShift m) = ((ActualSignedStageControls.parameters l).copyData s request).amplitude n k x
theorem
NavierStokes.ActualWaveRegularityData.fullRequest_deck
(s : WeightedClasses.StripData Point)
(P : SignedStressPrimitive.Patch)
(coord : ℝ)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(n : ℕ)
(m : TorusInverse.Frequency)
(x : FullPoint)
:
LocalSignedRequest.fullRequest s P coord c u n (x + ActualWaveRegularity.deckShift m) = LocalSignedRequest.fullRequest s P coord c u n x
theorem
NavierStokes.ActualWaveRegularityData.signed_request_amplitude_deck
{B N0 : ℕ}
(l : Index B N0)
(s : WeightedClasses.StripData Point)
(P : SignedStressPrimitive.Patch)
(coord : ℝ)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(n : ℕ)
(hn : Ordered l n)
(k m : TorusInverse.Frequency)
(x : FullPoint)
:
((ActualSignedStageControls.parameters l).copyData s (LocalSignedRequest.fullRequest s P coord c u)).amplitude n
((deckPermutation l n m) k) (x + ActualWaveRegularity.deckShift m) = ((ActualSignedStageControls.parameters l).copyData s (LocalSignedRequest.fullRequest s P coord c u)).amplitude n k x
theorem
NavierStokes.ActualWaveRegularityData.clock_deck
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(hn : Ordered l n)
(Y : TorusInverse.Plane)
(m : TorusInverse.Frequency)
:
PeriodicPhaseAssembly.periodicClock (CorrectionInitialization.ActualPrimary.geometry l.2 l.1)
(CorrectionInitialization.ActualPrimary.clockWindow l.1).cutoff
((CommonCoverSolve.coverPower
(CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).symm
(Y + TorusAverages.latticePoint m)) = PeriodicPhaseAssembly.periodicClock (CorrectionInitialization.ActualPrimary.geometry l.2 l.1)
(CorrectionInitialization.ActualPrimary.clockWindow l.1).cutoff
((CommonCoverSolve.coverPower
(CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).symm
Y)
theorem
NavierStokes.ActualWaveRegularityData.phase_deck
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(hn : Ordered l n)
(m : TorusInverse.Frequency)
:
theorem
NavierStokes.ActualWaveRegularityData.radius_deck
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(m : TorusInverse.Frequency)
:
theorem
NavierStokes.ActualWaveRegularityData.radial_deck
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(m : TorusInverse.Frequency)
:
noncomputable def
NavierStokes.ActualWaveRegularityData.signedAngles
{B N0 : ℕ}
(l : Index B N0)
(s : WeightedClasses.StripData Point)
(P : SignedStressPrimitive.Patch)
(coord : ℝ)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
:
Signed angles, bundling slope, radius, radial, phase and the required compatibility
proofs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The actual slow mask selects an ordered native cover #
theorem
NavierStokes.ActualWaveRegularityData.near_of_native_band
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
{p : PhaseCalculus.Slow}
(ht : 0 < p.2.2)
(hq0 : SimilarityHomogeneity.chartQ CorrectionInitialization.ActualPrimary.h p ∈ Set.Ioo (1 / 2) 2)
(hq :
SimilarityHomogeneity.chartQ CorrectionInitialization.ActualPrimary.h
((ActualSignedGeometry.slowChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n)
(ChartScales.Q (BaseChartJets.cellBand l.1)))
p) ∈ Set.Icc (1 / 2) 2)
:
ActualPrimaryBounds.near (l.2, l.1) n
theorem
NavierStokes.ActualWaveRegularityData.ordered_of_native_band
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
{p : PhaseCalculus.Slow}
(ht : 0 < p.2.2)
(hq0 : SimilarityHomogeneity.chartQ CorrectionInitialization.ActualPrimary.h p ∈ Set.Ioo (1 / 2) 2)
(hq :
SimilarityHomogeneity.chartQ CorrectionInitialization.ActualPrimary.h
((ActualSignedGeometry.slowChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n)
(ChartScales.Q (BaseChartJets.cellBand l.1)))
p) ∈ Set.Icc (1 / 2) 2)
:
Ordered l n
theorem
NavierStokes.ActualWaveRegularityData.ordered_of_mask
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(k : TorusInverse.Frequency)
{x : FullPoint}
(hx : x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion)
(hm : ActualSignedStageControls.mask l k n x ≠ 0)
:
Ordered l n
theorem
NavierStokes.ActualWaveRegularityData.mask_zero_of_not_ordered
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(hn : ¬Ordered l n)
(k : TorusInverse.Frequency)
{x : FullPoint}
(hx : x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion)
:
theorem
NavierStokes.ActualWaveRegularityData.mask_zero_germ_of_not_ordered
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(hn : ¬Ordered l n)
(k : TorusInverse.Frequency)
{x : FullPoint}
(hx : x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion)
:
theorem
NavierStokes.ActualWaveRegularityData.signed_zero_germs_of_not_ordered
{B N0 : ℕ}
(l : Index B N0)
(s : WeightedClasses.StripData Point)
(request : ℕ → FullPoint → SignedWaveUpdate.Vec2)
(n : ℕ)
(hn : ¬Ordered l n)
{x : FullPoint}
(hx : x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion)
:
have a := (ActualSignedStageControls.parameters l).copyData s request;
((a.commonCorrected (HarmonicWaveInteraction.productStrip s)
(ActualSignedStageControls.parameters l).directions).amplitude
n =ᶠ[nhds x] fun (x : FullPoint) => 0) ∧ (a.common.pressure n =ᶠ[nhds x] fun (x : FullPoint) => 0) ∧ a.globalGaussian (ActualSignedStageControls.parameters l).directions n =ᶠ[nhds x] fun (x : FullPoint) => 0
The actual three assembled fields vanish on inactive common bands. The proof uses raw zero germs before applying the curl and copy sum.
theorem
NavierStokes.ActualWaveRegularityData.signed_block_periodic
{B N0 : ℕ}
(l : Index B N0)
(s : WeightedClasses.StripData Point)
(P : SignedStressPrimitive.Patch)
(coord : ℝ)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
:
The actual full-domain phase patches #
noncomputable def
NavierStokes.ActualWaveRegularityData.signedPhasePatch
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(k : TorusInverse.Frequency)
:
Signed phase patch as an element of Set FullPoint.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ActualWaveRegularityData.signedPhasePatch_open
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(k : TorusInverse.Frequency)
:
IsOpen (signedPhasePatch l n k)
theorem
NavierStokes.ActualWaveRegularityData.native_time_pos
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(k : TorusInverse.Frequency)
{x : FullPoint}
(hx : x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion)
:
theorem
NavierStokes.ActualWaveRegularityData.mask_zero_germ_outside_carrier
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(k : TorusInverse.Frequency)
{x : FullPoint}
(hx : x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion)
(hc :
(ActualSignedStageControls.nativePoint l n k x).1 ∉
(PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal
(CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier
l.1)
:
theorem
NavierStokes.ActualWaveRegularityData.signed_patch_cover
{B N0 : ℕ}
(l : Index B N0)
(s : WeightedClasses.StripData Point)
(request : ℕ → FullPoint → SignedWaveUpdate.Vec2)
(n : ℕ)
(k : TorusInverse.Frequency)
{x : FullPoint}
(hx : x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion)
:
Every point of the full slow domain either lies in the genuine positive-radius, interior-clock patch, or has a zero localized raw germ.
theorem
NavierStokes.ActualWaveRegularityData.signedPhasePatch_positive
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(k : TorusInverse.Frequency)
{x : FullPoint}
(hx :
x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion ∩ signedPhasePatch l n k)
:
theorem
NavierStokes.ActualWaveRegularityData.signed_phase_smooth
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(k : TorusInverse.Frequency)
:
theorem
NavierStokes.ActualWaveRegularityData.signed_geometry
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(k : TorusInverse.Frequency)
:
CurlClassBounds.CylindricalGeometry
(ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion ∩ signedPhasePatch l n k)
((ActualSignedStageControls.parameters l).base.radius n)
((ActualSignedStageControls.parameters l).directions.radialField n)
(fun (x : ActualWaveRegularity.Cylinder) => (ActualSignedStageControls.parameters l).directions.angular)
((ActualSignedStageControls.parameters l).directions.axialField
(HarmonicWaveInteraction.productStrip ActualPrimaryBounds.strip) n)
theorem
NavierStokes.ActualWaveRegularityData.signed_normal_ne
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(k : TorusInverse.Frequency)
{x : FullPoint}
(hx :
x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion ∩ signedPhasePatch l n k)
:
Literal exterior values of the signed quotient #
theorem
NavierStokes.ActualWaveRegularityData.raw_zero_of_target
{B N0 : ℕ}
(l : Index B N0)
(s : WeightedClasses.StripData Point)
(request : ℕ → FullPoint → SignedWaveUpdate.Vec2)
(n : ℕ)
(k : TorusInverse.Frequency)
(x : FullPoint)
(ht : ActualSignedStageControls.target l k n x = 0)
:
((ActualSignedStageControls.parameters l).copyData s request).amplitude n k x = 0 ∧ ((ActualSignedStageControls.parameters l).copyData s request).pressure n k x = 0
theorem
NavierStokes.ActualWaveRegularityData.target_zero_outside
{p : PhaseCalculus.Slow}
(ht : 0 < p.2.2)
(hr : 0 < p.1)
(hout :
PrimaryTargetBounds.profileRadius CorrectionInitialization.ActualPrimary.h p ∉
Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal))
:
Radius, given by x.1.1 / VariableGaugeMean.qLength (2 * ActualPrimary.h) x.1.2.1.
Equations
Instances For
theorem
NavierStokes.ActualWaveRegularityData.native_radius
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(k : TorusInverse.Frequency)
{x : FullPoint}
(hx : x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion)
(hr : 0 < x.1.1)
:
theorem
NavierStokes.ActualWaveRegularityData.signed_raw_zero_outside
{B N0 : ℕ}
(l : Index B N0)
(s : WeightedClasses.StripData Point)
(request : ℕ → FullPoint → SignedWaveUpdate.Vec2)
(n : ℕ)
(k : TorusInverse.Frequency)
{x : FullPoint}
(hx : x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion)
(hout :
radius x ∉
Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal))
:
((ActualSignedStageControls.parameters l).copyData s request).amplitude n k x = 0 ∧ ((ActualSignedStageControls.parameters l).copyData s request).pressure n k x = 0
theorem
NavierStokes.ActualWaveRegularityData.mask_zero_germ_outside_band
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(k : TorusInverse.Frequency)
{x : FullPoint}
(hx : x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion)
(hq :
SimilarityHomogeneity.chartQ CorrectionInitialization.ActualPrimary.h
(ActualSignedStageControls.nativePoint l n k x).1 ∉
Set.Icc (1 / 2) 2)
:
theorem
NavierStokes.ActualWaveRegularityData.signed_phaseCell_or_zero
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(k : TorusInverse.Frequency)
{x : FullPoint}
(hx : x ∈ ActualSignedStageControls.fullStrip.domain)
:
x ∈ ActualSignedStageControls.phaseCell l n k ∨ (ActualSignedStageControls.cutoff l k n =ᶠ[nhds x] fun (x : FullPoint) => 0) ∨ ActualSignedStageControls.mask l k n =ᶠ[nhds x] fun (x : FullPoint) => 0
Actual quantitative cells cover every nonzero localized copy on the whole open strip. Closed dyadic, transverse and temporal endpoints remain in the cell; only genuine zero neighborhoods are used in the alternatives.
The actual strip weight gives all zero edge tensors #
theorem
NavierStokes.ActualWaveRegularityData.strip_domain_eq :
ActualSignedStageControls.fullStrip.domain = WaveEdgeExtension.windowDomain (ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion)
radius (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)
theorem
NavierStokes.ActualWaveRegularityData.strip_zeta
(x : FullPoint)
:
ActualSignedStageControls.fullStrip.zeta x = WaveEdgeExtension.flatWeight radius (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)
(FinalSlowBase.edgeExponent CorrectionInitialization.ActualPrimary.nominal / 4) 1 x
theorem
NavierStokes.ActualWaveRegularityData.full_regular_of_class
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : ℕ → FullPoint → E}
{α : ℝ}
(hf :
WeightedClasses.MemClass ActualSignedStageControls.fullStrip
(fun (x : ℕ) (x_1 : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x_1)) α f)
(hz :
∀ (n : ℕ),
∀ x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion,
radius x ∉
Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) →
f n x = 0)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) (f n) (ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion) ∧ ∀ (m : ℕ),
∀ x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion,
radius x = PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal ∨ radius x = PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal →
iteratedFDeriv ℝ m (f n) x = 0
This uses the actual product weight and actual strip growth. There is no boundary-continuity premise and no change to the given function.
theorem
NavierStokes.ActualWaveRegularityData.full_regular_of_envelope_class
{B N0 : ℕ}
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(l : Index B N0)
{f : ℕ → FullPoint → E}
{α : ℝ}
(hf :
WeightedClasses.MemClass ActualSignedStageControls.fullStrip
(fun (n : ℕ) (x : ActualSignedStageControls.FullPoint) =>
√(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope l n x)
α f)
(hz :
∀ (n : ℕ),
∀ x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion,
radius x ∉
Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) →
f n x = 0)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) (f n) (ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion) ∧ ∀ (m : ℕ),
∀ x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion,
radius x = PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal ∨ radius x = PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal →
iteratedFDeriv ℝ m (f n) x = 0
Whole-domain regularity of the literal signed fields #
noncomputable def
NavierStokes.ActualWaveRegularityData.signedCopies
{B N0 : ℕ}
(l : Index B N0)
(request : ℕ → FullPoint → SignedWaveUpdate.Vec2)
:
Signed copies, given by (ActualSignedStageControls.parameters l).copyData ActualPrimaryBounds.strip request.
Equations
Instances For
theorem
NavierStokes.ActualWaveRegularityData.signed_common_raw_zero_outside
{B N0 : ℕ}
(l : Index B N0)
(request : ℕ → FullPoint → SignedWaveUpdate.Vec2)
(n : ℕ)
{x : FullPoint}
(hx : x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion)
(hout :
radius x ∉
Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal))
:
(signedCopies l request).common.amplitude n x = 0 ∧ (signedCopies l request).common.pressure n x = 0
theorem
NavierStokes.ActualWaveRegularityData.signed_common_raw_zero_germ
{B N0 : ℕ}
(l : Index B N0)
(request : ℕ → FullPoint → SignedWaveUpdate.Vec2)
(n : ℕ)
{x : FullPoint}
(hx : x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion)
(hout :
radius x ∉
Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal))
:
theorem
NavierStokes.ActualWaveRegularityData.radius_nonpos
{x : FullPoint}
(hx : x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion)
(hr : x.1.1 ≤ 0)
:
theorem
NavierStokes.ActualWaveRegularityData.signed_common_zero_germ_nonpositive
{B N0 : ℕ}
(l : Index B N0)
(request : ℕ → FullPoint → SignedWaveUpdate.Vec2)
(n : ℕ)
{x : FullPoint}
(hx : x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion)
(hr : x.1.1 ≤ 0)
:
theorem
NavierStokes.ActualWaveRegularityData.signed_raw_full_regular
{B N0 : ℕ}
(l : Index B N0)
(request : ℕ → FullPoint → SignedWaveUpdate.Vec2)
{α : ℝ}
(ha :
WeightedClasses.MemClass ActualSignedStageControls.fullStrip
(fun (n : ℕ) (x : ActualSignedStageControls.FullPoint) =>
√(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope l n x)
α (signedCopies l request).common.amplitude)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) ((signedCopies l request).common.amplitude n)
(ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion) ∧ ∀ (m : ℕ),
∀ x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion,
radius x = PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal ∨ radius x = PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal →
iteratedFDeriv ℝ m ((signedCopies l request).common.amplitude n) x = 0
theorem
NavierStokes.ActualWaveRegularityData.signed_pressure_full_regular
{B N0 : ℕ}
(l : Index B N0)
(request : ℕ → FullPoint → SignedWaveUpdate.Vec2)
{α : ℝ}
(hp :
WeightedClasses.MemClass ActualSignedStageControls.fullStrip
(fun (n : ℕ) (x : ActualSignedStageControls.FullPoint) =>
√(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope l n x)
α (signedCopies l request).common.pressure)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) ((signedCopies l request).common.pressure n)
(ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion) ∧ ∀ (m : ℕ),
∀ x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion,
radius x = PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal ∨ radius x = PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal →
iteratedFDeriv ℝ m ((signedCopies l request).common.pressure n) x = 0
Positive domain, given by ActualWaveRegularity.fullDomain ActualPrimary.standardRegion ∩ ActualPrimaryCoherence.positiveRadialChart.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ActualWaveRegularityData.smooth_of_positive_or_zero
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : FullPoint → E}
(hf : ContDiffOn ℝ (↑⊤) f positiveDomain)
(hz :
∀ x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion,
x.1.1 ≤ 0 → f =ᶠ[nhds x] fun (x : ActualWaveRegularity.Cylinder) => 0)
:
noncomputable def
NavierStokes.ActualWaveRegularityData.signedNormal
{B N0 : ℕ}
(l : Index B N0)
(request : ℕ → FullPoint → SignedWaveUpdate.Vec2)
(n : ℕ)
:
Signed normal, constructed using CurlClassBounds.coefficient.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.ActualWaveRegularityData.signedCorrected
{B N0 : ℕ}
(l : Index B N0)
(request : ℕ → FullPoint → SignedWaveUpdate.Vec2)
:
Signed corrected, given by (signedCopies l request).commonCorrected ActualSignedStageControls.fullStrip (ActualSignedStageControls.parameters l).directions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ActualWaveRegularityData.positive_geometry
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
:
CurlClassBounds.CylindricalGeometry positiveDomain ((ActualSignedStageControls.parameters l).base.radius n)
((ActualSignedStageControls.parameters l).directions.radialField n)
(fun (x : FullPoint) => (ActualSignedStageControls.parameters l).directions.angular)
((ActualSignedStageControls.parameters l).directions.axialField ActualSignedStageControls.fullStrip n)
theorem
NavierStokes.ActualWaveRegularityData.signed_normal_zero_germ
{B N0 : ℕ}
(l : Index B N0)
(request : ℕ → FullPoint → SignedWaveUpdate.Vec2)
(n : ℕ)
{x : FullPoint}
(hx : x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion)
(hout :
radius x ∉
Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal))
:
theorem
NavierStokes.ActualWaveRegularityData.signed_corrected_zero_germ
{B N0 : ℕ}
(l : Index B N0)
(request : ℕ → FullPoint → SignedWaveUpdate.Vec2)
(n : ℕ)
{x : FullPoint}
(hx : x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion)
(hout :
radius x ∉
Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal))
:
theorem
NavierStokes.ActualWaveRegularityData.signed_normal_smooth
{B N0 : ℕ}
(l : Index B N0)
(request : ℕ → FullPoint → SignedWaveUpdate.Vec2)
{α : ℝ}
(ha :
WeightedClasses.MemClass ActualSignedStageControls.fullStrip
(fun (n : ℕ) (x : ActualSignedStageControls.FullPoint) =>
√(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope l n x)
α (signedCopies l request).common.amplitude)
(n : ℕ)
:
theorem
NavierStokes.ActualWaveRegularityData.signed_corrected_smooth
{B N0 : ℕ}
(l : Index B N0)
(request : ℕ → FullPoint → SignedWaveUpdate.Vec2)
{α : ℝ}
(ha :
WeightedClasses.MemClass ActualSignedStageControls.fullStrip
(fun (n : ℕ) (x : ActualSignedStageControls.FullPoint) =>
√(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope l n x)
α (signedCopies l request).common.amplitude)
(n : ℕ)
:
noncomputable def
NavierStokes.ActualWaveRegularityData.signedField
{B N0 : ℕ}
(l : Index B N0)
(a : ℕ → FullPoint → HarmonicCalculus.ComplexVector)
:
Signed field as an element of CorrectionState.Oscillation Point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ActualWaveRegularityData.signedField_smooth
{B N0 : ℕ}
(l : Index B N0)
(a : ℕ → FullPoint → HarmonicCalculus.ComplexVector)
(ha :
∀ (n : ℕ),
ContDiffOn ℝ (↑⊤) (a n) (ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion))
(hz :
∀ (n : ℕ),
∀ x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion,
x.1.1 ≤ 0 → a n =ᶠ[nhds x] fun (x : ActualWaveRegularity.Cylinder) => 0)
:
theorem
NavierStokes.ActualWaveRegularityData.signedField_support
{B N0 : ℕ}
(l : Index B N0)
(a : ℕ → FullPoint → HarmonicCalculus.ComplexVector)
(hz :
∀ (n : ℕ),
∀ x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion,
radius x ∉
Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) →
a n =ᶠ[nhds x] fun (x : ActualWaveRegularity.Cylinder) => 0)
:
theorem
NavierStokes.ActualWaveRegularityData.signed_exact_smooth
{B N0 : ℕ}
(l : Index B N0)
(P : SignedStressPrimitive.Patch)
(coord : ℝ)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
{α : ℝ}
(ha :
WeightedClasses.MemClass ActualSignedStageControls.fullStrip
(fun (n : ℕ) (x : ActualSignedStageControls.FullPoint) =>
√(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope l n x)
α (signedCopies l (LocalSignedRequest.fullRequest ActualPrimaryBounds.strip P coord c u)).common.amplitude)
:
theorem
NavierStokes.ActualWaveRegularityData.signed_exact_support
{B N0 : ℕ}
(l : Index B N0)
(P : SignedStressPrimitive.Patch)
(coord : ℝ)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
:
WaveStateRegularity.WaveSupport CorrectionInitialization.ActualPrimary.standardRegion
(PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)
((ActualSignedStageControls.parameters l).exactBlock ActualPrimaryBounds.strip
(LocalSignedRequest.fullRequest ActualPrimaryBounds.strip P coord c u)).oscillation
theorem
NavierStokes.ActualWaveRegularityData.signed_gaussian_zero_outside
{B N0 : ℕ}
(l : Index B N0)
(request : ℕ → FullPoint → SignedWaveUpdate.Vec2)
(n : ℕ)
{x : FullPoint}
(hx : x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion)
(hout :
radius x ∉
Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal))
:
theorem
NavierStokes.ActualWaveRegularityData.signed_gaussian_full_regular
{B N0 : ℕ}
(l : Index B N0)
(request : ℕ → FullPoint → SignedWaveUpdate.Vec2)
{α : ℝ}
(hg :
WeightedClasses.MemClass ActualSignedStageControls.fullStrip
(fun (x : ℕ) (x_1 : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x_1)) α
((signedCopies l request).globalGaussian (ActualSignedStageControls.parameters l).directions))
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) ((signedCopies l request).globalGaussian (ActualSignedStageControls.parameters l).directions n)
(ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion) ∧ ∀ (m : ℕ),
∀ x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion,
radius x = PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal ∨ radius x = PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal →
iteratedFDeriv ℝ m
((signedCopies l request).globalGaussian (ActualSignedStageControls.parameters l).directions n) x = 0
theorem
NavierStokes.ActualWaveRegularityData.signed_tangent_eq_field
{B N0 : ℕ}
(l : Index B N0)
(P : SignedStressPrimitive.Patch)
(coord : ℝ)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
:
theorem
NavierStokes.ActualWaveRegularityData.signed_tangent_smooth
{B N0 : ℕ}
(l : Index B N0)
(P : SignedStressPrimitive.Patch)
(coord : ℝ)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
{α : ℝ}
(ha :
WeightedClasses.MemClass ActualSignedStageControls.fullStrip
(fun (n : ℕ) (x : ActualSignedStageControls.FullPoint) =>
√(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope l n x)
α (signedCopies l (LocalSignedRequest.fullRequest ActualPrimaryBounds.strip P coord c u)).common.amplitude)
:
theorem
NavierStokes.ActualWaveRegularityData.signed_tangent_support
{B N0 : ℕ}
(l : Index B N0)
(P : SignedStressPrimitive.Patch)
(coord : ℝ)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
:
WaveStateRegularity.WaveSupport CorrectionInitialization.ActualPrimary.standardRegion
(PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)
((ActualSignedStageControls.parameters l).tangentBlock ActualPrimaryBounds.strip
(LocalSignedRequest.fullRequest ActualPrimaryBounds.strip P coord c u)).oscillation
theorem
NavierStokes.ActualWaveRegularityData.signed_common_raw_zero_germ_of_not_ordered
{B N0 : ℕ}
(l : Index B N0)
(request : ℕ → FullPoint → SignedWaveUpdate.Vec2)
(n : ℕ)
(hn : ¬Ordered l n)
{x : FullPoint}
(hx : x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion)
:
theorem
NavierStokes.ActualWaveRegularityData.signed_tangent_periodic
{B N0 : ℕ}
(l : Index B N0)
(P : SignedStressPrimitive.Patch)
(coord : ℝ)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
:
theorem
NavierStokes.ActualWaveRegularityData.smooth_conjugatePair
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{U : Set D}
{f : D → ℂ}
(hf : ContDiffOn ℝ (↑⊤) f U)
(j : ℤ)
:
theorem
NavierStokes.ActualWaveRegularityData.signed_exact_coefficients_smooth
{B N0 : ℕ}
(l : Index B N0)
(request : ℕ → FullPoint → SignedWaveUpdate.Vec2)
{α : ℝ}
(ha :
WeightedClasses.MemClass ActualSignedStageControls.fullStrip
(fun (n : ℕ) (x : ActualSignedStageControls.FullPoint) =>
√(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope l n x)
α (signedCopies l request).common.amplitude)
(n : ℕ)
(i : Fin 3)
:
theorem
NavierStokes.ActualWaveRegularityData.signed_tangent_coefficients_smooth
{B N0 : ℕ}
(l : Index B N0)
(request : ℕ → FullPoint → SignedWaveUpdate.Vec2)
{α : ℝ}
(ha :
WeightedClasses.MemClass ActualSignedStageControls.fullStrip
(fun (n : ℕ) (x : ActualSignedStageControls.FullPoint) =>
√(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope l n x)
α (signedCopies l request).common.amplitude)
(n : ℕ)
(i : Fin 3)
:
theorem
NavierStokes.ActualWaveRegularityData.signed_pressure_coefficients_smooth
{B N0 : ℕ}
(l : Index B N0)
(request : ℕ → FullPoint → SignedWaveUpdate.Vec2)
{α : ℝ}
(hp :
WeightedClasses.MemClass ActualSignedStageControls.fullStrip
(fun (n : ℕ) (x : ActualSignedStageControls.FullPoint) =>
√(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope l n x)
α (signedCopies l request).common.pressure)
(n : ℕ)
:
theorem
NavierStokes.ActualWaveRegularityData.signed_gaussian_coefficients_smooth
{B N0 : ℕ}
(l : Index B N0)
(request : ℕ → FullPoint → SignedWaveUpdate.Vec2)
{α : ℝ}
(hg :
WeightedClasses.MemClass ActualSignedStageControls.fullStrip
(fun (x : ℕ) (x_1 : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x_1)) α
((signedCopies l request).globalGaussian (ActualSignedStageControls.parameters l).directions))
(n : ℕ)
(i : Fin 3)
:
theorem
NavierStokes.ActualWaveRegularityData.signed_pressure_smooth
{B N0 : ℕ}
(l : Index B N0)
(P : SignedStressPrimitive.Patch)
(coord : ℝ)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
{α : ℝ}
(hp :
WeightedClasses.MemClass ActualSignedStageControls.fullStrip
(fun (n : ℕ) (x : ActualSignedStageControls.FullPoint) =>
√(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope l n x)
α (signedCopies l (LocalSignedRequest.fullRequest ActualPrimaryBounds.strip P coord c u)).common.pressure)
(n : ℕ)
:
The same edge continuation in the particular solver's coordinates #
Particular full strip, given by ParticularWaveBounds.reindexStrip ActualWaveRegularity.particularChart.symm ActualSignedStageControls.fullStrip.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ActualWaveRegularityData.particular_pull_class
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : ℕ → ActualWaveRegularity.ParticularSpace → E}
{α : ℝ}
(hf :
WeightedClasses.MemClass particularFullStrip
(fun (x : ℕ) (x_1 : ActualWaveRegularity.ParticularSpace) => √(particularFullStrip.zeta x_1)) α f)
:
WeightedClasses.MemClass ActualSignedStageControls.fullStrip
(fun (x : ℕ) (x_1 : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x_1)) α
fun (n : ℕ) (x : ActualSignedStageControls.FullPoint) => f n (ActualWaveRegularity.particularChart x)
theorem
NavierStokes.ActualWaveRegularityData.particular_full_regular_of_class
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : ℕ → ActualWaveRegularity.ParticularSpace → E}
{α : ℝ}
(hf :
WeightedClasses.MemClass particularFullStrip
(fun (x : ℕ) (x_1 : ActualWaveRegularity.ParticularSpace) => √(particularFullStrip.zeta x_1)) α f)
(hz :
∀ (n : ℕ),
∀
z ∈
ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart
CorrectionInitialization.ActualPrimary.standardRegion,
radius (ActualWaveRegularity.particularChart.symm z) ∉
Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) →
f n z = 0)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) (f n)
(ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart
CorrectionInitialization.ActualPrimary.standardRegion) ∧ ∀ (m : ℕ),
∀
z ∈
ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart
CorrectionInitialization.ActualPrimary.standardRegion,
radius (ActualWaveRegularity.particularChart.symm z) = PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal ∨ radius (ActualWaveRegularity.particularChart.symm z) = PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal →
iteratedFDeriv ℝ m (f n) z = 0
No new radial coordinate or flat weight is chosen for the particular solver. Reassociation preserves the actual derivative norms.
The particular phase below is the literal carrier of its incoming block. Its equality with the selected primary phase is a carrier invariant, not a smoothness assumption on an output.
noncomputable def
NavierStokes.ActualWaveRegularityData.particularCopies
{B N0 : ℕ}
(l : ActualParticularStageControls.Label B N0)
(c : CorrectionState.Context (CorrectionStep.CycleSlow × TorusInverse.Plane))
(u : CorrectionState.State (CorrectionStep.CycleSlow × TorusInverse.Plane))
(b : CorrectionState.HarmonicBlock (CorrectionStep.CycleSlow × TorusInverse.Plane))
(G A : HarmonicResidual.BlockCoefficients (CorrectionStep.CycleSlow × TorusInverse.Plane))
(j : ℤ)
:
Particular copies, given by (ActualParticularStageControls.canonicalParameters l).copyData c u b G A j.
Equations
- NavierStokes.ActualWaveRegularityData.particularCopies l c u b G A j = (NavierStokes.ActualParticularStageControls.canonicalParameters l).copyData c u b G A j
Instances For
Particular positive, given by ActualWaveRegularity.particularChart.symm ⁻¹' positiveDomain.
Equations
Instances For
theorem
NavierStokes.ActualWaveRegularityData.particular_native_normal
{B N0 : ℕ}
(l : ActualParticularStageControls.Label B N0)
(n : ℕ)
{z : ActualWaveRegularity.ParticularSpace}
(hz : z ∈ particularPositive)
:
(ActualParticularStageControls.background l).normal particularFullStrip ActualParticularStageControls.directions n z = (CorrectionInitialization.ActualPrimary.chartCoefficients l.1 l.2).normal ActualSignedStageControls.fullStrip
(ActualSignedStageControls.parameters (l.2, l.1)).directions n (ActualWaveRegularity.particularChart.symm z)
theorem
NavierStokes.ActualWaveRegularityData.particular_geometry_smooth
{B N0 : ℕ}
(l : ActualParticularStageControls.Label B N0)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) ((ActualParticularStageControls.background l).radius n) particularPositive ∧ (∀ z ∈ particularPositive, (ActualParticularStageControls.background l).radius n z ≠ 0) ∧ ContDiffOn ℝ (↑⊤) (ActualParticularStageControls.directions.radialField n) particularPositive ∧ ContDiffOn ℝ (↑⊤)
(fun (x : ActualWaveRegularity.ParticularSpace) => ActualParticularStageControls.directions.angular)
particularPositive ∧ ContDiffOn ℝ (↑⊤) (ActualParticularStageControls.directions.axialField particularFullStrip n) particularPositive
theorem
NavierStokes.ActualWaveRegularityData.particular_zero_germ
{E : Type}
[NormedAddCommGroup E]
(f : ℕ → ActualWaveRegularity.ParticularSpace → E)
(hz :
∀ (n : ℕ),
∀
z ∈
ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart
CorrectionInitialization.ActualPrimary.standardRegion,
radius (ActualWaveRegularity.particularChart.symm z) ∉
Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) →
f n z = 0)
(n : ℕ)
{z : ActualWaveRegularity.ParticularSpace}
(hm :
z ∈ ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart
CorrectionInitialization.ActualPrimary.standardRegion)
(ho :
radius (ActualWaveRegularity.particularChart.symm z) ∉
Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal))
:
theorem
NavierStokes.ActualWaveRegularityData.particular_smooth_of_positive_or_zero
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : ActualWaveRegularity.ParticularSpace → E}
(hp : ContDiffOn ℝ (↑⊤) f particularPositive)
(hz :
∀
z ∈
ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart
CorrectionInitialization.ActualPrimary.standardRegion,
z.1.1.1 ≤ 0 → f =ᶠ[nhds z] fun (x : ActualWaveRegularity.ParticularSpace) => 0)
:
noncomputable def
NavierStokes.ActualWaveRegularityData.particularNormal
{B N0 : ℕ}
(l : ActualParticularStageControls.Label B N0)
(c : CorrectionState.Context (CorrectionStep.CycleSlow × TorusInverse.Plane))
(u : CorrectionState.State (CorrectionStep.CycleSlow × TorusInverse.Plane))
(b : CorrectionState.HarmonicBlock (CorrectionStep.CycleSlow × TorusInverse.Plane))
(G A : HarmonicResidual.BlockCoefficients (CorrectionStep.CycleSlow × TorusInverse.Plane))
(j : ℤ)
(n : ℕ)
:
Particular normal, constructed using CurlClassBounds.coefficient.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ActualWaveRegularityData.particular_normal_smooth
{B N0 : ℕ}
(l : ActualParticularStageControls.Label B N0)
(c : CorrectionState.Context (CorrectionStep.CycleSlow × TorusInverse.Plane))
(u : CorrectionState.State (CorrectionStep.CycleSlow × TorusInverse.Plane))
(b : CorrectionState.HarmonicBlock (CorrectionStep.CycleSlow × TorusInverse.Plane))
(G A : HarmonicResidual.BlockCoefficients (CorrectionStep.CycleSlow × TorusInverse.Plane))
(j : ℤ)
(hphase : (particularCopies l c u b G A j).background.phase = (ActualParticularStageControls.background l).phase)
{α : ℝ}
(ha :
WeightedClasses.MemClass particularFullStrip
(fun (x : ℕ) (z : ActualWaveRegularity.ParticularSpace) => √(particularFullStrip.zeta z)) α
(particularCopies l c u b G A j).common.amplitude)
(hz :
∀ (n : ℕ),
∀
z ∈
ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart
CorrectionInitialization.ActualPrimary.standardRegion,
radius (ActualWaveRegularity.particularChart.symm z) ∉
Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) →
(particularCopies l c u b G A j).common.amplitude n z = 0)
(n : ℕ)
:
theorem
NavierStokes.ActualWaveRegularityData.particular_corrected_zero_germ
{B N0 : ℕ}
(l : ActualParticularStageControls.Label B N0)
(c : CorrectionState.Context (CorrectionStep.CycleSlow × TorusInverse.Plane))
(u : CorrectionState.State (CorrectionStep.CycleSlow × TorusInverse.Plane))
(b : CorrectionState.HarmonicBlock (CorrectionStep.CycleSlow × TorusInverse.Plane))
(G A : HarmonicResidual.BlockCoefficients (CorrectionStep.CycleSlow × TorusInverse.Plane))
(j : ℤ)
(hz :
∀ (n : ℕ),
∀
z ∈
ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart
CorrectionInitialization.ActualPrimary.standardRegion,
radius (ActualWaveRegularity.particularChart.symm z) ∉
Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) →
(particularCopies l c u b G A j).common.amplitude n z = 0)
(n : ℕ)
{z : ActualWaveRegularity.ParticularSpace}
(hm :
z ∈ ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart
CorrectionInitialization.ActualPrimary.standardRegion)
(ho :
radius (ActualWaveRegularity.particularChart.symm z) ∉
Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal))
:
((particularCopies l c u b G A j).commonCorrected particularFullStrip
(ActualParticularStageControls.canonicalParameters l).directions).amplitude
n =ᶠ[nhds z] fun (x : ActualWaveRegularity.ParticularSpace) => 0
theorem
NavierStokes.ActualWaveRegularityData.particular_corrected_smooth
{B N0 : ℕ}
(l : ActualParticularStageControls.Label B N0)
(c : CorrectionState.Context (CorrectionStep.CycleSlow × TorusInverse.Plane))
(u : CorrectionState.State (CorrectionStep.CycleSlow × TorusInverse.Plane))
(b : CorrectionState.HarmonicBlock (CorrectionStep.CycleSlow × TorusInverse.Plane))
(G A : HarmonicResidual.BlockCoefficients (CorrectionStep.CycleSlow × TorusInverse.Plane))
(j : ℤ)
(hphase : (particularCopies l c u b G A j).background.phase = (ActualParticularStageControls.background l).phase)
{α : ℝ}
(ha :
WeightedClasses.MemClass particularFullStrip
(fun (x : ℕ) (z : ActualWaveRegularity.ParticularSpace) => √(particularFullStrip.zeta z)) α
(particularCopies l c u b G A j).common.amplitude)
(hz :
∀ (n : ℕ),
∀
z ∈
ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart
CorrectionInitialization.ActualPrimary.standardRegion,
radius (ActualWaveRegularity.particularChart.symm z) ∉
Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) →
(particularCopies l c u b G A j).common.amplitude n z = 0)
(n : ℕ)
:
theorem
NavierStokes.ActualWaveRegularityData.particular_phase_smooth
{B N0 : ℕ}
(l : ActualParticularStageControls.Label B N0)
(c : CorrectionState.Context (CorrectionStep.CycleSlow × TorusInverse.Plane))
(u : CorrectionState.State (CorrectionStep.CycleSlow × TorusInverse.Plane))
(b : CorrectionState.HarmonicBlock (CorrectionStep.CycleSlow × TorusInverse.Plane))
(G A : HarmonicResidual.BlockCoefficients (CorrectionStep.CycleSlow × TorusInverse.Plane))
(j : ℤ)
(hphase : (particularCopies l c u b G A j).background.phase = (ActualParticularStageControls.background l).phase)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) ((particularCopies l c u b G A j).background.phase n) particularPositive
theorem
NavierStokes.ActualWaveRegularityData.particular_mode_smooth
{B N0 : ℕ}
(l : ActualParticularStageControls.Label B N0)
(c : CorrectionState.Context (CorrectionStep.CycleSlow × TorusInverse.Plane))
(u : CorrectionState.State (CorrectionStep.CycleSlow × TorusInverse.Plane))
(b : CorrectionState.HarmonicBlock (CorrectionStep.CycleSlow × TorusInverse.Plane))
(G A : HarmonicResidual.BlockCoefficients (CorrectionStep.CycleSlow × TorusInverse.Plane))
(j : ℤ)
(hphase : (particularCopies l c u b G A j).background.phase = (ActualParticularStageControls.background l).phase)
{α : ℝ}
(ha :
WeightedClasses.MemClass particularFullStrip
(fun (x : ℕ) (z : ActualWaveRegularity.ParticularSpace) => √(particularFullStrip.zeta z)) α
(particularCopies l c u b G A j).common.amplitude)
(hz :
∀ (n : ℕ),
∀
z ∈
ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart
CorrectionInitialization.ActualPrimary.standardRegion,
radius (ActualWaveRegularity.particularChart.symm z) ∉
Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) →
(particularCopies l c u b G A j).common.amplitude n z = 0)
:
WaveStateRegularity.AngularSmooth
(PhysicalMeanDomain.slowDomain CorrectionInitialization.ActualPrimary.standardRegion.carrier)
(ActualWaveRegularity.modeOscillation (particularCopies l c u b G A j) particularFullStrip
(ActualParticularStageControls.canonicalParameters l).directions ActualWaveRegularity.particularChart)
theorem
NavierStokes.ActualWaveRegularityData.particular_mode_support
{B N0 : ℕ}
(l : ActualParticularStageControls.Label B N0)
(c : CorrectionState.Context (CorrectionStep.CycleSlow × TorusInverse.Plane))
(u : CorrectionState.State (CorrectionStep.CycleSlow × TorusInverse.Plane))
(b : CorrectionState.HarmonicBlock (CorrectionStep.CycleSlow × TorusInverse.Plane))
(G A : HarmonicResidual.BlockCoefficients (CorrectionStep.CycleSlow × TorusInverse.Plane))
(j : ℤ)
(hz :
∀ (n : ℕ),
∀
z ∈
ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart
CorrectionInitialization.ActualPrimary.standardRegion,
radius (ActualWaveRegularity.particularChart.symm z) ∉
Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) →
(particularCopies l c u b G A j).common.amplitude n z = 0)
:
WaveStateRegularity.WaveSupport CorrectionInitialization.ActualPrimary.standardRegion
(PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)
(ActualWaveRegularity.modeOscillation (particularCopies l c u b G A j) particularFullStrip
(ActualParticularStageControls.canonicalParameters l).directions ActualWaveRegularity.particularChart)
theorem
NavierStokes.ActualWaveRegularityData.particular_mode_pressure_smooth
{B N0 : ℕ}
(l : ActualParticularStageControls.Label B N0)
(c : CorrectionState.Context (CorrectionStep.CycleSlow × TorusInverse.Plane))
(u : CorrectionState.State (CorrectionStep.CycleSlow × TorusInverse.Plane))
(b : CorrectionState.HarmonicBlock (CorrectionStep.CycleSlow × TorusInverse.Plane))
(G A : HarmonicResidual.BlockCoefficients (CorrectionStep.CycleSlow × TorusInverse.Plane))
(j : ℤ)
(hphase : (particularCopies l c u b G A j).background.phase = (ActualParticularStageControls.background l).phase)
{β : ℝ}
(hp :
WeightedClasses.MemClass particularFullStrip
(fun (x : ℕ) (z : ActualWaveRegularity.ParticularSpace) => √(particularFullStrip.zeta z)) β
(particularCopies l c u b G A j).common.pressure)
(hzp :
∀ (n : ℕ),
∀
z ∈
ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart
CorrectionInitialization.ActualPrimary.standardRegion,
radius (ActualWaveRegularity.particularChart.symm z) ∉
Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) →
(particularCopies l c u b G A j).common.pressure n z = 0)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤)
(fun (x : ActualWaveRegularity.Cylinder) =>
(HarmonicCalculus.mode ((particularCopies l c u b G A j).background.frequency n)
((particularCopies l c u b G A j).background.phase n) ((particularCopies l c u b G A j).common.pressure n)
(ActualWaveRegularity.particularChart x)).re)
(ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion)
theorem
NavierStokes.ActualWaveRegularityData.particular_mode_periodic
{B N0 : ℕ}
(l : ActualParticularStageControls.Label B N0)
(c : CorrectionState.Context (CorrectionStep.CycleSlow × TorusInverse.Plane))
(u : CorrectionState.State (CorrectionStep.CycleSlow × TorusInverse.Plane))
(b : CorrectionState.HarmonicBlock (CorrectionStep.CycleSlow × TorusInverse.Plane))
(G A : HarmonicResidual.BlockCoefficients (CorrectionStep.CycleSlow × TorusInverse.Plane))
(j : ℤ)
(hphase : (particularCopies l c u b G A j).background.phase = (ActualParticularStageControls.background l).phase)
(hsource :
∀ (n : ℕ),
∀
z ∈
ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart
CorrectionInitialization.ActualPrimary.standardRegion,
CommonCoverSolve.PeriodicAt ((particularCopies l c u b G A j).source n) z.1)
(hzero :
∀ (n : ℕ),
¬Ordered (l.2, l.1) n →
∀
z ∈
ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart
CorrectionInitialization.ActualPrimary.standardRegion,
(particularCopies l c u b G A j).common.amplitude n =ᶠ[nhds z] fun (x : ActualWaveRegularity.ParticularSpace) =>
0)
:
Closed support and actual source continuity, unlike an interior norm bound alone, determine the literal values on the radial faces.
theorem
NavierStokes.ActualWaveRegularityData.zero_on_radial_faces
{E : Type}
[NormedAddCommGroup E]
{f : FullPoint → E}
(hf : ContinuousOn f (ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion))
(hz :
∀ x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion,
radius x ∉
Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) →
f x = 0)
{x : FullPoint}
(hx : x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion)
(ho :
radius x ∉
Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal))
:
theorem
NavierStokes.ActualWaveRegularityData.particular_zero_on_radial_faces
{E : Type}
[NormedAddCommGroup E]
{f : ActualWaveRegularity.ParticularSpace → E}
(hf :
ContinuousOn f
(ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart
CorrectionInitialization.ActualPrimary.standardRegion))
(hz :
∀
z ∈
ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart
CorrectionInitialization.ActualPrimary.standardRegion,
radius (ActualWaveRegularity.particularChart.symm z) ∉
Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) →
f z = 0)
{z : ActualWaveRegularity.ParticularSpace}
(hm :
z ∈ ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart
CorrectionInitialization.ActualPrimary.standardRegion)
(ho :
radius (ActualWaveRegularity.particularChart.symm z) ∉
Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal)
(PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal))
:
theorem
NavierStokes.ActualWaveRegularityData.common_pressure_translation
{D I : Type}
[NormedAddCommGroup D]
(a : PeriodizedWaveBounds.CopyData D I)
{Ω : Set D}
{v : D}
(n : ℕ)
(e : I ≃ I)
(hcut : ∀ (i : I), ∀ x ∈ Ω, a.cutoff n (e i) (x + v) = a.cutoff n i x)
(hp : ∀ (i : I), ∀ x ∈ Ω, a.pressure n (e i) (x + v) = a.pressure n i x)
:
ActualWaveRegularity.TranslationOn Ω v (a.common.pressure n)
theorem
NavierStokes.ActualWaveRegularityData.common_gaussian_translation
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(a : PeriodizedWaveBounds.CopyData D I)
(d : LinearWaveBounds.GraphDirections D)
{Ω : Set D}
{v : D}
(hΩ : IsOpen Ω)
(n : ℕ)
(e : I ≃ I)
(hcut : ∀ (i : I), ∀ x ∈ Ω, a.cutoff n (e i) (x + v) = a.cutoff n i x)
(ha : ∀ (i : I), ∀ x ∈ Ω, a.amplitude n (e i) (x + v) = a.amplitude n i x)
(hf : ActualWaveRegularity.TranslationOn Ω v (a.source n))
:
ActualWaveRegularity.TranslationOn Ω v (a.globalGaussian d n)
theorem
NavierStokes.ActualWaveRegularityData.signed_pressure_deck
{B N0 : ℕ}
(l : Index B N0)
(s : WeightedClasses.StripData Point)
(request : ℕ → FullPoint → SignedWaveUpdate.Vec2)
(n : ℕ)
(hn : Ordered l n)
(k m : TorusInverse.Frequency)
(x : FullPoint)
(hrequest : request n (x + ActualWaveRegularity.deckShift m) = request n x)
:
((ActualSignedStageControls.parameters l).copyData s request).pressure n ((deckPermutation l n m) k)
(x + ActualWaveRegularity.deckShift m) = ((ActualSignedStageControls.parameters l).copyData s request).pressure n k x
theorem
NavierStokes.ActualWaveRegularityData.signed_coefficient_translations
{B N0 : ℕ}
(l : Index B N0)
(P : SignedStressPrimitive.Patch)
(coord : ℝ)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(n : ℕ)
(hn : Ordered l n)
(m : TorusInverse.Frequency)
:
have a := signedCopies l (LocalSignedRequest.fullRequest ActualPrimaryBounds.strip P coord c u);
have Ω := ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion;
ActualWaveRegularity.TranslationOn Ω (ActualWaveRegularity.deckShift m) (a.common.amplitude n) ∧ ActualWaveRegularity.TranslationOn Ω (ActualWaveRegularity.deckShift m)
((a.commonCorrected ActualSignedStageControls.fullStrip
(ActualSignedStageControls.parameters l).directions).amplitude
n) ∧ ActualWaveRegularity.TranslationOn Ω (ActualWaveRegularity.deckShift m) (a.common.pressure n) ∧ ActualWaveRegularity.TranslationOn Ω (ActualWaveRegularity.deckShift m)
(a.globalGaussian (ActualSignedStageControls.parameters l).directions n)
Coefficient periods for the actual signed wave, before angular or finite-label assembly.
theorem
NavierStokes.ActualWaveRegularityData.particular_coefficient_translations
{B N0 : ℕ}
(l : ActualParticularStageControls.Label B N0)
(c : CorrectionState.Context (CorrectionStep.CycleSlow × TorusInverse.Plane))
(u : CorrectionState.State (CorrectionStep.CycleSlow × TorusInverse.Plane))
(b : CorrectionState.HarmonicBlock (CorrectionStep.CycleSlow × TorusInverse.Plane))
(G A : HarmonicResidual.BlockCoefficients (CorrectionStep.CycleSlow × TorusInverse.Plane))
(j : ℤ)
(hphase : (particularCopies l c u b G A j).background.phase = (ActualParticularStageControls.background l).phase)
(n : ℕ)
(hn : Ordered (l.2, l.1) n)
(m : TorusInverse.Frequency)
(hsource :
∀
z ∈
ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart
CorrectionInitialization.ActualPrimary.standardRegion,
CommonCoverSolve.PeriodicAt ((particularCopies l c u b G A j).source n) z.1)
:
have a := particularCopies l c u b G A j;
have Ω :=
ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart
CorrectionInitialization.ActualPrimary.standardRegion;
have v := ActualWaveRegularity.particularChart (ActualWaveRegularity.deckShift m);
ActualWaveRegularity.TranslationOn Ω v (a.common.amplitude n) ∧ ActualWaveRegularity.TranslationOn Ω v
((a.commonCorrected particularFullStrip
(ActualParticularStageControls.canonicalParameters l).directions).amplitude
n) ∧ ActualWaveRegularity.TranslationOn Ω v (a.common.pressure n) ∧ ActualWaveRegularity.TranslationOn Ω v
(a.globalGaussian (ActualParticularStageControls.canonicalParameters l).directions n)
The source callback is a per-label, complete-fiber statement. It is not replaced by periodicity of the total real oscillation.