Constructed signed wave increments #
The signed coefficient is the inverse of the same integrated primary matrix, divided by twice the same positive primary amplitude. Its sign is unrestricted. The homogeneous pressure, exact curl, signed square, and slot-cutoff error are retained as actual fields.
Explicit harmonic witnesses for the retained error fields #
Every representation in this file is constructed from its source field. Gaussian errors retain the original carrier and its conjugate, while actual mean aliases occupy the zero mode. No full-residual identity is assumed.
Conjugate pair as an element of Coefficients D.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ErrorHarmonics.evaluate_conjugatePair
{D : Type}
(j : ℤ)
(a : D → ℂ)
(x : D)
(φ : ℝ)
:
theorem
NavierStokes.ErrorHarmonics.field_conjugatePair
{D : Type}
(j : ℤ)
(a : D → ℂ)
(k : ℝ)
(Φ : D → ℝ)
(kp : ℤ)
(p : D × ℝ)
:
HarmonicFields.field (conjugatePair j a) k Φ kp p = ↑(a p.1 * HarmonicFields.character j (k * Φ p.1 + ↑kp * p.2)).re
theorem
NavierStokes.ErrorHarmonics.band_conjugateReverse
{D : Type}
{c : HarmonicFields.Coefficients D}
{N : ℕ}
(hc : HarmonicFields.BandLimited c N)
:
noncomputable def
NavierStokes.ErrorHarmonics.pairedBlock
{D : Type}
(j : ℤ)
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
(a : ℕ → D → HarmonicCalculus.ComplexVector)
:
Paired block, bundling velocity, pressure, frequency, phase and the required
compatibility proofs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ErrorHarmonics.pairedBlock_band
{D : Type}
(j : ℤ)
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
(a : ℕ → D → HarmonicCalculus.ComplexVector)
:
(pairedBlock j k Φ kp a).BandLimited j.natAbs
theorem
NavierStokes.ErrorHarmonics.pairedBlock_symmetric
{D : Type}
(j : ℤ)
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
(a : ℕ → D → HarmonicCalculus.ComplexVector)
(n : ℕ)
(i : Fin 3)
:
HarmonicFields.ConjugateSymmetric ((pairedBlock j k Φ kp a).velocity n i)
theorem
NavierStokes.ErrorHarmonics.pairedBlock_evaluation
{D : Type}
(j : ℤ)
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
(a : ℕ → D → HarmonicCalculus.ComplexVector)
(n : ℕ)
(p : D × ℝ)
(i : Fin 3)
:
(pairedBlock j k Φ kp a).oscillation n p i = (a n p.1 i * HarmonicFields.character j (k n * Φ n p.1 + ↑(kp n) * p.2)).re
noncomputable def
NavierStokes.ErrorHarmonics.zeroBlock
{D : Type}
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
(a : CorrectionState.MeanVector D)
:
Zero block, bundling velocity, pressure, frequency, phase and the required
compatibility proofs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ErrorHarmonics.zeroBlock_band
{D : Type}
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
(a : CorrectionState.MeanVector D)
:
(zeroBlock k Φ kp a).BandLimited 0
theorem
NavierStokes.ErrorHarmonics.zeroBlock_symmetric
{D : Type}
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
(a : CorrectionState.MeanVector D)
(n : ℕ)
(i : Fin 3)
:
HarmonicFields.ConjugateSymmetric ((zeroBlock k Φ kp a).velocity n i)
theorem
NavierStokes.ErrorHarmonics.dfast_angleIndependent
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(d : LinearWaveBounds.GraphDirections (D × ℝ))
{ψ : ℕ → D × ℝ → ℝ}
(hψ : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (ψ n))
(hψa : AngleIndependent ψ)
:
AngleIndependent (d.Dfast ψ)
theorem
NavierStokes.ErrorHarmonics.excludedSlotError_angleIndependent
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(d : LinearWaveBounds.GraphDirections (D × ℝ))
{ψ : ℕ → D × ℝ → ℝ}
{a source : ℕ → D × ℝ → HarmonicCalculus.ComplexVector}
(hψ : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (ψ n))
(hψa : AngleIndependent ψ)
(ha : AngleIndependent a)
(hs : AngleIndependent source)
:
AngleIndependent (LinearWaveBounds.excludedSlotError d ψ a source)
theorem
NavierStokes.ErrorHarmonics.slot_coordinate_angleIndependent
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData (D × ℝ)}
(g : GaussianTailFlat.SlotFamily s)
(hangle : ∀ (n : ℕ), (g.linear n) (0, 1) = 0)
:
theorem
NavierStokes.ErrorHarmonics.slot_cutoff_angleIndependent
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData (D × ℝ)}
(g : GaussianTailFlat.SlotFamily s)
(hangle : ∀ (n : ℕ), (g.linear n) (0, 1) = 0)
:
noncomputable def
NavierStokes.ErrorHarmonics.gaussianField
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(d : LinearWaveBounds.GraphDirections (D × ℝ))
(ψ : ℕ → D × ℝ → ℝ)
(a source : ℕ → D × ℝ → HarmonicCalculus.ComplexVector)
(j : ℤ)
(k : ℕ → ℝ)
(Ψ : ℕ → D × ℝ → ℝ)
:
The retained Gaussian term as a literal real carrier field.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.ErrorHarmonics.gaussianBlock
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(d : LinearWaveBounds.GraphDirections (D × ℝ))
(ψ : ℕ → D × ℝ → ℝ)
(a source : ℕ → D × ℝ → HarmonicCalculus.ComplexVector)
(j : ℤ)
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
:
Gaussian block, given by pairedBlock j k Φ kp (fun n x => LinearWaveBounds.excludedSlotError d ψ a source n (x, 0)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ErrorHarmonics.gaussianBlock_metadata
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(d : LinearWaveBounds.GraphDirections (D × ℝ))
(ψ : ℕ → D × ℝ → ℝ)
(a source : ℕ → D × ℝ → HarmonicCalculus.ComplexVector)
(j : ℤ)
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
:
(gaussianBlock d ψ a source j k Φ kp).frequency = k ∧ (gaussianBlock d ψ a source j k Φ kp).phase = Φ ∧ (gaussianBlock d ψ a source j k Φ kp).angularFrequency = kp
theorem
NavierStokes.ErrorHarmonics.gaussianBlock_band
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(d : LinearWaveBounds.GraphDirections (D × ℝ))
(ψ : ℕ → D × ℝ → ℝ)
(a source : ℕ → D × ℝ → HarmonicCalculus.ComplexVector)
(j : ℤ)
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
:
(gaussianBlock d ψ a source j k Φ kp).BandLimited j.natAbs
theorem
NavierStokes.ErrorHarmonics.gaussianBlock_symmetric
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(d : LinearWaveBounds.GraphDirections (D × ℝ))
(ψ : ℕ → D × ℝ → ℝ)
(a source : ℕ → D × ℝ → HarmonicCalculus.ComplexVector)
(j : ℤ)
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
(n : ℕ)
(i : Fin 3)
:
HarmonicFields.ConjugateSymmetric ((gaussianBlock d ψ a source j k Φ kp).velocity n i)
theorem
NavierStokes.ErrorHarmonics.gaussianBlock_represents
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(d : LinearWaveBounds.GraphDirections (D × ℝ))
{ψ : ℕ → D × ℝ → ℝ}
{a source : ℕ → D × ℝ → HarmonicCalculus.ComplexVector}
(j : ℤ)
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(Ψ : ℕ → D × ℝ → ℝ)
(kp : ℕ → ℤ)
(hψ : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (ψ n))
(hψa : AngleIndependent ψ)
(ha : AngleIndependent a)
(hs : AngleIndependent source)
(hphase : ∀ (n : ℕ) (x : D) (θ : ℝ), k n * Ψ n (x, θ) = k n * Φ n x + ↑(kp n) * θ)
:
The witness evaluates to the actual error, from primitive angular independence and the actual phase identity. No error representation is assumed.
theorem
NavierStokes.ErrorHarmonics.gaussianSlotBlock_represents
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData (D × ℝ)}
(g : GaussianTailFlat.SlotFamily s)
(d : LinearWaveBounds.GraphDirections (D × ℝ))
{a source : ℕ → D × ℝ → HarmonicCalculus.ComplexVector}
(j : ℤ)
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(Ψ : ℕ → D × ℝ → ℝ)
(kp : ℕ → ℤ)
(hangle : ∀ (n : ℕ), (g.linear n) (0, 1) = 0)
(ha : AngleIndependent a)
(hs : AngleIndependent source)
(hphase : ∀ (n : ℕ) (x : D) (θ : ℝ), k n * Ψ n (x, θ) = k n * Φ n x + ↑(kp n) * θ)
:
The affine Gaussian slot profile supplies the cutoff invariance itself.
theorem
NavierStokes.ErrorHarmonics.gaussianField_eq_gaussianTailError
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData (D × ℝ)}
(g : GaussianTailFlat.SlotFamily s)
(d : LinearWaveBounds.GraphDirections (D × ℝ))
(hfast : ∀ (n : ℕ), (g.linear n) (d.fastScale n • d.fast) = (g.length n)⁻¹)
(a source : ℕ → D × ℝ → HarmonicCalculus.ComplexVector)
(j : ℤ)
(k : ℕ → ℝ)
(Ψ : ℕ → D × ℝ → ℝ)
:
noncomputable def
NavierStokes.ErrorHarmonics.pressureAliasBlock
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(r : CorrectionState.ReconstructionData)
(c : CorrectionState.Context (CorrectionState.Lift S))
(u : CorrectionState.State (CorrectionState.Lift S))
(k : ℕ → ℝ)
(Φ : ℕ → CorrectionState.Lift S → ℝ)
(kp : ℕ → ℤ)
:
The pressure alias already used in the correction state, represented in mode zero. Its metadata can be chosen to equal any associated label.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ErrorHarmonics.pressureAliasBlock_represents
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(r : CorrectionState.ReconstructionData)
(c : CorrectionState.Context (CorrectionState.Lift S))
(u : CorrectionState.State (CorrectionState.Lift S))
(k : ℕ → ℝ)
(Φ : ℕ → CorrectionState.Lift S → ℝ)
(kp : ℕ → ℤ)
:
theorem
NavierStokes.ErrorHarmonics.pressureAliasBlock_band
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(r : CorrectionState.ReconstructionData)
(c : CorrectionState.Context (CorrectionState.Lift S))
(u : CorrectionState.State (CorrectionState.Lift S))
(k : ℕ → ℝ)
(Φ : ℕ → CorrectionState.Lift S → ℝ)
(kp : ℕ → ℤ)
:
(pressureAliasBlock r c u k Φ kp).BandLimited 0
theorem
NavierStokes.ErrorHarmonics.pressureAlias_angleIndependent
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(r : CorrectionState.ReconstructionData)
(c : CorrectionState.Context (CorrectionState.Lift S))
(u : CorrectionState.State (CorrectionState.Lift S))
:
noncomputable def
NavierStokes.ErrorHarmonics.temporalAliasBlock
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(r : CorrectionState.ReconstructionData)
(h : ℝ)
(c : CorrectionState.Context (CorrectionState.Lift S))
(u : CorrectionState.State (CorrectionState.Lift S))
(k : ℕ → ℝ)
(Φ : ℕ → CorrectionState.Lift S → ℝ)
(kp : ℕ → ℤ)
:
The temporal alias retains its actual differentiated shifted integral.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ErrorHarmonics.temporalAliasBlock_represents
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(r : CorrectionState.ReconstructionData)
(h : ℝ)
(c : CorrectionState.Context (CorrectionState.Lift S))
(u : CorrectionState.State (CorrectionState.Lift S))
(k : ℕ → ℝ)
(Φ : ℕ → CorrectionState.Lift S → ℝ)
(kp : ℕ → ℤ)
:
theorem
NavierStokes.ErrorHarmonics.temporalAliasBlock_band
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(r : CorrectionState.ReconstructionData)
(h : ℝ)
(c : CorrectionState.Context (CorrectionState.Lift S))
(u : CorrectionState.State (CorrectionState.Lift S))
(k : ℕ → ℝ)
(Φ : ℕ → CorrectionState.Lift S → ℝ)
(kp : ℕ → ℤ)
:
(temporalAliasBlock r h c u k Φ kp).BandLimited 0
theorem
NavierStokes.ErrorHarmonics.temporalAlias_angleIndependent
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(r : CorrectionState.ReconstructionData)
(h : ℝ)
(c : CorrectionState.Context (CorrectionState.Lift S))
(u : CorrectionState.State (CorrectionState.Lift S))
:
noncomputable def
NavierStokes.ErrorHarmonics.pressureAliasRefreshBlock
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(r : CorrectionState.ReconstructionData)
(c : CorrectionState.Context (CorrectionState.Lift S))
(oldState newState : CorrectionState.State (CorrectionState.Lift S))
(k : ℕ → ℝ)
(Φ : ℕ → CorrectionState.Lift S → ℝ)
(kp : ℕ → ℤ)
:
Replacing a pressure reconstruction changes the saved alias by its exact new-minus-old value, which is again mode zero.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ErrorHarmonics.pressureAliasRefreshBlock_represents
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(r : CorrectionState.ReconstructionData)
(c : CorrectionState.Context (CorrectionState.Lift S))
(oldState newState : CorrectionState.State (CorrectionState.Lift S))
(k : ℕ → ℝ)
(Φ : ℕ → CorrectionState.Lift S → ℝ)
(kp : ℕ → ℤ)
:
(pressureAliasRefreshBlock r c oldState newState k Φ kp).oscillation = CorrectionState.pressureAlias r c newState - CorrectionState.pressureAlias r c oldState
theorem
NavierStokes.ErrorHarmonics.pressureAliasRefreshBlock_band
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(r : CorrectionState.ReconstructionData)
(c : CorrectionState.Context (CorrectionState.Lift S))
(oldState newState : CorrectionState.State (CorrectionState.Lift S))
(k : ℕ → ℝ)
(Φ : ℕ → CorrectionState.Lift S → ℝ)
(kp : ℕ → ℤ)
:
(pressureAliasRefreshBlock r c oldState newState k Φ kp).BandLimited 0
Conjugacy is kept for both velocity and pressure coefficients.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ErrorHarmonics.pairedBlock_real
{D : Type}
(j : ℤ)
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
(a : ℕ → D → HarmonicCalculus.ComplexVector)
:
RealBlock (pairedBlock j k Φ kp a)
theorem
NavierStokes.ErrorHarmonics.gaussianBlock_real
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(d : LinearWaveBounds.GraphDirections (D × ℝ))
(ψ : ℕ → D × ℝ → ℝ)
(a source : ℕ → D × ℝ → HarmonicCalculus.ComplexVector)
(j : ℤ)
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
:
RealBlock (gaussianBlock d ψ a source j k Φ kp)
theorem
NavierStokes.ErrorHarmonics.pressureAliasBlock_real
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(r : CorrectionState.ReconstructionData)
(c : CorrectionState.Context (CorrectionState.Lift S))
(u : CorrectionState.State (CorrectionState.Lift S))
(k : ℕ → ℝ)
(Φ : ℕ → CorrectionState.Lift S → ℝ)
(kp : ℕ → ℤ)
:
RealBlock (pressureAliasBlock r c u k Φ kp)
theorem
NavierStokes.ErrorHarmonics.temporalAliasBlock_real
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(r : CorrectionState.ReconstructionData)
(h : ℝ)
(c : CorrectionState.Context (CorrectionState.Lift S))
(u : CorrectionState.State (CorrectionState.Lift S))
(k : ℕ → ℝ)
(Φ : ℕ → CorrectionState.Lift S → ℝ)
(kp : ℕ → ℤ)
:
RealBlock (temporalAliasBlock r h c u k Φ kp)
theorem
NavierStokes.ErrorHarmonics.pressureAliasRefreshBlock_real
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(r : CorrectionState.ReconstructionData)
(c : CorrectionState.Context (CorrectionState.Lift S))
(oldState newState : CorrectionState.State (CorrectionState.Lift S))
(k : ℕ → ℝ)
(Φ : ℕ → CorrectionState.Lift S → ℝ)
(kp : ℕ → ℤ)
:
RealBlock (pressureAliasRefreshBlock r c oldState newState k Φ kp)
theorem
NavierStokes.ErrorHarmonics.symmetric_add
{D : Type}
{a b : HarmonicFields.Coefficients D}
(ha : HarmonicFields.ConjugateSymmetric a)
(hb : HarmonicFields.ConjugateSymmetric b)
:
theorem
NavierStokes.ErrorHarmonics.band_sum
{D ι : Type}
(s : Finset ι)
(a : ι → HarmonicFields.Coefficients D)
(N : ℕ)
(ha : ∀ l ∈ s, HarmonicFields.BandLimited (a l) N)
:
HarmonicFields.BandLimited (∑ l ∈ s, a l) N
theorem
NavierStokes.ErrorHarmonics.symmetric_sum
{D ι : Type}
(s : Finset ι)
(a : ι → HarmonicFields.Coefficients D)
(ha : ∀ l ∈ s, HarmonicFields.ConjugateSymmetric (a l))
:
HarmonicFields.ConjugateSymmetric (∑ l ∈ s, a l)
noncomputable def
NavierStokes.ErrorHarmonics.sumBlock
{D ι : Type}
(s : Finset ι)
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
(b : ι → CorrectionState.HarmonicBlock D)
:
Accumulation is coefficient addition within one fixed label. Distinct labels are left distinct even if their numerical carriers coincide.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ErrorHarmonics.sumBlock_band
{D ι : Type}
(s : Finset ι)
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
(b : ι → CorrectionState.HarmonicBlock D)
(N : ℕ)
(hb : ∀ l ∈ s, (b l).BandLimited N)
:
(sumBlock s k Φ kp b).BandLimited N
theorem
NavierStokes.ErrorHarmonics.realBlock_field
{D : Type}
{b : CorrectionState.HarmonicBlock D}
(hb : RealBlock b)
(n : ℕ)
(p : D × ℝ)
(i : Fin 3)
:
↑(b.oscillation n p i) = HarmonicFields.field (b.velocity n i) (b.frequency n) (b.phase n) (b.angularFrequency n) p
structure
NavierStokes.ErrorHarmonics.GaussianData
(D : Type)
[NormedAddCommGroup D]
[NormedSpace ℝ D]
:
Only primitive data are stored. The error field and its coefficients are computed from the cutoff derivative, amplitudes, and carrier.
- directions : LinearWaveBounds.GraphDirections (D × ℝ)
Directions of
GaussianData, of typeLinearWaveBounds.GraphDirections (D × ℝ). Cutoff of
GaussianData, of typeℕ → D × ℝ → ℝ.- amplitude : ℕ → D × ℝ → HarmonicCalculus.ComplexVector
Amplitude of
GaussianData, of typeℕ → D × ℝ → HarmonicCalculus.ComplexVector. - source : ℕ → D × ℝ → HarmonicCalculus.ComplexVector
Source of
GaussianData, of typeℕ → D × ℝ → HarmonicCalculus.ComplexVector. - harmonic : ℤ
Harmonic of
GaussianData, of typeℤ. Phase of
GaussianData, of typeℕ → D × ℝ → ℝ.
Instances For
noncomputable def
NavierStokes.ErrorHarmonics.GaussianData.error
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(g : GaussianData D)
(k : ℕ → ℝ)
:
Error, given by gaussianField g.directions g.cutoff g.amplitude g.source g.harmonic k g.phase.
Equations
- g.error k = NavierStokes.ErrorHarmonics.gaussianField g.directions g.cutoff g.amplitude g.source g.harmonic k g.phase
Instances For
noncomputable def
NavierStokes.ErrorHarmonics.GaussianData.block
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(g : GaussianData D)
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
:
Block, given by gaussianBlock g.directions g.cutoff g.amplitude g.source g.harmonic k Φ kp.
Equations
- g.block k Φ kp = NavierStokes.ErrorHarmonics.gaussianBlock g.directions g.cutoff g.amplitude g.source g.harmonic k Φ kp
Instances For
def
NavierStokes.ErrorHarmonics.GaussianData.Compatible
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(g : GaussianData D)
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
:
Compatible as an element of Prop.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ErrorHarmonics.GaussianData.block_represents
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(g : GaussianData D)
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
(hg : g.Compatible k Φ kp)
:
noncomputable def
NavierStokes.ErrorHarmonics.accumulatedGaussianBlock
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(steps : ℕ)
(g : ℕ → GaussianData D)
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
:
Accumulated gaussian block, given by sumBlock (Finset.range steps) k Φ kp (fun s => (g s).block k Φ kp).
Equations
- NavierStokes.ErrorHarmonics.accumulatedGaussianBlock steps g k Φ kp = NavierStokes.ErrorHarmonics.sumBlock (Finset.range steps) k Φ kp fun (s : ℕ) => (g s).block k Φ kp
Instances For
theorem
NavierStokes.ErrorHarmonics.accumulatedGaussianBlock_represents
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(steps : ℕ)
(g : ℕ → GaussianData D)
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
(hg : ∀ s < steps, (g s).Compatible k Φ kp)
:
theorem
NavierStokes.ErrorHarmonics.accumulatedGaussianBlock_band
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(steps : ℕ)
(g : ℕ → GaussianData D)
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
(N : ℕ)
(hj : ∀ s < steps, (g s).harmonic.natAbs ≤ N)
:
(accumulatedGaussianBlock steps g k Φ kp).BandLimited N
theorem
NavierStokes.ErrorHarmonics.accumulatedGaussianBlock_band_pow
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(steps : ℕ)
(g : ℕ → GaussianData D)
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
(hj : ∀ s < steps, (g s).harmonic.natAbs ≤ 2 ^ s)
:
(accumulatedGaussianBlock steps g k Φ kp).BandLimited (2 ^ steps)
This bounds the values of the occupied harmonics, not merely their count.
theorem
NavierStokes.ErrorHarmonics.accumulatedGaussianBlock_real
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(steps : ℕ)
(g : ℕ → GaussianData D)
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
:
RealBlock (accumulatedGaussianBlock steps g k Φ kp)
noncomputable def
NavierStokes.ErrorHarmonics.accumulatedAlias
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(steps : ℕ)
(r : CorrectionState.ReconstructionData)
(h : ℝ)
(c : CorrectionState.Context (CorrectionState.Lift S))
(u : ℕ → CorrectionState.State (CorrectionState.Lift S))
:
Actual saved aliases after finitely many temporal stages and the current pressure reconstruction. The state path may be produced by any correction rule.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.ErrorHarmonics.accumulatedAliasBlock
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(steps : ℕ)
(r : CorrectionState.ReconstructionData)
(h : ℝ)
(c : CorrectionState.Context (CorrectionState.Lift S))
(u : ℕ → CorrectionState.State (CorrectionState.Lift S))
(k : ℕ → ℝ)
(Φ : ℕ → CorrectionState.Lift S → ℝ)
(kp : ℕ → ℤ)
:
Accumulated alias block, given by zeroBlock k Φ kp (fun n x => accumulatedAlias steps r h c u n (x, 0)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ErrorHarmonics.accumulatedAlias_angleIndependent
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(steps : ℕ)
(r : CorrectionState.ReconstructionData)
(h : ℝ)
(c : CorrectionState.Context (CorrectionState.Lift S))
(u : ℕ → CorrectionState.State (CorrectionState.Lift S))
:
AngleIndependent (accumulatedAlias steps r h c u)
theorem
NavierStokes.ErrorHarmonics.accumulatedAliasBlock_represents
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(steps : ℕ)
(r : CorrectionState.ReconstructionData)
(h : ℝ)
(c : CorrectionState.Context (CorrectionState.Lift S))
(u : ℕ → CorrectionState.State (CorrectionState.Lift S))
(k : ℕ → ℝ)
(Φ : ℕ → CorrectionState.Lift S → ℝ)
(kp : ℕ → ℤ)
:
theorem
NavierStokes.ErrorHarmonics.accumulatedAliasBlock_band
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(steps : ℕ)
(r : CorrectionState.ReconstructionData)
(h : ℝ)
(c : CorrectionState.Context (CorrectionState.Lift S))
(u : ℕ → CorrectionState.State (CorrectionState.Lift S))
(k : ℕ → ℝ)
(Φ : ℕ → CorrectionState.Lift S → ℝ)
(kp : ℕ → ℤ)
:
(accumulatedAliasBlock steps r h c u k Φ kp).BandLimited 0
theorem
NavierStokes.ErrorHarmonics.accumulatedAliasBlock_real
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(steps : ℕ)
(r : CorrectionState.ReconstructionData)
(h : ℝ)
(c : CorrectionState.Context (CorrectionState.Lift S))
(u : ℕ → CorrectionState.State (CorrectionState.Lift S))
(k : ℕ → ℝ)
(Φ : ℕ → CorrectionState.Lift S → ℝ)
(kp : ℕ → ℤ)
:
RealBlock (accumulatedAliasBlock steps r h c u k Φ kp)
theorem
NavierStokes.ErrorHarmonics.accumulatedAlias_succ
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(steps : ℕ)
(r : CorrectionState.ReconstructionData)
(h : ℝ)
(c : CorrectionState.Context (CorrectionState.Lift S))
(u : ℕ → CorrectionState.State (CorrectionState.Lift S))
:
accumulatedAlias (steps + 1) r h c u = accumulatedAlias steps r h c u + CorrectionState.temporalAlias r h c (u steps) + (CorrectionState.pressureAlias r c (u (steps + 1)) - CorrectionState.pressureAlias r c (u steps))
theorem
NavierStokes.ErrorHarmonics.pressure_refreshes_telescope
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(steps : ℕ)
(r : CorrectionState.ReconstructionData)
(c : CorrectionState.Context (CorrectionState.Lift S))
(u : ℕ → CorrectionState.State (CorrectionState.Lift S))
:
∑ s ∈ Finset.range steps, (CorrectionState.pressureAlias r c (u (s + 1)) - CorrectionState.pressureAlias r c (u s)) = CorrectionState.pressureAlias r c (u steps) - CorrectionState.pressureAlias r c (u 0)
noncomputable def
NavierStokes.ErrorHarmonics.accumulatedErrorBlock
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(steps : ℕ)
(g : ℕ → GaussianData (CorrectionState.Lift S))
(r : CorrectionState.ReconstructionData)
(h : ℝ)
(c : CorrectionState.Context (CorrectionState.Lift S))
(u : ℕ → CorrectionState.State (CorrectionState.Lift S))
(k : ℕ → ℝ)
(Φ : ℕ → CorrectionState.Lift S → ℝ)
(kp : ℕ → ℤ)
:
The two retained error types for one label are added as actual finite coefficient families. The base error is handled separately in the physical decomposition and cancels from the good residual.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ErrorHarmonics.accumulatedErrorBlock_represents
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(steps : ℕ)
(g : ℕ → GaussianData (CorrectionState.Lift S))
(r : CorrectionState.ReconstructionData)
(h : ℝ)
(c : CorrectionState.Context (CorrectionState.Lift S))
(u : ℕ → CorrectionState.State (CorrectionState.Lift S))
(k : ℕ → ℝ)
(Φ : ℕ → CorrectionState.Lift S → ℝ)
(kp : ℕ → ℤ)
(hg : ∀ s < steps, (g s).Compatible k Φ kp)
:
(accumulatedErrorBlock steps g r h c u k Φ kp).oscillation = ∑ s ∈ Finset.range steps, (g s).error k + accumulatedAlias steps r h c u
theorem
NavierStokes.ErrorHarmonics.accumulatedErrorBlock_band
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(steps : ℕ)
(g : ℕ → GaussianData (CorrectionState.Lift S))
(r : CorrectionState.ReconstructionData)
(h : ℝ)
(c : CorrectionState.Context (CorrectionState.Lift S))
(u : ℕ → CorrectionState.State (CorrectionState.Lift S))
(k : ℕ → ℝ)
(Φ : ℕ → CorrectionState.Lift S → ℝ)
(kp : ℕ → ℤ)
(hj : ∀ s < steps, (g s).harmonic.natAbs ≤ 2 ^ s)
:
(accumulatedErrorBlock steps g r h c u k Φ kp).BandLimited (2 ^ steps)
theorem
NavierStokes.ErrorHarmonics.accumulatedErrorBlock_real
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
(steps : ℕ)
(g : ℕ → GaussianData (CorrectionState.Lift S))
(r : CorrectionState.ReconstructionData)
(h : ℝ)
(c : CorrectionState.Context (CorrectionState.Lift S))
(u : ℕ → CorrectionState.State (CorrectionState.Lift S))
(k : ℕ → ℝ)
(Φ : ℕ → CorrectionState.Lift S → ℝ)
(kp : ℕ → ℤ)
:
RealBlock (accumulatedErrorBlock steps g r h c u k Φ kp)
Cartesian location of the cylindrical point (r,z,θ).
Equations
- NavierStokes.ErrorHarmonics.polarSpace r z θ = NavierStokes.AxisymmetricResidual.pack (r * Real.cos θ) (r * Real.sin θ) z
Instances For
Polar profile, given by (q.1, (q.2.1 ^ 2 / 2, q.2.2)).
Instances For
theorem
NavierStokes.ErrorHarmonics.profilePoint_polarSpace
(q : AxisymmetricFields.ProfilePoint)
(θ : ℝ)
:
noncomputable def
NavierStokes.ErrorHarmonics.cylindricalComponents
(θ : ℝ)
(v : ProblemStatement.Space)
:
Components in the actual orthonormal radial/angular/axial frame.
Equations
Instances For
theorem
NavierStokes.ErrorHarmonics.axisymmetricVelocity_components
(B F U : AxisymmetricFields.Profile)
(q : AxisymmetricFields.ProfilePoint)
(θ : ℝ)
:
cylindricalComponents θ (AxisymmetricResidual.velocity B F U (q.1, polarSpace q.2.1 q.2.2 θ)) = ![-q.2.1 * B (polarProfile q), q.2.1 * F (polarProfile q), U (polarProfile q)]
noncomputable def
NavierStokes.ErrorHarmonics.axisymmetricBaseError
(B F U P : ℕ → AxisymmetricFields.Profile)
:
The literal Cartesian Navier--Stokes residual, expressed in its cylindrical frame. This is not an independently specified error oracle.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.ErrorHarmonics.axisymmetricBaseValue
(B F U P : ℕ → AxisymmetricFields.Profile)
:
Axisymmetric base value as an element of MeanVector ProfilePoint.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ErrorHarmonics.axisymmetricBaseError_eq_value
(B F U P : ℕ → AxisymmetricFields.Profile)
(n : ℕ)
(q : AxisymmetricFields.ProfilePoint)
(θ : ℝ)
(hB : AxisymmetricResidual.SliceC2 (B n) q.1)
(hF : AxisymmetricResidual.SliceC2 (F n) q.1)
(hU : AxisymmetricResidual.SliceC2 (U n) q.1)
(hP : AxisymmetricResidual.SliceDifferentiable (P n) q.1)
:
theorem
NavierStokes.ErrorHarmonics.axisymmetricBaseError_angleIndependent_at
(B F U P : ℕ → AxisymmetricFields.Profile)
(n : ℕ)
(q : AxisymmetricFields.ProfilePoint)
(θ : ℝ)
(hB : AxisymmetricResidual.SliceC2 (B n) q.1)
(hF : AxisymmetricResidual.SliceC2 (F n) q.1)
(hU : AxisymmetricResidual.SliceC2 (U n) q.1)
(hP : AxisymmetricResidual.SliceDifferentiable (P n) q.1)
:
A local-in-time identity; no smooth continuation through singular time is required to place the actual base residual in the zero harmonic.
noncomputable def
NavierStokes.ErrorHarmonics.axisymmetricBaseBlock
(B F U P : ℕ → AxisymmetricFields.Profile)
(k : ℕ → ℝ)
(Φ : ℕ → AxisymmetricFields.ProfilePoint → ℝ)
(kp : ℕ → ℤ)
:
Axisymmetric base block, given by zeroBlock k Φ kp (axisymmetricBaseValue B F U P).
Equations
- NavierStokes.ErrorHarmonics.axisymmetricBaseBlock B F U P k Φ kp = NavierStokes.ErrorHarmonics.zeroBlock k Φ kp (NavierStokes.ErrorHarmonics.axisymmetricBaseValue B F U P)
Instances For
theorem
NavierStokes.ErrorHarmonics.axisymmetricBaseBlock_represents_at
(B F U P : ℕ → AxisymmetricFields.Profile)
(k : ℕ → ℝ)
(Φ : ℕ → AxisymmetricFields.ProfilePoint → ℝ)
(kp : ℕ → ℤ)
(n : ℕ)
(q : AxisymmetricFields.ProfilePoint)
(θ : ℝ)
(i : Fin 3)
(hB : AxisymmetricResidual.SliceC2 (B n) q.1)
(hF : AxisymmetricResidual.SliceC2 (F n) q.1)
(hU : AxisymmetricResidual.SliceC2 (U n) q.1)
(hP : AxisymmetricResidual.SliceDifferentiable (P n) q.1)
:
(axisymmetricBaseBlock B F U P k Φ kp).oscillation n (q, θ) i = axisymmetricBaseError B F U P n (q, θ) i
theorem
NavierStokes.ErrorHarmonics.axisymmetricBaseBlock_band
(B F U P : ℕ → AxisymmetricFields.Profile)
(k : ℕ → ℝ)
(Φ : ℕ → AxisymmetricFields.ProfilePoint → ℝ)
(kp : ℕ → ℤ)
:
(axisymmetricBaseBlock B F U P k Φ kp).BandLimited 0
theorem
NavierStokes.ErrorHarmonics.axisymmetricBaseBlock_real
(B F U P : ℕ → AxisymmetricFields.Profile)
(k : ℕ → ℝ)
(Φ : ℕ → AxisymmetricFields.ProfilePoint → ℝ)
(kp : ℕ → ℤ)
:
RealBlock (axisymmetricBaseBlock B F U P k Φ kp)
The requested stress is the negative primitive of the actual state #
noncomputable def
NavierStokes.SignedWaveUpdate.requestedStress
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(p : SignedStressPrimitive.Patch)
(c : CorrectionState.Context (PressureStream.Lift E))
(u : CorrectionState.State (PressureStream.Lift E))
:
Requested stress, defined pointwise by ![SignedStressPrimitive.barSigma p 2 (u.thetaResidual c n) z, SignedStressPrimitive.barSigma p 1 (u.axialResidual c n) z].
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.SignedWaveUpdate.requestedStress_contDiff
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(p : SignedStressPrimitive.Patch)
(c : CorrectionState.Context (PressureStream.Lift E))
(u : CorrectionState.State (PressureStream.Lift E))
(n : ℕ)
(ht : ContDiff ℝ (↑⊤) (u.thetaResidual c n))
(hz : ContDiff ℝ (↑⊤) (u.axialResidual c n))
(hst : RadialAlias.RadiallySupported p.a p.b (u.thetaResidual c n))
(hsz : RadialAlias.RadiallySupported p.a p.b (u.axialResidual c n))
:
ContDiff ℝ (↑⊤) (requestedStress p c u n)
theorem
NavierStokes.SignedWaveUpdate.requestedStress_negative_primitive
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(p : SignedStressPrimitive.Patch)
(c : CorrectionState.Context (PressureStream.Lift E))
(u : CorrectionState.State (PressureStream.Lift E))
(n : ℕ)
(ht : ContDiff ℝ (↑⊤) (u.thetaResidual c n))
(hz : ContDiff ℝ (↑⊤) (u.axialResidual c n))
(hst : RadialAlias.RadiallySupported p.a p.b (u.thetaResidual c n))
(hsz : RadialAlias.RadiallySupported p.a p.b (u.axialResidual c n))
(z : ℝ × E)
:
requestedStress p c u n z = ![(-∫ (r : ℝ) in 0..z.1, r ^ 2 * SignedStressPrimitive.adjusted p 2 (PressureStream.torusAverage (u.thetaResidual c n)) (r, z.2)) / z.1 ^ 2, (-∫ (r : ℝ) in 0..z.1, r ^ 1 * SignedStressPrimitive.adjusted p 1 (PressureStream.torusAverage (u.axialResidual c n)) (r, z.2)) / z.1 ^ 1]
theorem
NavierStokes.SignedWaveUpdate.requestedStress_divergence
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(p : SignedStressPrimitive.Patch)
(c : CorrectionState.Context (PressureStream.Lift E))
(u : CorrectionState.State (PressureStream.Lift E))
(n : ℕ)
(ht : ContDiff ℝ (↑⊤) (u.thetaResidual c n))
(hz : ContDiff ℝ (↑⊤) (u.axialResidual c n))
(hst : RadialAlias.RadiallySupported p.a p.b (u.thetaResidual c n))
(hsz : RadialAlias.RadiallySupported p.a p.b (u.axialResidual c n))
(z : E)
{r : ℝ}
(hr : 0 < r)
:
IntegratedMeanBalances.radialDivergence 2 (fun (t : ℝ) => requestedStress p c u n (t, z) 0) r = -SignedStressPrimitive.adjusted p 2 (PressureStream.torusAverage (u.thetaResidual c n)) (r, z) ∧ IntegratedMeanBalances.radialDivergence 1 (fun (t : ℝ) => requestedStress p c u n (t, z) 1) r = -SignedStressPrimitive.adjusted p 1 (PressureStream.torusAverage (u.axialResidual c n)) (r, z)
Inverse jets and the signed quotient #
structure
NavierStokes.SignedWaveUpdate.CovarianceControl
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(s : WeightedClasses.StripData D)
(H : ℕ → D → Mat2)
(T : ℕ → D → Vec2)
:
Only primitive matrix/target jets and zeroth-order primary margins occur in this record. There is no assumption on an inverse or a signed output.
- matrix_jets (i j : Fin 2) : PhaseJetBounds.PolynomialJets (PrimaryPulseBounds.phaseDomain s) fun (n : ℕ) (x : D) => H n x i j
- target_jets (i : Fin 2) : WeightedClasses.MeanClass s 0 fun (n : ℕ) (x : D) => T n x i
- b : ℝ
B of
CovarianceControl, of typeℝ. - M : ℝ
M of
CovarianceControl, of typeℝ. - c : ℝ
C of
CovarianceControl, of typeℝ.
Instances For
theorem
NavierStokes.SignedWaveUpdate.CovarianceControl.cone
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{H : ℕ → D → Mat2}
{T : ℕ → D → Vec2}
(h : CovarianceControl s H T)
(n : ℕ)
{x : D}
(hx : x ∈ s.domain)
:
SmoothCovariance.StrictCone (H n x) (T n x)
theorem
NavierStokes.SignedWaveUpdate.CovarianceControl.inverse_class
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{H : ℕ → D → Mat2}
{T : ℕ → D → Vec2}
(h : CovarianceControl s H T)
{R : ℕ → D → Vec2}
{β : ℝ}
(hR : ∀ (i : Fin 2), WeightedClasses.MeanClass s β fun (n : ℕ) (x : D) => R n x i)
(j : Fin 2)
:
WeightedClasses.MeanClass s β fun (n : ℕ) (x : D) => Matrix.mulVec (H n x)⁻¹ (R n x) j
Cramer's actual formula preserves every band exponent, including signed targets. Its denominator estimates are taken from the same primary matrix.
theorem
NavierStokes.SignedWaveUpdate.CovarianceControl.inverse_control
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{H : ℕ → D → Mat2}
{T : ℕ → D → Vec2}
(h : CovarianceControl s H T)
(j : Fin 2)
:
SignedCovariance.InverseControl s (fun (x : ℕ) (x_1 : D) => s.zeta x_1) fun (n : ℕ) (x : D) =>
Matrix.mulVec (H n x)⁻¹ (T n x) j
theorem
NavierStokes.SignedWaveUpdate.CovarianceControl.increment_class
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{H : ℕ → D → Mat2}
{T : ℕ → D → Vec2}
(h : CovarianceControl s H T)
{R : ℕ → D → Vec2}
{β : ℝ}
(hR : ∀ (i : Fin 2), WeightedClasses.MeanClass s β fun (n : ℕ) (x : D) => R n x i)
(j : Fin 2)
:
WeightedClasses.WaveClass s (fun (x : ℕ) (x_1 : D) => 1) β fun (n : ℕ) (x : D) =>
SignedCovariance.increment (H n x) (T n x) (R n x) j
noncomputable def
NavierStokes.SignedWaveUpdate.signedScalar
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(s : WeightedClasses.StripData D)
(H : ℕ → D → Mat2)
(T R : ℕ → D → Vec2)
(mask : ℕ → D → ℝ)
(j : Fin 2)
:
Signed scalar, defined pointwise by Real.sqrt (s.epsilon n) * SignedCovariance.increment (H n x) (T n x) (R n x) j * mask n x.
Equations
- NavierStokes.SignedWaveUpdate.signedScalar s H T R mask j n x = √(s.epsilon n) * NavierStokes.SignedCovariance.increment (H n x) (T n x) (R n x) j * mask n x
Instances For
noncomputable def
NavierStokes.SignedWaveUpdate.signedVector
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(s : WeightedClasses.StripData D)
(H : ℕ → D → Mat2)
(T R : ℕ → D → Vec2)
(mask : ℕ → D → ℝ)
(v : ℕ → D → Space)
(j : Fin 2)
:
Signed vector, defined pointwise by signedScalar s H T R mask j n x • v n x.
Equations
- NavierStokes.SignedWaveUpdate.signedVector s H T R mask v j n x = NavierStokes.SignedWaveUpdate.signedScalar s H T R mask j n x • v n x
Instances For
theorem
NavierStokes.SignedWaveUpdate.signedScalar_class
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{H : ℕ → D → Mat2}
{T R : ℕ → D → Vec2}
{mask : ℕ → D → ℝ}
{β : ℝ}
(h : CovarianceControl s H T)
(hR : ∀ (i : Fin 2), WeightedClasses.MeanClass s β fun (n : ℕ) (x : D) => R n x i)
(hm : WeightedClasses.UnweightedClass s 0 mask)
(j : Fin 2)
:
WeightedClasses.WaveClass s (fun (x : ℕ) (x_1 : D) => 1) (β + 1 / 2) (signedScalar s H T R mask j)
theorem
NavierStokes.SignedWaveUpdate.signedVector_class
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{H : ℕ → D → Mat2}
{T R : ℕ → D → Vec2}
{mask : ℕ → D → ℝ}
{v : ℕ → D → Space}
{P : ℕ → D → ℝ}
{β : ℝ}
(h : CovarianceControl s H T)
(hR : ∀ (i : Fin 2), WeightedClasses.MeanClass s β fun (n : ℕ) (x : D) => R n x i)
(hm : WeightedClasses.UnweightedClass s 0 mask)
(hv : WeightedClasses.MemClass s P 0 v)
(j : Fin 2)
:
WeightedClasses.WaveClass s P (β + 1 / 2) (signedVector s H T R mask v j)
The same homogeneous fundamental and its constructed pressure #
noncomputable def
NavierStokes.SignedWaveUpdate.homogeneousCoefficients
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(a : LinearWaveBounds.WaveCoefficients D)
(s : WeightedClasses.StripData D)
(d : LinearWaveBounds.GraphDirections D)
(v Ndot : ℕ → D → Space)
(A : ℕ → D → Space →L[ℝ] Space)
:
Homogeneous coefficients as an element of LinearWaveBounds.WaveCoefficients D.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.SignedWaveUpdate.coefficients
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(a : LinearWaveBounds.WaveCoefficients D)
(s : WeightedClasses.StripData D)
(d : LinearWaveBounds.GraphDirections D)
(H : ℕ → D → Mat2)
(T R : ℕ → D → Vec2)
(mask : ℕ → D → ℝ)
(v Ndot : ℕ → D → Space)
(A : ℕ → D → Space →L[ℝ] Space)
(j : Fin 2)
:
Coefficients, given by homogeneousCoefficients a s d (signedVector s H T R mask v j) Ndot A.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.SignedWaveUpdate.coefficients_inputBounds
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{a : LinearWaveBounds.WaveCoefficients D}
{P₀ P : ℕ → D → ℝ}
{α₀ β κ : ℝ}
(hbase : LinearWaveBounds.InputBounds s P₀ α₀ κ d a)
{H : ℕ → D → Mat2}
{T R : ℕ → D → Vec2}
{mask : ℕ → D → ℝ}
{v Ndot : ℕ → D → Space}
{A : ℕ → D → Space →L[ℝ] Space}
(hcov : CovarianceControl s H T)
(hR : ∀ (i : Fin 2), WeightedClasses.MeanClass s β fun (n : ℕ) (x : D) => R n x i)
(hm : WeightedClasses.UnweightedClass s 0 mask)
(hv : WeightedClasses.MemClass s P 0 v)
(hN : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain s) (a.normal s d))
(hNdot : WeightedClasses.UnweightedClass s 0 Ndot)
(hA : WeightedClasses.UnweightedClass s 0 A)
{b M : ℝ}
(hb : 0 < b)
(hlo : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ ‖a.normal s d n x‖)
(hhi : ∀ (n : ℕ), ∀ x ∈ s.domain, ‖a.normal s d n x‖ ≤ M)
(hK : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / a.frequency n)
(j : Fin 2)
:
LinearWaveBounds.InputBounds s P (β + 1 / 2) κ d (coefficients a s d H T R mask v Ndot A j)
Every signed amplitude and pressure bound is obtained from the actual inverse quotient and the primitive homogeneous fundamental. The input wave bound supplies only the already fixed background geometry.
def
NavierStokes.SignedWaveUpdate.FrozenAlong
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(v : D)
(f : ℕ → D → E)
:
Equality along an actual straight fast orbit, imposed on the primitive slow data, not on the signed solve or its derivatives.
Equations
Instances For
theorem
NavierStokes.SignedWaveUpdate.FrozenAlong.derivative
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{v : D}
{f : ℕ → D → E}
(hf : FrozenAlong v f)
(n : ℕ)
{x : D}
(hd : DifferentiableAt ℝ (f n) x)
:
theorem
NavierStokes.SignedWaveUpdate.signedScalar_frozen
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{H : ℕ → D → Mat2}
{T R : ℕ → D → Vec2}
{mask : ℕ → D → ℝ}
{v : D}
(hH : FrozenAlong v H)
(hT : FrozenAlong v T)
(hR : FrozenAlong v R)
(hm : FrozenAlong v mask)
(j : Fin 2)
:
FrozenAlong v (signedScalar s H T R mask j)
theorem
NavierStokes.SignedWaveUpdate.along_smul
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(V : D → D)
{f : D → ℝ}
{g : D → E}
{x : D}
(hf : DifferentiableAt ℝ f x)
(hg : DifferentiableAt ℝ g x)
:
HarmonicCalculus.along V (fun (y : D) => f y • g y) x = HarmonicCalculus.along V f x • g x + f x • HarmonicCalculus.along V g x
theorem
NavierStokes.SignedWaveUpdate.projectedRhs_smul
(N Ndot v Av : Space)
(δ c : ℝ)
:
TangentProjection.projectedRhs N Ndot (c • v) (c • Av) 0 δ = c • TangentProjection.projectedRhs N Ndot v Av 0 δ
theorem
NavierStokes.SignedWaveUpdate.shear_smul
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(R F G : D → ℝ)
(Vr : D → D)
(v : D → HarmonicCalculus.ComplexVector)
(c : D → ℝ)
(x : D)
:
LinearWaveResidual.shear R F G Vr (fun (y : D) => c y • v y) x = c x • LinearWaveResidual.shear R F G Vr v x
theorem
NavierStokes.SignedWaveUpdate.coefficients_principal_zero
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
(a : LinearWaveBounds.WaveCoefficients D)
{H : ℕ → D → Mat2}
{T R : ℕ → D → Vec2}
{mask : ℕ → D → ℝ}
{v Ndot : ℕ → D → Space}
{A : ℕ → D → Space →L[ℝ] Space}
(hcov : CovarianceControl s H T)
{β : ℝ}
(hR : ∀ (i : Fin 2), WeightedClasses.MeanClass s β fun (n : ℕ) (x : D) => R n x i)
(hm : WeightedClasses.UnweightedClass s 0 mask)
{P : ℕ → D → ℝ}
(hv : WeightedClasses.MemClass s P 0 v)
(hHf : FrozenAlong d.fast H)
(hTf : FrozenAlong d.fast T)
(hRf : FrozenAlong d.fast R)
(hmf : FrozenAlong d.fast mask)
(hK : ∀ (n : ℕ), a.frequency n ≠ 0)
(hode :
∀ (n : ℕ),
∀ x ∈ s.domain,
HarmonicCalculus.along (d.fastField n) (v n) x = TangentProjection.projectedRhs (a.normal s d n x) (Ndot n x) (v n x) ((A n x) (v n x)) 0
(s.epsilon n * a.frequency n ^ 2 * ‖a.normal s d n x‖ ^ 2))
(haction :
∀ (n : ℕ),
∀ x ∈ s.domain,
CurlClassBounds.complexify ((A n x) (v n x)) = LinearWaveResidual.shear (a.radius n) (a.frequencyBase n) (a.axialBase n) (d.radialField n)
(fun (y : D) => CurlClassBounds.complexify (v n y)) x)
(j : Fin 2)
(n : ℕ)
{x : D}
(hx : x ∈ s.domain)
:
Scaling the actual homogeneous projected ODE by the frozen inverse coefficient gives the signed principal equation, with its pressure constructed from the same normal and action. No signed equation is an input.
Instantiation with the constructed primary phase and pulse #
noncomputable def
NavierStokes.SignedWaveUpdate.phaseMatrix
{D : Type}
{U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow}
(F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U)
(pref : Fin 2 → ℕ → ℝ)
(χ : ℕ → D → PhaseCalculus.Slow × ℝ)
:
Phase matrix, given by PrimaryPulseBounds.chartCovariance pref (fun j => (F j).frame) (fun j => (F j).lam) (fun j => (F j).u) (fun j => (F j).L) χ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.SignedWaveUpdate.phaseFundamental
{D : Type}
{U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow}
(F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U)
(χ : ℕ → D → PhaseCalculus.Slow × ℝ)
(j : Fin 2)
:
Phase fundamental, defined pointwise by PrimaryPulseBounds.normalizedPulse ((F j).frame n) ((F j).lam n) ((F j).u n) ((F j).L n) (χ n x).
Equations
- NavierStokes.SignedWaveUpdate.phaseFundamental F χ j n x = NavierStokes.PrimaryPulseBounds.normalizedPulse ((F j).frame n) ((F j).lam n) ((F j).u n) ((F j).L n) (χ n x)
Instances For
noncomputable def
NavierStokes.SignedWaveUpdate.phaseEnvelope
{D : Type}
{U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow}
(F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U)
(χ : ℕ → D → PhaseCalculus.Slow × ℝ)
(j : Fin 2)
:
Phase envelope, defined pointwise by PrimaryPulseBounds.referenceP ((F j).lam n) ((F j).u n) ((F j).L n) ((F j).L n * (χ n x).2).
Equations
- NavierStokes.SignedWaveUpdate.phaseEnvelope F χ j n x = NavierStokes.PrimaryPulseBounds.referenceP ((F j).lam n) ((F j).u n) ((F j).L n) ((F j).L n * (χ n x).2)
Instances For
theorem
NavierStokes.SignedWaveUpdate.phaseFundamental_class
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow}
(F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U)
(χ : ℕ → D → PhaseCalculus.Slow × ℝ)
(hscale : ∀ (n : ℕ), U.scale n = s.slow n)
(hχ : PhaseJetBounds.PolynomialJets (PrimaryPulseBounds.phaseDomain s) χ)
(hmap : ∀ (n : ℕ), ∀ x ∈ s.domain, χ n x ∈ U.carrier n ×ˢ Set.Ioo 0 1)
(j : Fin 2)
:
WeightedClasses.MemClass s (phaseEnvelope F χ j) 0 (phaseFundamental F χ j)
theorem
NavierStokes.SignedWaveUpdate.phaseMatrix_jets
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow}
(F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U)
(pref : Fin 2 → ℕ → ℝ)
(χ : ℕ → D → PhaseCalculus.Slow × ℝ)
(hscale : ∀ (n : ℕ), U.scale n = s.slow n)
(hχ : PhaseJetBounds.PolynomialJets (PrimaryPulseBounds.phaseDomain s) χ)
(hmap : ∀ (n : ℕ), ∀ x ∈ s.domain, (χ n x).1 ∈ U.carrier n)
(hpref : ∀ (j : Fin 2), PhaseJetBounds.PolynomialJets U fun (n : ℕ) (x : PhaseCalculus.Slow) => pref j n)
(i j : Fin 2)
:
PhaseJetBounds.PolynomialJets (PrimaryPulseBounds.phaseDomain s) fun (n : ℕ) (x : D) => phaseMatrix F pref χ n x i j
noncomputable def
NavierStokes.SignedWaveUpdate.phaseControl
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow}
(F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U)
(pref : Fin 2 → ℕ → ℝ)
(χ : ℕ → D → PhaseCalculus.Slow × ℝ)
(T : ℕ → D → Vec2)
(hscale : ∀ (n : ℕ), U.scale n = s.slow n)
(hχ : PhaseJetBounds.PolynomialJets (PrimaryPulseBounds.phaseDomain s) χ)
(hmap : ∀ (n : ℕ), ∀ x ∈ s.domain, (χ n x).1 ∈ U.carrier n)
(hpref : ∀ (j : Fin 2), PhaseJetBounds.PolynomialJets U fun (n : ℕ) (x : PhaseCalculus.Slow) => pref j n)
(hT : ∀ (i : Fin 2), WeightedClasses.MeanClass s 0 fun (n : ℕ) (x : D) => T n x i)
(hζ : ∀ x ∈ s.domain, 0 < s.zeta x)
{b M c : ℝ}
(hb : 0 < b)
(hM : 1 ≤ M)
(hc : 0 < c)
(hdet :
∀ (n : ℕ),
∀ x ∈ s.domain, b ≤ |Matrix.det (PrimaryPulseBounds.normalizedMatrix (√(s.slow n)) (phaseMatrix F pref χ n x))|)
(hentry : ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ (i j : Fin 2), |√(s.slow n) * phaseMatrix F pref χ n x i j| ≤ M)
(hlower :
∀ (n : ℕ),
∀ x ∈ s.domain, ∀ (j : Fin 2), c * s.zeta x ≤ SmoothCovariance.weights (phaseMatrix F pref χ n x) (T n x) j)
:
CovarianceControl s (phaseMatrix F pref χ) T
The matrix jets in this constructor are proved from the actual primary ODE, including its Gaussian initial normalization and slot integrals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.SignedWaveUpdate.phase_signedVector_class
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow}
(F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U)
(pref : Fin 2 → ℕ → ℝ)
(χ : ℕ → D → PhaseCalculus.Slow × ℝ)
(T R : ℕ → D → Vec2)
(mask : ℕ → D → ℝ)
(hscale : ∀ (n : ℕ), U.scale n = s.slow n)
(hχ : PhaseJetBounds.PolynomialJets (PrimaryPulseBounds.phaseDomain s) χ)
(hmap : ∀ (n : ℕ), ∀ x ∈ s.domain, χ n x ∈ U.carrier n ×ˢ Set.Ioo 0 1)
(hpref : ∀ (j : Fin 2), PhaseJetBounds.PolynomialJets U fun (n : ℕ) (x : PhaseCalculus.Slow) => pref j n)
(hT : ∀ (i : Fin 2), WeightedClasses.MeanClass s 0 fun (n : ℕ) (x : D) => T n x i)
(hζ : ∀ x ∈ s.domain, 0 < s.zeta x)
{b M c : ℝ}
(hb : 0 < b)
(hM : 1 ≤ M)
(hc : 0 < c)
(hdet :
∀ (n : ℕ),
∀ x ∈ s.domain, b ≤ |Matrix.det (PrimaryPulseBounds.normalizedMatrix (√(s.slow n)) (phaseMatrix F pref χ n x))|)
(hentry : ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ (i j : Fin 2), |√(s.slow n) * phaseMatrix F pref χ n x i j| ≤ M)
(hlower :
∀ (n : ℕ),
∀ x ∈ s.domain, ∀ (j : Fin 2), c * s.zeta x ≤ SmoothCovariance.weights (phaseMatrix F pref χ n x) (T n x) j)
{B κ : ℝ}
(hR : ∀ (i : Fin 2), WeightedClasses.MeanClass s (B - 1 / 2 - κ) fun (n : ℕ) (x : D) => R n x i)
(hm : WeightedClasses.UnweightedClass s 0 mask)
(j : Fin 2)
:
WeightedClasses.WaveClass s (phaseEnvelope F χ j) (B - κ)
(signedVector s (phaseMatrix F pref χ) T R mask (phaseFundamental F χ j) j)
Same phase fundamental, same integrated matrix, arbitrary signed target. There is no assumed estimate for the inverse, the fundamental, or the result.
Literal harmonic blocks, with the same carrier metadata #
noncomputable def
NavierStokes.SignedWaveUpdate.coefficientBlock
{D : Type}
(frequency : ℕ → ℝ)
(phase : ℕ → D → ℝ)
(angularFrequency : ℕ → ℤ)
(v : ℕ → D → HarmonicCalculus.ComplexVector)
(p : ℕ → D → ℂ)
:
Coefficient block, bundling velocity, pressure, frequency, phase and the required
compatibility proofs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.SignedWaveUpdate.coefficientBlock_band
{D : Type}
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
(v : ℕ → D → HarmonicCalculus.ComplexVector)
(p : ℕ → D → ℂ)
:
(coefficientBlock k Φ kp v p).BandLimited 1
theorem
NavierStokes.SignedWaveUpdate.coefficientBlock_symmetric
{D : Type}
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
(v : ℕ → D → HarmonicCalculus.ComplexVector)
(p : ℕ → D → ℂ)
:
(∀ (n : ℕ) (i : Fin 3), HarmonicFields.ConjugateSymmetric ((coefficientBlock k Φ kp v p).velocity n i)) ∧ ∀ (n : ℕ), HarmonicFields.ConjugateSymmetric ((coefficientBlock k Φ kp v p).pressure n)
theorem
NavierStokes.SignedWaveUpdate.coefficientBlock_velocity
{D : Type}
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
(v : ℕ → D → HarmonicCalculus.ComplexVector)
(p : ℕ → D → ℂ)
(n : ℕ)
(x : D × ℝ)
(i : Fin 3)
:
(coefficientBlock k Φ kp v p).oscillation n x i = (v n x.1 i * HarmonicFields.character 1 (k n * Φ n x.1 + ↑(kp n) * x.2)).re
theorem
NavierStokes.SignedWaveUpdate.coefficientBlock_pressure
{D : Type}
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
(v : ℕ → D → HarmonicCalculus.ComplexVector)
(p : ℕ → D → ℂ)
(n : ℕ)
(x : D × ℝ)
:
(coefficientBlock k Φ kp v p).oscillatoryPressure n x = (p n x.1 * HarmonicFields.character 1 (k n * Φ n x.1 + ↑(kp n) * x.2)).re
theorem
NavierStokes.SignedWaveUpdate.conjugatePair_class
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{w : ℕ → D → ℝ}
{α : ℝ}
{a : ℕ → D → ℂ}
(ha : WeightedClasses.MemClass s w α a)
(j : ℤ)
:
WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => (ErrorHarmonics.conjugatePair 1 (a n)).coeff j x
theorem
NavierStokes.SignedWaveUpdate.coefficientBlock_classes
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{α γ : ℝ}
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
{v : ℕ → D → HarmonicCalculus.ComplexVector}
{p : ℕ → D → ℂ}
(hv : WeightedClasses.WaveClass s P α v)
(hp : WeightedClasses.WaveClass s P γ p)
:
CorrectionState.HarmonicBlock.WaveBounds s P α (coefficientBlock k Φ kp v p) ∧ CorrectionState.HarmonicBlock.PressureBounds s P γ (coefficientBlock k Φ kp v p)
noncomputable def
NavierStokes.SignedWaveUpdate.blockOfCoefficients
{D : Type}
(a : LinearWaveBounds.WaveCoefficients (D × ℝ))
(kp : ℕ → ℤ)
:
The full cylindrical construction is evaluated at angle zero to obtain
the coefficient algebra. Its physical angle is reintroduced by the unchanged
integer carrier, as proved in blockOfCoefficients_represents.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.SignedWaveUpdate.blockOfCoefficients_represents
{D : Type}
(a : LinearWaveBounds.WaveCoefficients (D × ℝ))
(kp : ℕ → ℤ)
(ha : ErrorHarmonics.AngleIndependent a.amplitude)
(hp : ErrorHarmonics.AngleIndependent a.pressure)
(hphase : ∀ (n : ℕ) (x : D) (θ : ℝ), a.frequency n * a.phase n (x, θ) = a.frequency n * a.phase n (x, 0) + ↑(kp n) * θ)
:
((blockOfCoefficients a kp).oscillation = fun (n : ℕ) (x : D × ℝ) (i : Fin 3) =>
(HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) (a.amplitude n) x i).re) ∧ (blockOfCoefficients a kp).oscillatoryPressure = fun (n : ℕ) (x : D × ℝ) =>
(HarmonicCalculus.mode (a.frequency n) (a.phase n) (a.pressure n) x).re
The bar operation preserves the actual flat mean class #
theorem
NavierStokes.SignedWaveUpdate.meanClass_radialAverage
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a b cL cR : ℝ}
(ha : 0 < a)
(hcL : 0 < cL)
(hcR : 0 < cR)
(ε S : ℕ → ℝ)
(hε : ∀ (n : ℕ), 0 < ε n)
(hεone : ∀ (n : ℕ), ε n ≤ 1)
(hS : ∀ (n : ℕ), 1 ≤ S n)
{α : ℝ}
{f : ℕ → ℝ × E → ℝ}
(hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n))
(hglobal : MeanMomentBounds.GlobalBandJets ε S α f)
(hclass : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α f)
(L : ℝ × E →L[ℝ] ℝ × E)
(hL : ‖L‖ ≤ 1)
(v : ℝ × E)
(hpreserve : ∀ (x : ℝ × E) (t : ℝ), (L x + t • v).1 = x.1)
:
WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α fun (n : ℕ) =>
MeanMomentBounds.affineAverage L v 0 1 (f n)
theorem
NavierStokes.SignedWaveUpdate.meanClass_liftedTorusAverage
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a b cL cR : ℝ}
(ha : 0 < a)
(hcL : 0 < cL)
(hcR : 0 < cR)
(ε S : ℕ → ℝ)
(hε : ∀ (n : ℕ), 0 < ε n)
(hεone : ∀ (n : ℕ), ε n ≤ 1)
(hS : ∀ (n : ℕ), 1 ≤ S n)
{α : ℝ}
{f : ℕ → PressureStream.Lift E → ℝ}
(hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n))
(hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (f n))
(hclass : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α f)
:
WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α fun (n : ℕ) =>
MeanMomentBounds.liftedTorusAverage (f n)
theorem
NavierStokes.SignedWaveUpdate.sigma_liftedTorusAverage
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(p : SignedStressPrimitive.Patch)
(e : ℕ)
(f : PressureStream.Lift E → ℝ)
(x : PressureStream.Lift E)
:
SignedStressPrimitive.sigma p e (MeanMomentBounds.liftedTorusAverage f) x = SignedStressPrimitive.barSigma p e f (x.1, x.2.1)
theorem
NavierStokes.SignedWaveUpdate.meanClass_barSigma
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(p : SignedStressPrimitive.Patch)
(e : ℕ)
{cL cR : ℝ}
(hcL : 0 < cL)
(hcR : 0 < cR)
(ε S : ℕ → ℝ)
(hε : ∀ (n : ℕ), 0 < ε n)
(hεone : ∀ (n : ℕ), ε n ≤ 1)
(hS : ∀ (n : ℕ), 1 ≤ S n)
{α : ℝ}
{f : ℕ → PressureStream.Lift E → ℝ}
(hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n))
(hs : ∀ (n : ℕ), RadialAlias.RadiallySupported p.a p.b (f n))
(hclass : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData p.a p.b cL cR ⋯ hcL hcR ε S hε hεone hS) α f)
:
WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData p.a p.b cL cR ⋯ hcL hcR ε S hε hεone hS) α
fun (n : ℕ) (x : PressureStream.Lift E) => SignedStressPrimitive.barSigma p e (f n) (x.1, x.2.1)
noncomputable def
NavierStokes.SignedWaveUpdate.normalizedRequest
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(s : WeightedClasses.StripData (PressureStream.Lift E))
(p : SignedStressPrimitive.Patch)
(c : CorrectionState.Context (PressureStream.Lift E))
(u : CorrectionState.State (PressureStream.Lift E))
:
ℕ → PressureStream.Lift E → Vec2
Normalized request, defined pointwise by (s.epsilon n)⁻¹ • requestedStress p c u n (x.1,x.2.1).
Equations
- NavierStokes.SignedWaveUpdate.normalizedRequest s p c u n x = (s.epsilon n)⁻¹ • NavierStokes.SignedWaveUpdate.requestedStress p c u n (x.1, x.2.1)
Instances For
theorem
NavierStokes.SignedWaveUpdate.normalizedRequest_frozen
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(s : WeightedClasses.StripData (PressureStream.Lift E))
(p : SignedStressPrimitive.Patch)
(c : CorrectionState.Context (PressureStream.Lift E))
(u : CorrectionState.State (PressureStream.Lift E))
(v : PressureStream.Plane)
:
FrozenAlong (0, 0, v) (normalizedRequest s p c u)
theorem
NavierStokes.SignedWaveUpdate.normalizedRequest_class
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(p : SignedStressPrimitive.Patch)
{cL cR : ℝ}
(hcL : 0 < cL)
(hcR : 0 < cR)
(ε S : ℕ → ℝ)
(hε : ∀ (n : ℕ), 0 < ε n)
(hεone : ∀ (n : ℕ), ε n ≤ 1)
(hS : ∀ (n : ℕ), 1 ≤ S n)
(c : CorrectionState.Context (PressureStream.Lift E))
(u : CorrectionState.State (PressureStream.Lift E))
{α : ℝ}
(ht : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (u.thetaResidual c n))
(hz : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (u.axialResidual c n))
(hst : ∀ (n : ℕ), RadialAlias.RadiallySupported p.a p.b (u.thetaResidual c n))
(hsz : ∀ (n : ℕ), RadialAlias.RadiallySupported p.a p.b (u.axialResidual c n))
(hct :
WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData p.a p.b cL cR ⋯ hcL hcR ε S hε hεone hS) α
(u.thetaResidual c))
(hcz :
WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData p.a p.b cL cR ⋯ hcL hcR ε S hε hεone hS) α
(u.axialResidual c))
(i : Fin 2)
:
WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData p.a p.b cL cR ⋯ hcL hcR ε S hε hεone hS) (α - 1)
fun (n : ℕ) (x : ℝ × E × PressureStream.Plane) =>
normalizedRequest (WeightedRadialPrimitive.logStripData p.a p.b cL cR ⋯ hcL hcR ε S hε hεone hS) p c u n x i
Angular independence is proved before taking a zero-angle section #
structure
NavierStokes.SignedWaveUpdate.AngularInputs
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(s : WeightedClasses.StripData D)
(d : LinearWaveBounds.GraphDirections D)
(a : LinearWaveBounds.WaveCoefficients D)
(H : ℕ → D → Mat2)
(T R : ℕ → D → Vec2)
(mask : ℕ → D → ℝ)
(v Ndot : ℕ → D → Space)
(A : ℕ → D → Space →L[ℝ] Space)
(ψ : ℕ → D → ℝ)
(m : ℕ → ℝ)
:
Angular inputs data, collecting radius, radial_base, frequency_base, axial_base,
radial_profile, phase and their compatibility conditions.
- radius : FrozenAlong d.angular a.radius
- radial_base : FrozenAlong d.angular a.radialBase
- frequency_base : FrozenAlong d.angular a.frequencyBase
- axial_base : FrozenAlong d.angular a.axialBase
- radial_profile : CopyAngularInvariance.Invariant d.angular d.radialProfile
- phase (n : ℕ) : CopyAngularInvariance.AffinePhase d.angular (m n) (a.phase n)
- matrix : FrozenAlong d.angular H
- primary_target : FrozenAlong d.angular T
- signed_target : FrozenAlong d.angular R
- mask : FrozenAlong d.angular mask
- fundamental : FrozenAlong d.angular v
- normal_motion : FrozenAlong d.angular Ndot
- action : FrozenAlong d.angular A
- cutoff : FrozenAlong d.angular ψ
Instances For
theorem
NavierStokes.SignedWaveUpdate.AngularInputs.radialField
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{a : LinearWaveBounds.WaveCoefficients D}
{H : ℕ → D → Mat2}
{T R : ℕ → D → Vec2}
{mask : ℕ → D → ℝ}
{v Ndot : ℕ → D → Space}
{A : ℕ → D → Space →L[ℝ] Space}
{ψ : ℕ → D → ℝ}
{m : ℕ → ℝ}
(h : AngularInputs s d a H T R mask v Ndot A ψ m)
(n : ℕ)
:
theorem
NavierStokes.SignedWaveUpdate.AngularInputs.normal
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{a : LinearWaveBounds.WaveCoefficients D}
{H : ℕ → D → Mat2}
{T R : ℕ → D → Vec2}
{mask : ℕ → D → ℝ}
{v Ndot : ℕ → D → Space}
{A : ℕ → D → Space →L[ℝ] Space}
{ψ : ℕ → D → ℝ}
{m : ℕ → ℝ}
(h : AngularInputs s d a H T R mask v Ndot A ψ m)
(n : ℕ)
:
CopyAngularInvariance.Invariant d.angular (a.normal s d n)
theorem
NavierStokes.SignedWaveUpdate.AngularInputs.amplitude
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{a : LinearWaveBounds.WaveCoefficients D}
{H : ℕ → D → Mat2}
{T R : ℕ → D → Vec2}
{mask : ℕ → D → ℝ}
{v Ndot : ℕ → D → Space}
{A : ℕ → D → Space →L[ℝ] Space}
{ψ : ℕ → D → ℝ}
{m : ℕ → ℝ}
(h : AngularInputs s d a H T R mask v Ndot A ψ m)
(j : Fin 2)
(n : ℕ)
:
CopyAngularInvariance.Invariant d.angular ((coefficients a s d H T R mask v Ndot A j).amplitude n)
theorem
NavierStokes.SignedWaveUpdate.AngularInputs.pressure
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{a : LinearWaveBounds.WaveCoefficients D}
{H : ℕ → D → Mat2}
{T R : ℕ → D → Vec2}
{mask : ℕ → D → ℝ}
{v Ndot : ℕ → D → Space}
{A : ℕ → D → Space →L[ℝ] Space}
{ψ : ℕ → D → ℝ}
{m : ℕ → ℝ}
(h : AngularInputs s d a H T R mask v Ndot A ψ m)
(j : Fin 2)
(n : ℕ)
:
CopyAngularInvariance.Invariant d.angular ((coefficients a s d H T R mask v Ndot A j).pressure n)
theorem
NavierStokes.SignedWaveUpdate.AngularInputs.corrected_amplitude
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{a : LinearWaveBounds.WaveCoefficients D}
{H : ℕ → D → Mat2}
{T R : ℕ → D → Vec2}
{mask : ℕ → D → ℝ}
{v Ndot : ℕ → D → Space}
{A : ℕ → D → Space →L[ℝ] Space}
{ψ : ℕ → D → ℝ}
{m : ℕ → ℝ}
(h : AngularInputs s d a H T R mask v Ndot A ψ m)
(j : Fin 2)
(n : ℕ)
:
CopyAngularInvariance.Invariant d.angular (((coefficients a s d H T R mask v Ndot A j).corrected s d ψ).amplitude n)
theorem
NavierStokes.SignedWaveUpdate.AngularInputs.corrected_pressure
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{a : LinearWaveBounds.WaveCoefficients D}
{H : ℕ → D → Mat2}
{T R : ℕ → D → Vec2}
{mask : ℕ → D → ℝ}
{v Ndot : ℕ → D → Space}
{A : ℕ → D → Space →L[ℝ] Space}
{ψ : ℕ → D → ℝ}
{m : ℕ → ℝ}
(h : AngularInputs s d a H T R mask v Ndot A ψ m)
(j : Fin 2)
(n : ℕ)
:
CopyAngularInvariance.Invariant d.angular (((coefficients a s d H T R mask v Ndot A j).corrected s d ψ).pressure n)
theorem
NavierStokes.SignedWaveUpdate.AngularInputs.exactConditions
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{a : LinearWaveBounds.WaveCoefficients D}
{H : ℕ → D → Mat2}
{T R : ℕ → D → Vec2}
{mask : ℕ → D → ℝ}
{v Ndot : ℕ → D → Space}
{A : ℕ → D → Space →L[ℝ] Space}
{ψ : ℕ → D → ℝ}
{m : ℕ → ℝ}
(h : AngularInputs s d a H T R mask v Ndot A ψ m)
(hRne : ∀ (n : ℕ), ∀ x ∈ s.domain, a.radius n x ≠ 0)
(hDrR : ∀ (n : ℕ), ∀ x ∈ s.domain, HarmonicCalculus.along (d.radialField n) (a.radius n) x = 1)
(j : Fin 2)
:
LinearWaveBounds.ExactConditions s d ((coefficients a s d H T R mask v Ndot A j).corrected s d ψ)
theorem
NavierStokes.SignedWaveUpdate.signedBlock_represents
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData (D × ℝ)}
{d : LinearWaveBounds.GraphDirections (D × ℝ)}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{H : ℕ → D × ℝ → Mat2}
{T R : ℕ → D × ℝ → Vec2}
{mask : ℕ → D × ℝ → ℝ}
{v Ndot : ℕ → D × ℝ → Space}
{A : ℕ → D × ℝ → Space →L[ℝ] Space}
{ψ : ℕ → D × ℝ → ℝ}
{m : ℕ → ℝ}
(h : AngularInputs s d a H T R mask v Ndot A ψ m)
(hθ : d.angular = (0, 1))
(kp : ℕ → ℤ)
(hkp : ∀ (n : ℕ), a.frequency n * m n = ↑(kp n))
(j : Fin 2)
:
have z := (coefficients a s d H T R mask v Ndot A j).corrected s d ψ;
((blockOfCoefficients z kp).oscillation = fun (n : ℕ) (x : D × ℝ) (i : Fin 3) =>
(HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) (z.amplitude n) x i).re) ∧ (blockOfCoefficients z kp).oscillatoryPressure = fun (n : ℕ) (x : D × ℝ) =>
(HarmonicCalculus.mode (a.frequency n) (a.phase n) (z.pressure n) x).re
Restriction of actual coefficient jets to the angular section #
noncomputable def
NavierStokes.SignedWaveUpdate.zeroSection
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
:
Zero section, given by (ContinuousLinearMap.id ℝ D).prod 0.
Equations
Instances For
theorem
NavierStokes.SignedWaveUpdate.zeroSection_norm_le
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
:
noncomputable def
NavierStokes.SignedWaveUpdate.sectionStrip
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(s : WeightedClasses.StripData (D × ℝ))
:
Section strip, bundling domain, isOpen_domain, epsilon, epsilon_pos and the required
compatibility proofs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.SignedWaveUpdate.class_zeroSection
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData (D × ℝ)}
{w : ℕ → D × ℝ → ℝ}
{α : ℝ}
{f : ℕ → D × ℝ → E}
(hf : WeightedClasses.MemClass s w α f)
:
WeightedClasses.MemClass (sectionStrip s) (fun (n : ℕ) (x : D) => w n (x, 0)) α fun (n : ℕ) (x : D) => f n (x, 0)
theorem
NavierStokes.SignedWaveUpdate.blockOfCoefficients_classes
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData (D × ℝ)}
{P : ℕ → D × ℝ → ℝ}
{α γ : ℝ}
(a : LinearWaveBounds.WaveCoefficients (D × ℝ))
(kp : ℕ → ℤ)
(ha : WeightedClasses.WaveClass s P α a.amplitude)
(hp : WeightedClasses.WaveClass s P γ a.pressure)
:
CorrectionState.HarmonicBlock.WaveBounds (sectionStrip s) (fun (n : ℕ) (x : D) => P n (x, 0)) α
(blockOfCoefficients a kp) ∧ CorrectionState.HarmonicBlock.PressureBounds (sectionStrip s) (fun (n : ℕ) (x : D) => P n (x, 0)) γ
(blockOfCoefficients a kp)
theorem
NavierStokes.SignedWaveUpdate.angularAverage_re_field
{D : Type}
(c : HarmonicFields.Coefficients D)
(k : ℝ)
(Φ : D → ℝ)
(kp : ℤ)
(x : D)
:
theorem
NavierStokes.SignedWaveUpdate.coefficientBlock_mean_zero
{D : Type}
(k : ℕ → ℝ)
(Φ : ℕ → D → ℝ)
(kp : ℕ → ℤ)
(v : ℕ → D → HarmonicCalculus.ComplexVector)
(p : ℕ → D → ℂ)
(hkp : ∀ (n : ℕ), kp n ≠ 0)
:
(∀ (i : Fin 3),
(CorrectionState.angularAverage fun (n : ℕ) (x : D × ℝ) => (coefficientBlock k Φ kp v p).oscillation n x i) = 0) ∧ CorrectionState.angularAverage (coefficientBlock k Φ kp v p).oscillatoryPressure = 0
These are actual angular integrals of the real velocity and pressure.
Actual homogeneous ODE under the native clock #
theorem
NavierStokes.SignedWaveUpdate.normalizedPulse_along
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{Q : Type}
[NormedAddCommGroup Q]
(f : PrimaryODE.FrameData Q)
(lam u : ℝ)
{L : ℝ}
(hL : 0 < L)
(U : Set Q)
(hA : ContinuousOn (f.coefficient 1) (U ×ˢ Set.Icc 0 L))
(χ : D → Q × ℝ)
(V : D → D)
{x : D}
(hp : (χ x).1 ∈ U)
(ht : (χ x).2 ∈ Set.Ioo 0 1)
(hk : f.Kinematics (χ x).1 (Set.Icc 0 L))
(hv : DifferentiableAt ℝ (fun (y : D) => PrimaryPulseBounds.normalizedPulse f lam u L (χ y)) x)
(hclock : ∀ (t : ℝ), χ (x + t • V x) = ((χ x).1, (χ x).2 + t / L))
:
HarmonicCalculus.along V (fun (y : D) => PrimaryPulseBounds.normalizedPulse f lam u L (χ y)) x = TangentProjection.projectedRhs (f.normal ((χ x).1, L * (χ x).2)) (f.normalMotion ((χ x).1, L * (χ x).2))
(PrimaryPulseBounds.normalizedPulse f lam u L (χ x))
(MovingFrameODE.baseAction (f.F ((χ x).1, L * (χ x).2)) (f.shear ((χ x).1, L * (χ x).2))
(PrimaryPulseBounds.normalizedPulse f lam u L (χ x)))
0 (f.viscosity ((χ x).1, L * (χ x).2))
theorem
NavierStokes.SignedWaveUpdate.phaseFundamental_tangent
{D : Type}
{U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow}
(F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U)
(χ : ℕ → D → PhaseCalculus.Slow × ℝ)
(j : Fin 2)
(n : ℕ)
(x : D)
:
theorem
NavierStokes.SignedWaveUpdate.phase_coefficients_principal_zero
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
(a : LinearWaveBounds.WaveCoefficients D)
{U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow}
(F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U)
(pref : Fin 2 → ℕ → ℝ)
(χ : ℕ → D → PhaseCalculus.Slow × ℝ)
{T R : ℕ → D → Vec2}
{mask : ℕ → D → ℝ}
{Ndot : ℕ → D → Space}
{A : ℕ → D → Space →L[ℝ] Space}
(hscale : ∀ (n : ℕ), U.scale n = s.slow n)
(hχ : PhaseJetBounds.PolynomialJets (PrimaryPulseBounds.phaseDomain s) χ)
(hmap : ∀ (n : ℕ), ∀ x ∈ s.domain, χ n x ∈ U.carrier n ×ˢ Set.Ioo 0 1)
(hcov : CovarianceControl s (phaseMatrix F pref χ) T)
{β : ℝ}
(hR : ∀ (i : Fin 2), WeightedClasses.MeanClass s β fun (n : ℕ) (x : D) => R n x i)
(hm : WeightedClasses.UnweightedClass s 0 mask)
(hHf : FrozenAlong d.fast (phaseMatrix F pref χ))
(hTf : FrozenAlong d.fast T)
(hRf : FrozenAlong d.fast R)
(hmf : FrozenAlong d.fast mask)
(hK : ∀ (n : ℕ), a.frequency n ≠ 0)
(j : Fin 2)
(hcoef : ∀ (n : ℕ), ContinuousOn (((F j).frame n).coefficient 1) (U.carrier n ×ˢ Set.Icc 0 ((F j).L n)))
(hkin : ∀ (n : ℕ), ∀ x ∈ s.domain, ((F j).frame n).Kinematics (χ n x).1 (Set.Icc 0 ((F j).L n)))
(hclock : ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ (t : ℝ), χ n (x + t • d.fastField n x) = ((χ n x).1, (χ n x).2 + t / (F j).L n))
(hnormal : ∀ (n : ℕ), ∀ x ∈ s.domain, ((F j).frame n).normal ((χ n x).1, (F j).L n * (χ n x).2) = a.normal s d n x)
(hmotion : ∀ (n : ℕ), ∀ x ∈ s.domain, ((F j).frame n).normalMotion ((χ n x).1, (F j).L n * (χ n x).2) = Ndot n x)
(haction :
∀ (n : ℕ),
∀ x ∈ s.domain,
∀ (z : Space),
MovingFrameODE.baseAction (((F j).frame n).F ((χ n x).1, (F j).L n * (χ n x).2))
(((F j).frame n).shear ((χ n x).1, (F j).L n * (χ n x).2)) z = (A n x) z)
(hdamp :
∀ (n : ℕ),
∀ x ∈ s.domain,
((F j).frame n).viscosity ((χ n x).1, (F j).L n * (χ n x).2) = s.epsilon n * a.frequency n ^ 2 * ‖a.normal s d n x‖ ^ 2)
(hphysical :
∀ (n : ℕ),
∀ x ∈ s.domain,
CurlClassBounds.complexify ((A n x) (phaseFundamental F χ j n x)) = LinearWaveResidual.shear (a.radius n) (a.frequencyBase n) (a.axialBase n) (d.radialField n)
(fun (y : D) => CurlClassBounds.complexify (phaseFundamental F χ j n y)) x)
(n : ℕ)
(x : D)
:
x ∈ s.domain →
(coefficients a s d (phaseMatrix F pref χ) T R mask (phaseFundamental F χ j) Ndot A j).principal s d n x = 0
The constructed curl, pressure, and retained linear error #
noncomputable def
NavierStokes.SignedWaveUpdate.exactCoefficients
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(a : LinearWaveBounds.WaveCoefficients D)
(s : WeightedClasses.StripData D)
(d : LinearWaveBounds.GraphDirections D)
(H : ℕ → D → Mat2)
(T R : ℕ → D → Vec2)
(mask : ℕ → D → ℝ)
(v Ndot : ℕ → D → Space)
(A : ℕ → D → Space →L[ℝ] Space)
(ψ : ℕ → D → ℝ)
(j : Fin 2)
:
Exact coefficients, given by (coefficients a s d H T R mask v Ndot A j).corrected s d ψ.
Equations
- NavierStokes.SignedWaveUpdate.exactCoefficients a s d H T R mask v Ndot A ψ j = (NavierStokes.SignedWaveUpdate.coefficients a s d H T R mask v Ndot A j).corrected s d ψ
Instances For
theorem
NavierStokes.SignedWaveUpdate.signed_bounds
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{a : LinearWaveBounds.WaveCoefficients D}
{P₀ P : ℕ → D → ℝ}
{α₀ B κ : ℝ}
(hbase : LinearWaveBounds.InputBounds s P₀ α₀ κ d a)
(hκ : κ ≤ 1 / 2)
{H : ℕ → D → Mat2}
{T R : ℕ → D → Vec2}
{mask ψ : ℕ → D → ℝ}
{v Ndot : ℕ → D → Space}
{A : ℕ → D → Space →L[ℝ] Space}
(hcov : CovarianceControl s H T)
(hR : ∀ (i : Fin 2), WeightedClasses.MeanClass s (B - 1 / 2 - κ) fun (n : ℕ) (x : D) => R n x i)
(hm : WeightedClasses.UnweightedClass s 0 mask)
(hv : WeightedClasses.MemClass s P 0 v)
(hN : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain s) (a.normal s d))
(hNdot : WeightedClasses.UnweightedClass s 0 Ndot)
(hA : WeightedClasses.UnweightedClass s 0 A)
{b M : ℝ}
(hb : 0 < b)
(hlo : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ ‖a.normal s d n x‖)
(hhi : ∀ (n : ℕ), ∀ x ∈ s.domain, ‖a.normal s d n x‖ ≤ M)
(hK : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / a.frequency n)
{radius : D → ℝ}
(hradius : a.radius = fun (x : ℕ) => radius)
(hψ : WeightedClasses.UnweightedClass s 0 ψ)
(j : Fin 2)
:
have z := coefficients a s d H T R mask v Ndot A j;
WeightedClasses.WaveClass s P (B - κ) (z.corrected s d ψ).amplitude ∧ WeightedClasses.WaveClass s P (B + 1 / 2 - κ) (z.corrected s d ψ).pressure ∧ (WeightedClasses.WaveClass s P (B + 1 / 2 - 2 * κ) fun (n : ℕ) (x : D) =>
(z.corrected s d ψ).amplitude n x - (z.withCutoff ψ).amplitude n x) ∧ WeightedClasses.WaveClass s P (B + 1 / 2 - 4 * κ) (z.constructedGood s d ψ)
theorem
NavierStokes.SignedWaveUpdate.coefficients_tangent
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
(a : LinearWaveBounds.WaveCoefficients D)
(H : ℕ → D → Mat2)
(T R : ℕ → D → Vec2)
(mask : ℕ → D → ℝ)
(v Ndot : ℕ → D → Space)
(A : ℕ → D → Space →L[ℝ] Space)
(ht : ∀ (n : ℕ), ∀ x ∈ s.domain, inner ℝ (a.normal s d n x) (v n x) = 0)
(j : Fin 2)
(n : ℕ)
{x : D}
(hx : x ∈ s.domain)
:
HarmonicCalculus.normalDot ((coefficients a s d H T R mask v Ndot A j).normal s d n x)
((coefficients a s d H T R mask v Ndot A j).amplitude n x) = 0
theorem
NavierStokes.SignedWaveUpdate.signed_curl_realization
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{a : LinearWaveBounds.WaveCoefficients D}
{P₀ P : ℕ → D → ℝ}
{α₀ β κ : ℝ}
(hbase : LinearWaveBounds.InputBounds s P₀ α₀ κ d a)
{H : ℕ → D → Mat2}
{T R : ℕ → D → Vec2}
{mask ψ : ℕ → D → ℝ}
{v Ndot : ℕ → D → Space}
{A : ℕ → D → Space →L[ℝ] Space}
(hcov : CovarianceControl s H T)
(hR : ∀ (i : Fin 2), WeightedClasses.MeanClass s β fun (n : ℕ) (x : D) => R n x i)
(hm : WeightedClasses.UnweightedClass s 0 mask)
(hv : WeightedClasses.MemClass s P 0 v)
(hN : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain s) (a.normal s d))
(hNdot : WeightedClasses.UnweightedClass s 0 Ndot)
(hA : WeightedClasses.UnweightedClass s 0 A)
{b M : ℝ}
(hb : 0 < b)
(hlo : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ ‖a.normal s d n x‖)
(hhi : ∀ (n : ℕ), ∀ x ∈ s.domain, ‖a.normal s d n x‖ ≤ M)
(hK : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / a.frequency n)
(hψ : WeightedClasses.UnweightedClass s 0 ψ)
(j : Fin 2)
(n : ℕ)
(G :
CurlClassBounds.CylindricalGeometry s.domain (a.radius n) (d.radialField n) (fun (x : D) => d.angular)
(d.axialField s n))
(hfreq : a.frequency n ≠ 0)
(hphase : ContDiffOn ℝ (↑⊤) (a.phase n) s.domain)
(ht : ∀ (n : ℕ), ∀ x ∈ s.domain, inner ℝ (a.normal s d n x) (v n x) = 0)
:
have z := coefficients a s d H T R mask v Ndot A j;
∀ x ∈ s.domain,
CurlClassBounds.cylindricalCurl (a.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n)
((z.withCutoff ψ).curlPotential s d n) x = HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) ((z.corrected s d ψ).amplitude n) x ∧ HarmonicCalculus.cylindricalDivergence (a.radius n) (d.radialField n) (fun (x : D) => d.angular) (d.axialField s n)
(HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) ((z.corrected s d ψ).amplitude n)) x = 0
theorem
NavierStokes.SignedWaveUpdate.signed_linear_identity
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
{a : LinearWaveBounds.WaveCoefficients D}
{P₀ P : ℕ → D → ℝ}
{α₀ β κ : ℝ}
(hbase : LinearWaveBounds.InputBounds s P₀ α₀ κ d a)
(hκ : κ ≤ 1 / 2)
{H : ℕ → D → Mat2}
{T R : ℕ → D → Vec2}
{mask ψ : ℕ → D → ℝ}
{v Ndot : ℕ → D → Space}
{A : ℕ → D → Space →L[ℝ] Space}
(hcov : CovarianceControl s H T)
(hR : ∀ (i : Fin 2), WeightedClasses.MeanClass s β fun (n : ℕ) (x : D) => R n x i)
(hm : WeightedClasses.UnweightedClass s 0 mask)
(hv : WeightedClasses.MemClass s P 0 v)
(hN : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain s) (a.normal s d))
(hNdot : WeightedClasses.UnweightedClass s 0 Ndot)
(hA : WeightedClasses.UnweightedClass s 0 A)
{b M : ℝ}
(hb : 0 < b)
(hlo : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ ‖a.normal s d n x‖)
(hhi : ∀ (n : ℕ), ∀ x ∈ s.domain, ‖a.normal s d n x‖ ≤ M)
(hK : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / a.frequency n)
{radius : D → ℝ}
(hradius : a.radius = fun (x : ℕ) => radius)
(hψ : WeightedClasses.UnweightedClass s 0 ψ)
{m : ℕ → ℝ}
(hangle : AngularInputs s d a H T R mask v Ndot A ψ m)
(hG :
∀ (n : ℕ),
CurlClassBounds.CylindricalGeometry s.domain (a.radius n) (d.radialField n) (fun (x : D) => d.angular)
(d.axialField s n))
(hHf : FrozenAlong d.fast H)
(hTf : FrozenAlong d.fast T)
(hRf : FrozenAlong d.fast R)
(hmf : FrozenAlong d.fast mask)
(hfreq : ∀ (n : ℕ), a.frequency n ≠ 0)
(hode :
∀ (n : ℕ),
∀ x ∈ s.domain,
HarmonicCalculus.along (d.fastField n) (v n) x = TangentProjection.projectedRhs (a.normal s d n x) (Ndot n x) (v n x) ((A n x) (v n x)) 0
(s.epsilon n * a.frequency n ^ 2 * ‖a.normal s d n x‖ ^ 2))
(haction :
∀ (n : ℕ),
∀ x ∈ s.domain,
CurlClassBounds.complexify ((A n x) (v n x)) = LinearWaveResidual.shear (a.radius n) (a.frequencyBase n) (a.axialBase n) (d.radialField n)
(fun (y : D) => CurlClassBounds.complexify (v n y)) x)
(j : Fin 2)
:
have z := coefficients a s d H T R mask v Ndot A j;
∀ (n : ℕ),
∀ x ∈ s.domain,
(z.corrected s d ψ).harmonicResidual s d n x = fun (i : Fin 3) =>
(z.constructedGood s d ψ n x i + LinearWaveBounds.excludedSlotError d ψ z.amplitude 0 n x i) * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x
Exact residual identity for the signed increment. The slot derivative is kept as a separate nonzero field and is not included in the good bound.
The same native pulse blocks in the exact covariance identity #
noncomputable def
NavierStokes.SignedWaveUpdate.nativeUnit
{D h : ℝ}
{vr vt : TorusInverse.Plane}
{sys : PartitionedCovariance.SlotSystem D h vr vt}
{U : PartitionedCovariance.UnsignedLabel}
(P : PartitionedCovariance.PairData sys U)
(hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0)
(j : Fin 2)
(Y : TorusInverse.Plane)
:
Native unit as an element of Space.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.SignedWaveUpdate.nativeTangentBlock
{D h : ℝ}
{vr vt : TorusInverse.Plane}
{sys : PartitionedCovariance.SlotSystem D h vr vt}
{U : PartitionedCovariance.UnsignedLabel}
(P : PartitionedCovariance.PairData sys U)
(hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0)
(outer ε : ℝ)
(a : Vec2)
(q : ℝ)
(x : SlotColoring.Position)
(j : Fin 2)
:
Native tangent block, constructed using coefficientBlock.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.SignedWaveUpdate.nativeTangentBlock_radial
{D h : ℝ}
{vr vt : TorusInverse.Plane}
{sys : PartitionedCovariance.SlotSystem D h vr vt}
{U : PartitionedCovariance.UnsignedLabel}
(P : PartitionedCovariance.PairData sys U)
(hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0)
(outer ε : ℝ)
(a : Vec2)
(q : ℝ)
(x : SlotColoring.Position)
(j : Fin 2)
(n : ℕ)
(Y : TorusInverse.Plane)
(θ : ℝ)
:
(nativeTangentBlock P hdet outer ε a q x j).oscillation n (Y, θ) 0 = SignedCovariance.radialWith P hdet outer ε a q x j Y θ
theorem
NavierStokes.SignedWaveUpdate.nativeTangentBlock_tangent
{D h : ℝ}
{vr vt : TorusInverse.Plane}
{sys : PartitionedCovariance.SlotSystem D h vr vt}
{U : PartitionedCovariance.UnsignedLabel}
(P : PartitionedCovariance.PairData sys U)
(hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0)
(outer ε : ℝ)
(a : Vec2)
(q : ℝ)
(x : SlotColoring.Position)
(j i : Fin 2)
(n : ℕ)
(Y : TorusInverse.Plane)
(θ : ℝ)
:
(nativeTangentBlock P hdet outer ε a q x j).oscillation n (Y, θ) i.succ = SignedCovariance.tangentWith P hdet outer ε a q x j i Y θ
noncomputable def
NavierStokes.SignedWaveUpdate.nativeAssembly
{D h : ℝ}
{vr vt : TorusInverse.Plane}
{sys : PartitionedCovariance.SlotSystem D h vr vt}
{N : ℕ}
(P :
(U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U))
(hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0)
(outer ε : PartitionedCovariance.UnsignedLabel → ℝ)
(a : PartitionedCovariance.UnsignedLabel → Vec2)
(q : ℝ)
(x : SlotColoring.Position)
:
TorusInverse.Plane → ℝ → Fin 3 → ℝ
Native assembly, defined pointwise by ∑ᶠ v : UnsignedLabel × Fin 2, (nativeTangentBlock (P v.1) hdet (outer v.1) (ε v.1) (a v.1) q x v.2).oscillation 0 (Y,θ) i.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.SignedWaveUpdate.nativeAssembly_radial
{D h : ℝ}
{vr vt : TorusInverse.Plane}
{sys : PartitionedCovariance.SlotSystem D h vr vt}
{N : ℕ}
(P :
(U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U))
(hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0)
(outer ε : PartitionedCovariance.UnsignedLabel → ℝ)
(a : PartitionedCovariance.UnsignedLabel → Vec2)
(q : ℝ)
(x : SlotColoring.Position)
(Y : TorusInverse.Plane)
(θ : ℝ)
:
nativeAssembly P hdet outer ε a q x Y θ 0 = SignedCovariance.assembledRadialWith P hdet outer ε a q x Y θ
theorem
NavierStokes.SignedWaveUpdate.nativeAssembly_tangent
{D h : ℝ}
{vr vt : TorusInverse.Plane}
{sys : PartitionedCovariance.SlotSystem D h vr vt}
{N : ℕ}
(P :
(U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U))
(hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0)
(outer ε : PartitionedCovariance.UnsignedLabel → ℝ)
(a : PartitionedCovariance.UnsignedLabel → Vec2)
(q : ℝ)
(x : SlotColoring.Position)
(i : Fin 2)
(Y : TorusInverse.Plane)
(θ : ℝ)
:
nativeAssembly P hdet outer ε a q x Y θ i.succ = SignedCovariance.assembledTangentWith P hdet outer ε a q x i Y θ
theorem
NavierStokes.SignedWaveUpdate.nativeAssembly_requested_cross
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{D h : ℝ}
{vr vt : TorusInverse.Plane}
(sys : PartitionedCovariance.SlotSystem D h vr vt)
(hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0)
(N : ℕ)
(hN : 1 ≤ N)
(P :
(U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U))
{q : ℝ}
(hq : 0 < q)
(hqN : q ≤ ChartScales.Q N)
(x : SlotColoring.Position)
(T0 : Vec2)
(p : SignedStressPrimitive.Patch)
(c : CorrectionState.Context (PressureStream.Lift E))
(u : CorrectionState.State (PressureStream.Lift E))
(n : ℕ)
(z : ℝ × E)
(hcone :
∀ (U : PartitionedCovariance.UnsignedLabel),
PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ≠ 0 →
SmoothCovariance.StrictCone (P U).matrix (PartitionedCovariance.chartTarget h q N T0 U))
(i : Fin 2)
:
have primary :=
nativeAssembly P hdet (PartitionedCovariance.physicalOuter h N) (PartitionedCovariance.physicalViscosity h N)
(fun (U : PartitionedCovariance.UnsignedLabel) =>
SmoothCovariance.amplitudes (P U).matrix (PartitionedCovariance.chartTarget h q N T0 U))
q x;
have signed :=
nativeAssembly P hdet (PartitionedCovariance.physicalOuter h N) (PartitionedCovariance.physicalViscosity h N)
(fun (U : PartitionedCovariance.UnsignedLabel) =>
SignedCovariance.increment (P U).matrix (PartitionedCovariance.chartTarget h q N T0 U)
(SignedCovariance.chartStress h N (requestedStress p c u n z) U))
q x;
(PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (θ : ℝ) =>
primary Y θ 0 * signed Y θ i.succ + signed Y θ 0 * primary Y θ i.succ) = requestedStress p c u n z i
theorem
NavierStokes.SignedWaveUpdate.nativeAssembly_signed_square
{D h : ℝ}
{vr vt : TorusInverse.Plane}
(sys : PartitionedCovariance.SlotSystem D h vr vt)
(hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0)
(N : ℕ)
(hN : 1 ≤ N)
(P :
(U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U))
(outer ε : PartitionedCovariance.UnsignedLabel → ℝ)
(T R : PartitionedCovariance.UnsignedLabel → Vec2)
{q : ℝ}
(hq : 0 < q)
(x : SlotColoring.Position)
(hε :
∀ (U : PartitionedCovariance.UnsignedLabel),
PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ≠ 0 → 0 ≤ ε U)
(i : Fin 2)
:
have signed :=
nativeAssembly P hdet outer ε
(fun (U : PartitionedCovariance.UnsignedLabel) => SignedCovariance.increment (P U).matrix (T U) (R U)) q x;
(PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (θ : ℝ) =>
signed Y θ 0 * signed Y θ i.succ) = ∑ᶠ (U : PartitionedCovariance.UnsignedLabel), outer U ^ 2 * ε U * PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ^ 2 * SignedCovariance.squareColumn (P U).matrix (T U) (R U) i
theorem
NavierStokes.SignedWaveUpdate.signed_square_class
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{H : ℕ → D → Mat2}
{T R : ℕ → D → Vec2}
(h : CovarianceControl s H T)
(B κ : ℝ)
(hR : ∀ (i : Fin 2), WeightedClasses.MeanClass s (B - 1 / 2 - κ) fun (n : ℕ) (x : D) => R n x i)
(i : Fin 2)
:
WeightedClasses.MeanClass s (2 * B - 2 * κ) fun (n : ℕ) (x : D) =>
s.epsilon n * SignedCovariance.squareColumn (H n x) (T n x) (R n x) i
Canonical pulse binding for the matrix and the native blocks #
theorem
NavierStokes.SignedWaveUpdate.phaseMatrix_eq_canonical_pair
{D : Type}
{U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow}
(F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U)
(pref : Fin 2 → ℕ → ℝ)
(χ : ℕ → D → PhaseCalculus.Slow × ℝ)
(n : ℕ)
(x : D)
(hp : (χ n x).1 ∈ U.carrier n)
(hA : ∀ (j : Fin 2), ContinuousOn (((F j).frame n).coefficient 1) (U.carrier n ×ˢ Set.Icc 0 ((F j).L n)))
(hk : ∀ (j : Fin 2), ((F j).frame n).Kinematics (χ n x).1 (Set.Icc 0 ((F j).L n)))
{D₀ h : ℝ}
{vr vt : TorusInverse.Plane}
{sys : PartitionedCovariance.SlotSystem D₀ h vr vt}
{label : PartitionedCovariance.UnsignedLabel}
(P : PartitionedCovariance.PairData sys label)
(hpulse :
∀ (j : Fin 2),
P.pulses j = PrimaryPulseBounds.canonicalPrimaryPulse ((F j).frame n) ((F j).lam n) ((F j).u n) ⋯ (U.carrier n) ⋯ (χ n x).1 hp
⋯)
(hpref : ∀ (j : Fin 2), pref j n = PartitionedCovariance.nativePrefactor vr vt sys.radius * P.ci j * (F j).L n)
:
theorem
NavierStokes.SignedWaveUpdate.nativeUnit_eq_canonical_pulse
{Q : Type}
[NormedAddCommGroup Q]
{D₀ h : ℝ}
{vr vt : TorusInverse.Plane}
{sys : PartitionedCovariance.SlotSystem D₀ h vr vt}
{label : PartitionedCovariance.UnsignedLabel}
(P : PartitionedCovariance.PairData sys label)
(hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0)
(j : Fin 2)
(f : PrimaryODE.FrameData Q)
(lam u : ℝ)
{L : ℝ}
(hL : 0 < L)
(U : Set Q)
(hA : ContinuousOn (f.coefficient 1) (U ×ˢ Set.Icc 0 L))
(p : Q)
(hp : p ∈ U)
(hk : f.Kinematics p (Set.Icc 0 L))
(hpulse : P.pulses j = PrimaryPulseBounds.canonicalPrimaryPulse f lam u hL U hA p hp hk)
(Y : TorusInverse.Plane)
(i : Fin 3)
:
(nativeUnit P hdet j Y).ofLp i = PartitionedCovariance.covered (SlotColoring.nativeIndex h label.1)
(PartitionedCovariance.nativePulse vr vt
(PartitionedCovariance.slotCenter h (PartitionedCovariance.signedLabel label j)) hdet (P.ci j) sys.radius
fun (z : PartitionedCovariance.Plane) => (PrimaryPulseBounds.localPrimaryProfile f lam u L sys.radius p z).ofLp i)
Y
theorem
NavierStokes.SignedWaveUpdate.masked_signed_square_class
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{H : ℕ → D → Mat2}
{T R : ℕ → D → Vec2}
(h : CovarianceControl s H T)
(B κ : ℝ)
(hR : ∀ (i : Fin 2), WeightedClasses.MeanClass s (B - 1 / 2 - κ) fun (n : ℕ) (x : D) => R n x i)
{mask : ℕ → D → ℝ}
(hm : WeightedClasses.UnweightedClass s 0 mask)
(i : Fin 2)
:
WeightedClasses.MeanClass s (2 * B - 2 * κ) fun (n : ℕ) (x : D) =>
mask n x ^ 2 * (s.epsilon n * SignedCovariance.squareColumn (H n x) (T n x) (R n x) i)
Exported blocks for the correction state #
noncomputable def
NavierStokes.SignedWaveUpdate.signedBlock
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(a : LinearWaveBounds.WaveCoefficients (D × ℝ))
(s : WeightedClasses.StripData (D × ℝ))
(d : LinearWaveBounds.GraphDirections (D × ℝ))
(H : ℕ → D × ℝ → Mat2)
(T R : ℕ → D × ℝ → Vec2)
(mask : ℕ → D × ℝ → ℝ)
(v Ndot : ℕ → D × ℝ → Space)
(A : ℕ → D × ℝ → Space →L[ℝ] Space)
(ψ : ℕ → D × ℝ → ℝ)
(kp : ℕ → ℤ)
(j : Fin 2)
:
Signed block, given by blockOfCoefficients (exactCoefficients a s d H T R mask v Ndot A ψ j) kp.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.SignedWaveUpdate.signedBlock_bounds
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData (D × ℝ)}
{d : LinearWaveBounds.GraphDirections (D × ℝ)}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{P₀ P : ℕ → D × ℝ → ℝ}
{α₀ B κ : ℝ}
(hbase : LinearWaveBounds.InputBounds s P₀ α₀ κ d a)
(hκ : κ ≤ 1 / 2)
{H : ℕ → D × ℝ → Mat2}
{T R : ℕ → D × ℝ → Vec2}
{mask ψ : ℕ → D × ℝ → ℝ}
{v Ndot : ℕ → D × ℝ → Space}
{A : ℕ → D × ℝ → Space →L[ℝ] Space}
(hcov : CovarianceControl s H T)
(hR : ∀ (i : Fin 2), WeightedClasses.MeanClass s (B - 1 / 2 - κ) fun (n : ℕ) (x : D × ℝ) => R n x i)
(hm : WeightedClasses.UnweightedClass s 0 mask)
(hv : WeightedClasses.MemClass s P 0 v)
(hN : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain s) (a.normal s d))
(hNdot : WeightedClasses.UnweightedClass s 0 Ndot)
(hA : WeightedClasses.UnweightedClass s 0 A)
{b M : ℝ}
(hb : 0 < b)
(hlo : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ ‖a.normal s d n x‖)
(hhi : ∀ (n : ℕ), ∀ x ∈ s.domain, ‖a.normal s d n x‖ ≤ M)
(hK : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / a.frequency n)
{radius : D × ℝ → ℝ}
(hradius : a.radius = fun (x : ℕ) => radius)
(hψ : WeightedClasses.UnweightedClass s 0 ψ)
(kp : ℕ → ℤ)
(j : Fin 2)
:
CorrectionState.HarmonicBlock.WaveBounds (sectionStrip s) (fun (n : ℕ) (x : D) => P n (x, 0)) (B - κ)
(signedBlock a s d H T R mask v Ndot A ψ kp j) ∧ CorrectionState.HarmonicBlock.PressureBounds (sectionStrip s) (fun (n : ℕ) (x : D) => P n (x, 0)) (B + 1 / 2 - κ)
(signedBlock a s d H T R mask v Ndot A ψ kp j)
theorem
NavierStokes.SignedWaveUpdate.signedBlock_band
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(a : LinearWaveBounds.WaveCoefficients (D × ℝ))
(s : WeightedClasses.StripData (D × ℝ))
(d : LinearWaveBounds.GraphDirections (D × ℝ))
(H : ℕ → D × ℝ → Mat2)
(T R : ℕ → D × ℝ → Vec2)
(mask : ℕ → D × ℝ → ℝ)
(v Ndot : ℕ → D × ℝ → Space)
(A : ℕ → D × ℝ → Space →L[ℝ] Space)
(ψ : ℕ → D × ℝ → ℝ)
(kp : ℕ → ℤ)
(j : Fin 2)
:
(signedBlock a s d H T R mask v Ndot A ψ kp j).BandLimited 1
noncomputable def
NavierStokes.SignedWaveUpdate.gaussianBlock
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(a : LinearWaveBounds.WaveCoefficients (D × ℝ))
(d : LinearWaveBounds.GraphDirections (D × ℝ))
(ψ : ℕ → D × ℝ → ℝ)
(kp : ℕ → ℤ)
:
Gaussian block, given by ErrorHarmonics.gaussianBlock d ψ a.amplitude 0 1 a.frequency (fun n x => a.phase n (x,0)) kp.
Equations
- NavierStokes.SignedWaveUpdate.gaussianBlock a d ψ kp = NavierStokes.ErrorHarmonics.gaussianBlock d ψ a.amplitude 0 1 a.frequency (fun (n : ℕ) (x : D) => a.phase n (x, 0)) kp
Instances For
theorem
NavierStokes.SignedWaveUpdate.gaussianBlock_represents
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData (D × ℝ)}
{d : LinearWaveBounds.GraphDirections (D × ℝ)}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{H : ℕ → D × ℝ → Mat2}
{T R : ℕ → D × ℝ → Vec2}
{mask : ℕ → D × ℝ → ℝ}
{v Ndot : ℕ → D × ℝ → Space}
{A : ℕ → D × ℝ → Space →L[ℝ] Space}
{ψ : ℕ → D × ℝ → ℝ}
{m : ℕ → ℝ}
(h : AngularInputs s d a H T R mask v Ndot A ψ m)
(hθ : d.angular = (0, 1))
(hψ : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (ψ n))
(kp : ℕ → ℤ)
(hkp : ∀ (n : ℕ), a.frequency n * m n = ↑(kp n))
(j : Fin 2)
:
have z := coefficients a s d H T R mask v Ndot A j;
(gaussianBlock z d ψ kp).oscillation = fun (n : ℕ) (x : D × ℝ) (i : Fin 3) =>
(LinearWaveBounds.excludedSlotError d ψ z.amplitude 0 n x i * HarmonicCalculus.carrier (a.frequency n) (a.phase n) x).re
The error block is evaluated from the actual cutoff derivative and the same uncut signed coefficient. It has the original carrier and its conjugate.
The realization hypothesis below concerns only the already constructed unit pulse and chart. It never identifies or bounds a signed output. The canonical unit pulse and its matrix are identified by the two preceding canonical-pulse theorems.
theorem
NavierStokes.SignedWaveUpdate.signed_tangent_native_realization
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{d : LinearWaveBounds.GraphDirections D}
(a : LinearWaveBounds.WaveCoefficients D)
(H : ℕ → D → Mat2)
(T R : ℕ → D → Vec2)
(mask ψ : ℕ → D → ℝ)
(v Ndot : ℕ → D → Space)
(A : ℕ → D → Space →L[ℝ] Space)
{D₀ h : ℝ}
{vr vt : TorusInverse.Plane}
{sys : PartitionedCovariance.SlotSystem D₀ h vr vt}
{label : PartitionedCovariance.UnsignedLabel}
(P : PartitionedCovariance.PairData sys label)
(hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0)
(outer q : ℝ)
(position : SlotColoring.Position)
(T₀ R₀ : Vec2)
(j : Fin 2)
(n : ℕ)
(x : D)
(Y : TorusInverse.Plane)
(θ : ℝ)
(hH : H n x = P.matrix)
(hT : T n x = T₀)
(hR : R n x = R₀)
(hm : mask n x = PartitionedCovariance.mask D₀ label q position)
(hpulse : ψ n x • v n x = nativeUnit P hdet j Y)
(hphase : a.frequency n * a.phase n x = P.phases j Y + ↑(P.modes j) * θ)
(i : Fin 3)
:
outer * (HarmonicCalculus.vectorMode (a.frequency n) (a.phase n)
(((coefficients a s d H T R mask v Ndot A j).withCutoff ψ).amplitude n) x i).re = (nativeTangentBlock P hdet outer (s.epsilon n) (SignedCovariance.increment P.matrix T₀ R₀) q position j).oscillation 0
(Y, θ) i