Auxiliary periodicity of the actual correction coefficients #
The total velocity does not determine the periods of each stored harmonic coefficient. This module tracks the individual velocity, pressure and Gaussian coefficients on precisely the bands whose common cover is ordered. The differential residual preserves these periods on its open slow domain.
Deck translations of the actual wave-block coefficients #
Native coefficient translations pass through the literal angular section, finite harmonic sum, conjugate pairing, and coordinate reindexing. The particular source assumption is made on full native parameter fibers.
Point deck, given by (0, (0, TorusAverages.latticePoint k)).
Equations
Instances For
Native section, given by ActualWaveRegularity.particularChart (x, 0).
Equations
Instances For
theorem
NavierStokes.ActualWaveCoefficientPeriodicity.fullSection_translation
{E : Type}
{k : Frequency}
{f : FullPoint → E}
(hf :
ActualWaveRegularity.TranslationOn
(ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion)
(ActualWaveRegularity.deckShift k) f)
:
ActualWaveRegularity.TranslationOn ActualInitialization.geometry.domain (pointDeck k) fun (x : SignedMeanGain.Point) =>
f (x, 0)
theorem
NavierStokes.ActualWaveCoefficientPeriodicity.nativeSection_translation
{E : Type}
{k : Frequency}
{f : ActualWaveRegularity.ParticularSpace → E}
(hf :
ActualWaveRegularity.TranslationOn
(ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart
CorrectionInitialization.ActualPrimary.standardRegion)
(ActualWaveRegularity.particularChart (ActualWaveRegularity.deckShift k)) f)
:
ActualWaveRegularity.TranslationOn ActualInitialization.geometry.domain (pointDeck k) fun (x : SignedMeanGain.Point) =>
f (nativeSection x)
theorem
NavierStokes.ActualWaveCoefficientPeriodicity.conjugatePair_translation
{D : Type}
[NormedAddCommGroup D]
{Ω : Set D}
{shift : D}
{f : D → ℂ}
(hf : ActualWaveRegularity.TranslationOn Ω shift f)
(j m : ℤ)
:
ActualWaveRegularity.TranslationOn Ω shift ((ErrorHarmonics.conjugatePair j f).coeff m)
theorem
NavierStokes.ActualWaveCoefficientPeriodicity.assembled_velocity_translation
{D : Type}
[NormedAddCommGroup D]
{Ω : Set D}
{shift : D}
{E : Type}
(e : D → E)
(N : ℕ)
(frequency : ℕ → ℝ)
(phase : ℕ → E → ℝ)
(angular : ℕ → ℤ)
(v : ℤ → ℕ → E → HarmonicCalculus.ComplexVector)
(p : ℤ → ℕ → E → ℂ)
(n : ℕ)
(hv : ∀ j ∈ ParticularWaveAssembly.modes N, ActualWaveRegularity.TranslationOn Ω shift fun (x : D) => v j n (e x))
(i : Fin 3)
(m : ℤ)
:
ActualWaveRegularity.TranslationOn Ω shift fun (x : D) =>
((ParticularWaveAssembly.assembledBlock N frequency phase angular v p).velocity n i).coeff m (e x)
theorem
NavierStokes.ActualWaveCoefficientPeriodicity.assembled_pressure_translation
{D : Type}
[NormedAddCommGroup D]
{Ω : Set D}
{shift : D}
{E : Type}
(e : D → E)
(N : ℕ)
(frequency : ℕ → ℝ)
(phase : ℕ → E → ℝ)
(angular : ℕ → ℤ)
(v : ℤ → ℕ → E → HarmonicCalculus.ComplexVector)
(p : ℤ → ℕ → E → ℂ)
(n : ℕ)
(hp : ∀ j ∈ ParticularWaveAssembly.modes N, ActualWaveRegularity.TranslationOn Ω shift fun (x : D) => p j n (e x))
(m : ℤ)
:
ActualWaveRegularity.TranslationOn Ω shift fun (x : D) =>
((ParticularWaveAssembly.assembledBlock N frequency phase angular v p).pressure n).coeff m (e x)
noncomputable def
NavierStokes.ActualWaveCoefficientPeriodicity.particularData
{B N0 : ℕ}
(v : CorrectionStep.CycleCoefficients (Index B N0))
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(l : Index B N0)
(j : ℤ)
:
Particular data, given by ActualWaveRegularity.particularCopyData (ActualCycleParameters.fixedParameters B N0) v c u l j.
Equations
Instances For
theorem
NavierStokes.ActualWaveCoefficientPeriodicity.particular_phase
{B N0 : ℕ}
(v : CorrectionStep.CycleCoefficients (Index B N0))
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(l : Index B N0)
(hc : CorrectionStep.SameCarrier (v.blocks l) (ActualInitialization.tangentBlock l))
(j : ℤ)
:
(particularData v c u l j).background.phase = (ActualParticularStageControls.background (l.2, l.1)).phase
The incoming carrier is identified before applying the native translation theorem; no carrier of a solved wave is assumed.
noncomputable def
NavierStokes.ActualWaveCoefficientPeriodicity.NativeSourcesPeriodic
{B N0 : ℕ}
(v : CorrectionStep.CycleCoefficients (Index B N0))
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(l : Index B N0)
(n : ℕ)
:
The finite list of actual particular sources has its asserted periods on the complete native parameter fibers.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ActualWaveCoefficientPeriodicity.particular_coefficients
{B N0 : ℕ}
(v : CorrectionStep.CycleCoefficients (Index B N0))
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(l : Index B N0)
(n : ℕ)
(hn : ActualWaveRegularityData.Ordered l n)
(k : Frequency)
(hc : CorrectionStep.SameCarrier (v.blocks l) (ActualInitialization.tangentBlock l))
(hsource : NativeSourcesPeriodic v c u l n)
:
(∀ (i : Fin 3) (m : ℤ),
ActualWaveRegularity.TranslationOn ActualInitialization.geometry.domain (pointDeck k)
((((ActualCycleParameters.fixedParameters B N0).particularBlock v c u l).velocity n i).coeff m)) ∧ (∀ (m : ℤ),
ActualWaveRegularity.TranslationOn ActualInitialization.geometry.domain (pointDeck k)
((((ActualCycleParameters.fixedParameters B N0).particularBlock v c u l).pressure n).coeff m)) ∧ ∀ (i : Fin 3) (m : ℤ),
ActualWaveRegularity.TranslationOn ActualInitialization.geometry.domain (pointDeck k)
((((ActualCycleParameters.fixedParameters B N0).particularGaussianBlock v c u l).velocity n i).coeff m)
Ordered-band periods of the literal particular block and its Gaussian block, including every Fourier coefficient rather than only real fields.
theorem
NavierStokes.ActualWaveCoefficientPeriodicity.signed_coefficients
{B N0 : ℕ}
(v : CorrectionStep.CycleCoefficients (Index B N0))
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(l : Index B N0)
(n : ℕ)
(hn : ActualWaveRegularityData.Ordered l n)
(k : Frequency)
:
(∀ (i : Fin 3) (m : ℤ),
ActualWaveRegularity.TranslationOn ActualInitialization.geometry.domain (pointDeck k)
((((ActualCycleParameters.fixedParameters B N0).signedBlock v c u l).velocity n i).coeff m)) ∧ (∀ (m : ℤ),
ActualWaveRegularity.TranslationOn ActualInitialization.geometry.domain (pointDeck k)
((((ActualCycleParameters.fixedParameters B N0).signedBlock v c u l).pressure n).coeff m)) ∧ ∀ (i : Fin 3) (m : ℤ),
ActualWaveRegularity.TranslationOn ActualInitialization.geometry.domain (pointDeck k)
((((ActualCycleParameters.fixedParameters B N0).signedGaussianBlock v c u l).velocity n i).coeff m)
The actual signed request gives the native periods directly; no periodicity assumption on an output block or on a freely supplied request is needed.
Torus periodicity of the actual seed coefficients #
The common cover is required to precede the fixed physical label's native cover. Under this ordering, the actual exact-curl velocity, pressure, and retained Gaussian coefficients are invariant under every torus deck shift.
The deck shift on the full free lift, leaving radius and slow variables unchanged. This is definitionally the shift used by the seed continuation.
Equations
Instances For
theorem
NavierStokes.ActualSeedPeriodicity.zeroSlice_add_deck
(k : TorusInverse.Frequency)
(x : Point)
:
theorem
NavierStokes.ActualSeedPeriodicity.conjugatePair_periodic
{E : Type}
[NormedAddCommGroup E]
(f : E → ℂ)
(w : E)
(hf : ∀ (x : E), f (x + w) = f x)
(j : ℤ)
(x : E)
:
theorem
NavierStokes.ActualSeedPeriodicity.phase_periodic
{B N0 : ℕ}
(l : ActualInitialization.Index B N0)
(n : ℕ)
(hn : ActualWaveRegularityData.Ordered l n)
(k : TorusInverse.Frequency)
(x : Point)
:
The stored phase uses the same ordered common cover.
theorem
NavierStokes.ActualSeedPeriodicity.primary_velocity_periodic
{B N0 : ℕ}
(l : ActualInitialization.Index B N0)
(n : ℕ)
(hn : ActualWaveRegularityData.Ordered l n)
(i : Fin 3)
(j : ℤ)
(k : TorusInverse.Frequency)
(x : Point)
:
((ActualInitialization.primaryBlock l).velocity n i).coeff j (x + pointDeck k) = ((ActualInitialization.primaryBlock l).velocity n i).coeff j x
Every harmonic coefficient of the actual exact-curl seed velocity is periodic, including the conjugate mode.
theorem
NavierStokes.ActualSeedPeriodicity.primary_pressure_periodic
{B N0 : ℕ}
(l : ActualInitialization.Index B N0)
(n : ℕ)
(hn : ActualWaveRegularityData.Ordered l n)
(j : ℤ)
(k : TorusInverse.Frequency)
(x : Point)
:
((ActualInitialization.primaryBlock l).pressure n).coeff j (x + pointDeck k) = ((ActualInitialization.primaryBlock l).pressure n).coeff j x
The pressure coefficient contains the actual cutoff and the same conjugate-pair normalization as the seed.
theorem
NavierStokes.ActualSeedPeriodicity.gaussian_velocity_periodic
{B N0 : ℕ}
(l : ActualInitialization.Index B N0)
(n : ℕ)
(hn : ActualWaveRegularityData.Ordered l n)
(i : Fin 3)
(j : ℤ)
(k : TorusInverse.Frequency)
(x : Point)
:
((ActualInitialization.gaussianBlock l).velocity n i).coeff j (x + pointDeck k) = ((ActualInitialization.gaussianBlock l).velocity n i).coeff j x
The Gaussian error is kept as its differentiated cutoff coefficient. Its invariance follows by translating that derivative, not by deleting it.
Translation calculus for finite harmonic coefficients.
def
NavierStokes.ActualCyclePeriodicity.CoefficientsTranslation
{D : Type}
[NormedAddCommGroup D]
(U : Set D)
(v : D)
(a : HarmonicFields.Coefficients D)
:
Coefficients translation, given by ∀ j, TranslationOn U v (a j).
Equations
- NavierStokes.ActualCyclePeriodicity.CoefficientsTranslation U v a = ∀ (j : ℤ), NavierStokes.ActualWaveRegularity.TranslationOn U v (a.coeff j)
Instances For
theorem
NavierStokes.ActualCyclePeriodicity.CoefficientsTranslation.zero
{D : Type}
[NormedAddCommGroup D]
{U : Set D}
{v : D}
:
CoefficientsTranslation U v 0
theorem
NavierStokes.ActualCyclePeriodicity.CoefficientsTranslation.add
{D : Type}
[NormedAddCommGroup D]
{U : Set D}
{v : D}
{a b : HarmonicFields.Coefficients D}
(ha : CoefficientsTranslation U v a)
(hb : CoefficientsTranslation U v b)
:
CoefficientsTranslation U v (a + b)
theorem
NavierStokes.ActualCyclePeriodicity.CoefficientsTranslation.neg
{D : Type}
[NormedAddCommGroup D]
{U : Set D}
{v : D}
{a : HarmonicFields.Coefficients D}
(ha : CoefficientsTranslation U v a)
:
CoefficientsTranslation U v (-a)
theorem
NavierStokes.ActualCyclePeriodicity.CoefficientsTranslation.sub
{D : Type}
[NormedAddCommGroup D]
{U : Set D}
{v : D}
{a b : HarmonicFields.Coefficients D}
(ha : CoefficientsTranslation U v a)
(hb : CoefficientsTranslation U v b)
:
CoefficientsTranslation U v (a - b)
theorem
NavierStokes.ActualCyclePeriodicity.CoefficientsTranslation.mul
{D : Type}
[NormedAddCommGroup D]
{U : Set D}
{v : D}
{a b : HarmonicFields.Coefficients D}
(ha : CoefficientsTranslation U v a)
(hb : CoefficientsTranslation U v b)
:
CoefficientsTranslation U v (a * b)
theorem
NavierStokes.ActualCyclePeriodicity.CoefficientsTranslation.boundConstant
{D : Type}
[NormedAddCommGroup D]
{U : Set D}
{v : D}
{f : D → ℂ}
(hf : ActualWaveRegularity.TranslationOn U v f)
:
theorem
NavierStokes.ActualCyclePeriodicity.CoefficientsTranslation.differentiate
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{U : Set D}
{v : D}
{a : HarmonicFields.Coefficients D}
(ha : CoefficientsTranslation U v a)
(hU : IsOpen U)
{V : D → D}
{Φ : D → ℝ}
(hV : ActualWaveRegularity.TranslationOn U v V)
(hΦ : ActualWaveRegularity.TranslationOn U v Φ)
(k : ℝ)
:
CoefficientsTranslation U v (HarmonicFields.differentiate V k Φ a)
theorem
NavierStokes.ActualCyclePeriodicity.CoefficientsTranslation.angular
{D : Type}
[NormedAddCommGroup D]
{U : Set D}
{v : D}
{a : HarmonicFields.Coefficients D}
(ha : CoefficientsTranslation U v a)
(k : ℤ)
:
theorem
NavierStokes.ActualCyclePeriodicity.CoefficientsTranslation.realProjection
{D : Type}
[NormedAddCommGroup D]
{U : Set D}
{v : D}
{a : HarmonicFields.Coefficients D}
(ha : CoefficientsTranslation U v a)
:
theorem
NavierStokes.ActualCyclePeriodicity.CoefficientsTranslation.nonconstant
{D : Type}
[NormedAddCommGroup D]
{U : Set D}
{v : D}
{a : HarmonicFields.Coefficients D}
(ha : CoefficientsTranslation U v a)
:
theorem
NavierStokes.ActualCyclePeriodicity.CoefficientsTranslation.sum
{D : Type}
[NormedAddCommGroup D]
{U : Set D}
{v : D}
{ι : Type}
(s : Finset ι)
(f : ι → HarmonicFields.Coefficients D)
(hf : ∀ i ∈ s, CoefficientsTranslation U v (f i))
:
CoefficientsTranslation U v (∑ i ∈ s, f i)
theorem
NavierStokes.ActualCyclePeriodicity.CoefficientsTranslation.field
{D : Type}
[NormedAddCommGroup D]
{U : Set D}
{v : D}
{a : HarmonicFields.Coefficients D}
(ha : CoefficientsTranslation U v a)
{Φ : D → ℝ}
(hΦ : ActualWaveRegularity.TranslationOn U v Φ)
(k : ℝ)
(kp : ℤ)
(θ : ℝ)
:
ActualWaveRegularity.TranslationOn U v fun (x : D) => HarmonicFields.field a k Φ kp (x, θ)
structure
NavierStokes.ActualCyclePeriodicity.FrameTranslation
{D : Type}
[NormedAddCommGroup D]
(U : Set D)
(v : D)
(g : HarmonicResidual.Frame D)
:
Frame translation data, collecting radius, radial, axial, time.
- radius : ActualWaveRegularity.TranslationOn U v g.radius
- radial : ActualWaveRegularity.TranslationOn U v g.radial
- axial : ActualWaveRegularity.TranslationOn U v g.axial
- time : ActualWaveRegularity.TranslationOn U v g.time
Instances For
theorem
NavierStokes.ActualCyclePeriodicity.FrameTranslation.scalarLaplacian
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{U : Set D}
{v : D}
{g : HarmonicResidual.Frame D}
(hg : FrameTranslation U v g)
(hU : IsOpen U)
{Φ : D → ℝ}
(hΦ : ActualWaveRegularity.TranslationOn U v Φ)
(k : ℝ)
(kp : ℤ)
{a : HarmonicFields.Coefficients D}
(ha : CoefficientsTranslation U v a)
:
CoefficientsTranslation U v (HarmonicResidual.scalarLaplacian g k Φ kp a)
theorem
NavierStokes.ActualCyclePeriodicity.FrameTranslation.rotate
{D : Type}
[NormedAddCommGroup D]
{U : Set D}
{v : D}
{a : HarmonicResidual.VectorCoefficients D}
(ha : ∀ (i : Fin 3), CoefficientsTranslation U v (a i))
(i : Fin 3)
:
theorem
NavierStokes.ActualCyclePeriodicity.FrameTranslation.vectorLaplacian
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{U : Set D}
{v : D}
{g : HarmonicResidual.Frame D}
(hg : FrameTranslation U v g)
(hU : IsOpen U)
{Φ : D → ℝ}
(hΦ : ActualWaveRegularity.TranslationOn U v Φ)
(k : ℝ)
(kp : ℤ)
{a : HarmonicResidual.VectorCoefficients D}
(ha : ∀ (i : Fin 3), CoefficientsTranslation U v (a i))
(i : Fin 3)
:
CoefficientsTranslation U v (HarmonicResidual.vectorLaplacian g k Φ kp a i)
theorem
NavierStokes.ActualCyclePeriodicity.FrameTranslation.transport
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{U : Set D}
{v : D}
{g : HarmonicResidual.Frame D}
(hg : FrameTranslation U v g)
(hU : IsOpen U)
{Φ : D → ℝ}
(hΦ : ActualWaveRegularity.TranslationOn U v Φ)
(k : ℝ)
(kp : ℤ)
{a b : HarmonicResidual.VectorCoefficients D}
(ha : ∀ (i : Fin 3), CoefficientsTranslation U v (a i))
(hb : ∀ (i : Fin 3), CoefficientsTranslation U v (b i))
(i : Fin 3)
:
CoefficientsTranslation U v (HarmonicResidual.transport g k Φ kp a b i)
theorem
NavierStokes.ActualCyclePeriodicity.FrameTranslation.gradient
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{U : Set D}
{v : D}
{g : HarmonicResidual.Frame D}
(hg : FrameTranslation U v g)
(hU : IsOpen U)
{Φ : D → ℝ}
(hΦ : ActualWaveRegularity.TranslationOn U v Φ)
(k : ℝ)
(kp : ℤ)
{p : HarmonicFields.Coefficients D}
(hp : CoefficientsTranslation U v p)
(i : Fin 3)
:
CoefficientsTranslation U v (HarmonicResidual.gradient g k Φ kp p i)
theorem
NavierStokes.ActualCyclePeriodicity.FrameTranslation.linearResidual
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{U : Set D}
{v : D}
{g : HarmonicResidual.Frame D}
(hg : FrameTranslation U v g)
(hU : IsOpen U)
{Φ : D → ℝ}
(hΦ : ActualWaveRegularity.TranslationOn U v Φ)
(k : ℝ)
(kp : ℤ)
{B a : HarmonicResidual.VectorCoefficients D}
{p : HarmonicFields.Coefficients D}
(hB : ∀ (i : Fin 3), CoefficientsTranslation U v (B i))
(ha : ∀ (i : Fin 3), CoefficientsTranslation U v (a i))
(hp : CoefficientsTranslation U v p)
(i : Fin 3)
:
CoefficientsTranslation U v (HarmonicResidual.linearResidual g k Φ kp B a p i)
theorem
NavierStokes.ActualCyclePeriodicity.FrameTranslation.nonlinearResidual
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{U : Set D}
{v : D}
{g : HarmonicResidual.Frame D}
(hg : FrameTranslation U v g)
(hU : IsOpen U)
{Φ : D → ℝ}
(hΦ : ActualWaveRegularity.TranslationOn U v Φ)
(k : ℝ)
(kp : ℤ)
{B a : HarmonicResidual.VectorCoefficients D}
{p : HarmonicFields.Coefficients D}
(hB : ∀ (i : Fin 3), CoefficientsTranslation U v (B i))
(ha : ∀ (i : Fin 3), CoefficientsTranslation U v (a i))
(hp : CoefficientsTranslation U v p)
(i : Fin 3)
:
CoefficientsTranslation U v (HarmonicResidual.nonlinearResidual g k Φ kp B a p i)
theorem
NavierStokes.ActualCyclePeriodicity.residualSource_translation
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{U : Set D}
{v : D}
(hU : IsOpen U)
(c : CorrectionState.Context D)
(u : CorrectionState.State D)
(b : CorrectionState.HarmonicBlock D)
(G A : HarmonicResidual.BlockCoefficients D)
(n : ℕ)
(hg : FrameTranslation U v (HarmonicResidual.contextFrame c n))
(hB : ActualWaveRegularity.TranslationOn U v (HarmonicResidual.contextBase c n))
(hM : ActualWaveRegularity.TranslationOn U v (HarmonicResidual.stateMean u n))
(hΦ : ActualWaveRegularity.TranslationOn U v (b.phase n))
(hv : ∀ (i : Fin 3), CoefficientsTranslation U v (b.velocity n i))
(hp : CoefficientsTranslation U v (b.pressure n))
(hG : ∀ (i : Fin 3), CoefficientsTranslation U v (G n i))
(hA : ∀ (i : Fin 3), CoefficientsTranslation U v (A n i))
(j : ℤ)
:
ActualWaveRegularity.TranslationOn U v (ParticularWaveAssembly.residualSource c u b G A j n)
The actual finite residual, including both excluded-error inputs, commutes with a translation when its primitive data do.
The separately carried periodicity invariant.
Point deck, given by (0, (0, TorusAverages.latticePoint k)).
Equations
Instances For
theorem
NavierStokes.ActualCyclePeriodicity.add_pointDeck
(z : Point)
(k : TorusInverse.Frequency)
:
structure
NavierStokes.ActualCyclePeriodicity.Periodic
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Index B N0))
:
Periodic data, collecting velocity, pressure, gaussian.
- velocity (l : ActualWaveRegularityData.Index B N0) (n : ℕ) : ActualWaveRegularityData.Ordered l n → ∀ (k : TorusInverse.Frequency) (i : Fin 3), CoefficientsTranslation ActualInitialization.geometry.domain (pointDeck k) ((x.coefficients.blocks l).velocity n i)
- pressure (l : ActualWaveRegularityData.Index B N0) (n : ℕ) : ActualWaveRegularityData.Ordered l n → ∀ (k : TorusInverse.Frequency), CoefficientsTranslation ActualInitialization.geometry.domain (pointDeck k) ((x.coefficients.blocks l).pressure n)
- gaussian (l : ActualWaveRegularityData.Index B N0) (n : ℕ) : ActualWaveRegularityData.Ordered l n → ∀ (k : TorusInverse.Frequency) (i : Fin 3), CoefficientsTranslation ActualInitialization.geometry.domain (pointDeck k) (x.coefficients.gaussian l n i)
Instances For
The literal initialized state has every auxiliary period required below.
theorem
NavierStokes.ActualCyclePeriodicity.Periodic.step_of_waves
{B N0 : ℕ}
{x : CorrectionStep.CycleState (Index B N0)}
(h : Periodic x)
(p : CorrectionStep.CycleParameters (Index B N0))
(c : CorrectionState.Context Point)
(hp :
∀ (l : ActualWaveRegularityData.Index B N0) (n : ℕ),
ActualWaveRegularityData.Ordered l n →
∀ (k : TorusInverse.Frequency),
(∀ (i : Fin 3),
CoefficientsTranslation ActualInitialization.geometry.domain (pointDeck k)
((p.particularBlock x.coefficients c x.state l).velocity n i)) ∧ CoefficientsTranslation ActualInitialization.geometry.domain (pointDeck k)
((p.particularBlock x.coefficients c x.state l).pressure n) ∧ ∀ (i : Fin 3),
CoefficientsTranslation ActualInitialization.geometry.domain (pointDeck k)
((p.particularGaussianBlock x.coefficients c x.state l).velocity n i))
(hs :
∀ (l : ActualWaveRegularityData.Index B N0) (n : ℕ),
ActualWaveRegularityData.Ordered l n →
∀ (k : TorusInverse.Frequency),
(∀ (i : Fin 3),
CoefficientsTranslation ActualInitialization.geometry.domain (pointDeck k)
((p.signedBlock x.coefficients c x.state l).velocity n i)) ∧ CoefficientsTranslation ActualInitialization.geometry.domain (pointDeck k)
((p.signedBlock x.coefficients c x.state l).pressure n) ∧ ∀ (i : Fin 3),
CoefficientsTranslation ActualInitialization.geometry.domain (pointDeck k)
((p.signedGaussianBlock x.coefficients c x.state l).velocity n i))
:
Addition of the two actual wave increments preserves the coefficient periods. The mean and axisymmetric updates do not alter these coefficients.
theorem
NavierStokes.ActualCyclePeriodicity.domain_deck
(k : TorusInverse.Frequency)
{z : Point}
(hz : z ∈ ActualInitialization.geometry.domain)
:
theorem
NavierStokes.ActualCyclePeriodicity.state_mean_translation
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
{P : Index B N0 → ℕ → Point → ℝ}
{S : Index B N0 → ℕ → Set Point}
(H :
CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry
(CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock P S σ x)
(n : ℕ)
(k : TorusInverse.Frequency)
:
theorem
NavierStokes.ActualCyclePeriodicity.state_phase_translation
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
{P : Index B N0 → ℕ → Point → ℝ}
{S : Index B N0 → ℕ → Set Point}
(H :
CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry
(CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock P S σ x)
(l : Index B N0)
(n : ℕ)
(hn : ActualWaveRegularityData.Ordered l n)
(k : TorusInverse.Frequency)
:
theorem
NavierStokes.ActualCyclePeriodicity.fields_ordered
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
{P : Index B N0 → ℕ → Point → ℝ}
{S : Index B N0 → ℕ → Set Point}
(H :
CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry
(CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock P S σ x)
(h : Periodic x)
(l : Index B N0)
(n : ℕ)
(hn : ActualWaveRegularityData.Ordered l n)
(k : TorusInverse.Frequency)
(θ : ℝ)
:
(ActualWaveRegularity.TranslationOn ActualInitialization.geometry.domain (pointDeck k) fun (z : SignedMeanGain.Point) =>
(x.coefficients.blocks l).oscillation n (z, θ)) ∧ (ActualWaveRegularity.TranslationOn ActualInitialization.geometry.domain (pointDeck k)
fun (z : SignedMeanGain.Point) => (x.coefficients.blocks l).oscillatoryPressure n (z, θ)) ∧ ActualWaveRegularity.TranslationOn ActualInitialization.geometry.domain (pointDeck k)
fun (z : SignedMeanGain.Point) =>
CorrectionStep.coefficientField (x.coefficients.blocks l) (x.coefficients.gaussian l) n (z, θ)
The per-label real velocity, pressure, and retained Gaussian field have the same periods as their literal coefficients.
theorem
NavierStokes.ActualCyclePeriodicity.source_ordered
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
{P : Index B N0 → ℕ → Point → ℝ}
{S : Index B N0 → ℕ → Set Point}
(H :
CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry
(CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock P S σ x)
(h : Periodic x)
(l : Index B N0)
(n : ℕ)
(hn : ActualWaveRegularityData.Ordered l n)
(j : ℤ)
(k : TorusInverse.Frequency)
:
Every actual residual coefficient has the common periods on an ordered band. This uses the separate per-label hypotheses, not merely the total velocity.
theorem
NavierStokes.ActualCyclePeriodicity.source_all
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
{P : Index B N0 → ℕ → Point → ℝ}
{S : Index B N0 → ℕ → Set Point}
(H :
CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry
(CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock P S σ x)
(h : Periodic x)
(hzero :
∀ (l : ActualWaveRegularityData.Index B N0) (n : ℕ),
¬ActualWaveRegularityData.Ordered l n →
∀ (j : ℤ),
∀ z ∈ ActualInitialization.geometry.domain,
ParticularWaveAssembly.residualSource (CorrectionInitialization.ActualPrimary.commonContext B) x.state
(x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l) j n z = 0)
(l : Index B N0)
(n : ℕ)
(j : ℤ)
(k : TorusInverse.Frequency)
:
The literal source, with the associator used by the particular solver.
noncomputable def
NavierStokes.ActualCyclePeriodicity.copies
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Index B N0))
(l : Index B N0)
(j : ℤ)
:
Copies, constructed using ActualWaveRegularityData.particularCopies.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ActualCyclePeriodicity.copies_source
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Index B N0))
(l : Index B N0)
(j : ℤ)
(n : ℕ)
(z : ActualWaveRegularity.ParticularSpace)
:
(copies x l j).source n z = ParticularWaveAssembly.residualSource (CorrectionInitialization.ActualPrimary.commonContext B) x.state
(x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l) j n
(ActualWaveRegularity.particularChart.symm z).1
theorem
NavierStokes.ActualCyclePeriodicity.copies_source_ordered
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
{P : Index B N0 → ℕ → Point → ℝ}
{S : Index B N0 → ℕ → Set Point}
(H :
CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry
(CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock P S σ x)
(h : Periodic x)
(l : Index B N0)
(n : ℕ)
(hn : ActualWaveRegularityData.Ordered l n)
(j : ℤ)
(z : ActualWaveRegularity.ParticularSpace)
(hz :
z ∈ ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart
CorrectionInitialization.ActualPrimary.standardRegion)
:
CommonCoverSolve.PeriodicAt ((copies x l j).source n) z.1
theorem
NavierStokes.ActualCyclePeriodicity.copies_source_periodic
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
{P : Index B N0 → ℕ → Point → ℝ}
{S : Index B N0 → ℕ → Set Point}
(H :
CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry
(CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock P S σ x)
(h : Periodic x)
(hzero :
∀ (l : ActualWaveRegularityData.Index B N0) (n : ℕ),
¬ActualWaveRegularityData.Ordered l n →
∀ (j : ℤ),
∀ z ∈ ActualInitialization.geometry.domain,
ParticularWaveAssembly.residualSource (CorrectionInitialization.ActualPrimary.commonContext B) x.state
(x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l) j n z = 0)
(l : Index B N0)
(j : ℤ)
(n : ℕ)
(z : ActualWaveRegularity.ParticularSpace)
(hz :
z ∈ ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart
CorrectionInitialization.ActualPrimary.standardRegion)
:
CommonCoverSolve.PeriodicAt ((copies x l j).source n) z.1
The complete source callback required by the actual particular-copy solver. Unordered bands are supplied by the independent support/zero-germ argument.
theorem
NavierStokes.ActualCyclePeriodicity.native_sources_periodic
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
{P : Index B N0 → ℕ → Point → ℝ}
{S : Index B N0 → ℕ → Set Point}
(H :
CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry
(CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock P S σ x)
(h : Periodic x)
(l : Index B N0)
(n : ℕ)
(hn : ActualWaveRegularityData.Ordered l n)
:
theorem
NavierStokes.ActualCyclePeriodicity.step
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
{P : Index B N0 → ℕ → Point → ℝ}
{S : Index B N0 → ℕ → Set Point}
(H :
CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry
(CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock P S σ x)
(h : Periodic x)
:
The literal four-stage cycle preserves the auxiliary periodicity invariant. Both increments are the actual constructed waves, and their source-periodicity premises are proved from the incoming coefficients.