Actual harmonic residual grouping on a valid open chart #
Closed wave supports need be disjoint only after intersection with the valid chart. At a point in that chart, a nonzero left wave forces the right wave to have a zero germ, so all cross-label transport terms vanish. The resulting grouping retains the independent axisymmetric alias in the actual mean mode.
Grouping the actual residual with an independent axisymmetric alias #
The alias removed from the good residual may contain an arbitrary function of the non-angular variables in addition to the finite harmonic label sums. Subtracting that function changes the angular mean by the same amount and leaves the nonconstant residual unchanged. The needed angular integrability is derived from the represented finite harmonic fields, with no regularity or support assumption on the independent alias.
noncomputable def
NavierStokes.AxisymmetricResidualGrouping.axisymmetricLift
{D : Type}
(a : CorrectionState.MeanVector D)
:
Lift an arbitrary mean vector to a field constant in the angular variable.
Equations
- NavierStokes.AxisymmetricResidualGrouping.axisymmetricLift a n x = a n x.1
Instances For
noncomputable def
NavierStokes.AxisymmetricResidualGrouping.addAxisymmetricAlias
{D : Type}
(s : CorrectionState.State D)
(a : CorrectionState.MeanVector D)
:
Add an independent alias without changing any velocity or pressure field.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.AxisymmetricResidualGrouping.eraseAxisymmetricAlias
{D : Type}
(s : CorrectionState.State D)
(a : CorrectionState.MeanVector D)
:
Remove precisely the specified independent alias from the stored errors.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
NavierStokes.AxisymmetricResidualGrouping.add_eraseAxisymmetricAlias
{D : Type}
(s : CorrectionState.State D)
(a : CorrectionState.MeanVector D)
:
@[simp]
theorem
NavierStokes.AxisymmetricResidualGrouping.erase_addAxisymmetricAlias
{D : Type}
(s : CorrectionState.State D)
(a : CorrectionState.MeanVector D)
:
@[simp]
theorem
NavierStokes.AxisymmetricResidualGrouping.stateFullResidual_addAxisymmetricAlias
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(c : CorrectionState.Context D)
(s : CorrectionState.State D)
(a : CorrectionState.MeanVector D)
:
@[simp]
theorem
NavierStokes.AxisymmetricResidualGrouping.stateFullResidual_eraseAxisymmetricAlias
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(c : CorrectionState.Context D)
(s : CorrectionState.State D)
(a : CorrectionState.MeanVector D)
:
theorem
NavierStokes.AxisymmetricResidualGrouping.stateGoodResidual_addAxisymmetricAlias
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(c : CorrectionState.Context D)
(s : CorrectionState.State D)
(a : CorrectionState.MeanVector D)
(n : ℕ)
(x : D × ℝ)
(i : Fin 3)
:
HarmonicResidual.stateGoodResidual c (addAxisymmetricAlias s a) n x i = HarmonicResidual.stateGoodResidual c s n x i - a n x.1 i
theorem
NavierStokes.AxisymmetricResidualGrouping.stateGoodResidual_eraseAxisymmetricAlias
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(c : CorrectionState.Context D)
(s : CorrectionState.State D)
(a : CorrectionState.MeanVector D)
(n : ℕ)
(x : D × ℝ)
(i : Fin 3)
:
HarmonicResidual.stateGoodResidual c (eraseAxisymmetricAlias s a) n x i = HarmonicResidual.stateGoodResidual c s n x i + a n x.1 i
theorem
NavierStokes.AxisymmetricResidualGrouping.angularAverage_sub_axisymmetric
{D : Type}
(f : CorrectionState.OscillatoryScalar D)
(a : CorrectionState.ScalarField D)
(n : ℕ)
(x : D)
(hf : IntervalIntegrable (fun (θ : ℝ) => f n (x, θ)) MeasureTheory.volume 0 (2 * Real.pi))
:
CorrectionState.angularAverage (fun (m : ℕ) (y : D × ℝ) => f m y - a m y.1) n x = CorrectionState.angularAverage f n x - a n x
Angular integration needs integrability only on this one fiber.
theorem
NavierStokes.AxisymmetricResidualGrouping.stateGoodWaveResidual_addAxisymmetricAlias
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(c : CorrectionState.Context D)
(s : CorrectionState.State D)
(a : CorrectionState.MeanVector D)
(n : ℕ)
(x : D × ℝ)
(i : Fin 3)
(hf :
IntervalIntegrable (fun (θ : ℝ) => HarmonicResidual.stateGoodResidual c s n (x.1, θ) i) MeasureTheory.volume 0
(2 * Real.pi))
:
HarmonicResidual.stateGoodWaveResidual c (addAxisymmetricAlias s a) n x i = HarmonicResidual.stateGoodWaveResidual c s n x i
Adding an arbitrary axisymmetric alias leaves the nonconstant residual unchanged on every angular fiber on which the original residual is integrable.
structure
NavierStokes.AxisymmetricResidualGrouping.Representation
{D : Type}
{ι : Type u_1}
(labels : ℕ → Finset ι)
(blocks : ι → CorrectionState.HarmonicBlock D)
(gaussianCoeffs aliasCoeffs : ι → HarmonicResidual.BlockCoefficients D)
(s : CorrectionState.State D)
(axis : CorrectionState.MeanVector D)
:
The finite label representation keeps the independent zero mode explicit.
- velocity (n : ℕ) (x : D × ℝ) (i : Fin 3) : s.oscillation n x i = ∑ l ∈ labels n, (blocks l).oscillation n x i
- pressure (n : ℕ) (x : D × ℝ) : s.oscillatoryPressure n x = ∑ l ∈ labels n, (blocks l).oscillatoryPressure n x
- gaussian (n : ℕ) (x : D × ℝ) (i : Fin 3) : s.errors.gaussian n x i = ∑ l ∈ labels n, ((HarmonicResidual.ofBlock (blocks l) (gaussianCoeffs l) (aliasCoeffs l) n).gaussianField x i).re
- aliasError (n : ℕ) (x : D × ℝ) (i : Fin 3) : s.errors.aliasError n x i = ∑ l ∈ labels n, ((HarmonicResidual.ofBlock (blocks l) (gaussianCoeffs l) (aliasCoeffs l) n).aliasField x i).re + axis n x.1 i
Instances For
theorem
NavierStokes.AxisymmetricResidualGrouping.Representation.erase
{D : Type}
{ι : Type u_1}
{labels : ℕ → Finset ι}
{blocks : ι → CorrectionState.HarmonicBlock D}
{gaussian aliasCoeffs : ι → HarmonicResidual.BlockCoefficients D}
{s : CorrectionState.State D}
{axis : CorrectionState.MeanVector D}
(h : Representation labels blocks gaussian aliasCoeffs s axis)
:
HarmonicResidual.BlockRepresentation labels blocks gaussian aliasCoeffs (eraseAxisymmetricAlias s axis)
theorem
NavierStokes.AxisymmetricResidualGrouping.extractionRegular_erase
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{ι : Type u_1}
{U : Set D}
{c : CorrectionState.Context D}
{s : CorrectionState.State D}
{labels : ℕ → Finset ι}
{blocks : ι → CorrectionState.HarmonicBlock D}
{gaussian aliasCoeffs : ι → HarmonicResidual.BlockCoefficients D}
{n : ℕ}
(h : HarmonicResidual.ExtractionRegular U c s labels blocks gaussian aliasCoeffs n)
(axis : CorrectionState.MeanVector D)
:
HarmonicResidual.ExtractionRegular U c (eraseAxisymmetricAlias s axis) labels blocks gaussian aliasCoeffs n
@[simp]
theorem
NavierStokes.AxisymmetricResidualGrouping.residualBlock_erase
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(c : CorrectionState.Context D)
(s : CorrectionState.State D)
(axis : CorrectionState.MeanVector D)
(b : CorrectionState.HarmonicBlock D)
(gaussian aliasCoeffs : HarmonicResidual.BlockCoefficients D)
:
HarmonicResidual.residualBlock c (eraseAxisymmetricAlias s axis) b gaussian aliasCoeffs = HarmonicResidual.residualBlock c s b gaussian aliasCoeffs
@[simp]
theorem
NavierStokes.AxisymmetricResidualGrouping.stateMeanCoefficientValue_erase
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{ι : Type u_1}
(labels : ℕ → Finset ι)
(blocks : ι → CorrectionState.HarmonicBlock D)
(gaussian aliasCoeffs : ι → HarmonicResidual.BlockCoefficients D)
(c : CorrectionState.Context D)
(s : CorrectionState.State D)
(axis : CorrectionState.MeanVector D)
:
HarmonicResidual.stateMeanCoefficientValue labels blocks gaussian aliasCoeffs c (eraseAxisymmetricAlias s axis) = HarmonicResidual.stateMeanCoefficientValue labels blocks gaussian aliasCoeffs c s
theorem
NavierStokes.AxisymmetricResidualGrouping.represented_goodResidual_angular_continuous
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{ι : Type u_1}
{U : Set D}
(hU : IsOpen U)
{c : CorrectionState.Context D}
{s : CorrectionState.State D}
{labels : ℕ → Finset ι}
{blocks : ι → CorrectionState.HarmonicBlock D}
{gaussian aliasCoeffs : ι → HarmonicResidual.BlockCoefficients D}
(hrep : HarmonicResidual.BlockRepresentation labels blocks gaussian aliasCoeffs s)
{n : ℕ}
(h : HarmonicResidual.ExtractionRegular U c s labels blocks gaussian aliasCoeffs n)
{x : D}
(hx : x ∈ U)
(i : Fin 3)
:
Continuous fun (θ : ℝ) => HarmonicResidual.stateGoodResidual c s n (x, θ) i
The existing finite harmonic representation implies continuity in the angular variable even when the independent base error is not regular.
theorem
NavierStokes.AxisymmetricResidualGrouping.Representation.goodResidual_angular_continuous
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{ι : Type u_1}
{U : Set D}
(hU : IsOpen U)
{c : CorrectionState.Context D}
{s : CorrectionState.State D}
{labels : ℕ → Finset ι}
{blocks : ι → CorrectionState.HarmonicBlock D}
{gaussian aliasCoeffs : ι → HarmonicResidual.BlockCoefficients D}
{axis : CorrectionState.MeanVector D}
(hrep : Representation labels blocks gaussian aliasCoeffs s axis)
{n : ℕ}
(h : HarmonicResidual.ExtractionRegular U c s labels blocks gaussian aliasCoeffs n)
{x : D}
(hx : x ∈ U)
(i : Fin 3)
:
Continuous fun (θ : ℝ) => HarmonicResidual.stateGoodResidual c s n (x, θ) i
An arbitrary independent alias does not disturb angular continuity.
theorem
NavierStokes.AxisymmetricResidualGrouping.stateGoodWaveResidual_grouped
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{ι : Type u_1}
{U : Set D}
(hU : IsOpen U)
{c : CorrectionState.Context D}
{s : CorrectionState.State D}
{labels : ℕ → Finset ι}
{blocks : ι → CorrectionState.HarmonicBlock D}
{gaussian aliasCoeffs : ι → HarmonicResidual.BlockCoefficients D}
{axis : CorrectionState.MeanVector D}
(hrep : Representation labels blocks gaussian aliasCoeffs s axis)
{n : ℕ}
(h : HarmonicResidual.ExtractionRegular U c s labels blocks gaussian aliasCoeffs n)
{x : D × ℝ}
(hx : x ∈ HarmonicResidual.liftDomain U)
(i : Fin 3)
:
HarmonicResidual.stateGoodWaveResidual c s n x i = ∑ l ∈ labels n, (HarmonicResidual.residualBlock c s (blocks l) (gaussian l) (aliasCoeffs l)).oscillation n x i
Actual nonconstant residual grouping, with no smoothness or support assumption on the independent axisymmetric alias.
theorem
NavierStokes.AxisymmetricResidualGrouping.stateGoodResidual_angularAverage
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{ι : Type u_1}
{U : Set D}
(hU : IsOpen U)
{c : CorrectionState.Context D}
{s : CorrectionState.State D}
{labels : ℕ → Finset ι}
{blocks : ι → CorrectionState.HarmonicBlock D}
{gaussian aliasCoeffs : ι → HarmonicResidual.BlockCoefficients D}
{axis : CorrectionState.MeanVector D}
(hrep : Representation labels blocks gaussian aliasCoeffs s axis)
{n : ℕ}
(h : HarmonicResidual.ExtractionRegular U c s labels blocks gaussian aliasCoeffs n)
{x : D}
(hx : x ∈ U)
(i : Fin 3)
:
CorrectionState.angularAverage (fun (m : ℕ) (y : D × ℝ) => HarmonicResidual.stateGoodResidual c s m y i) n x = HarmonicResidual.stateMeanCoefficientValue labels blocks gaussian aliasCoeffs c s n x i - axis n x i
The independent alias changes the actual zero mode by its negative.
theorem
NavierStokes.AxisymmetricResidualGrouping.stateFullResidual_reconstructed
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{ι : Type u_1}
{U : Set D}
(hU : IsOpen U)
{c : CorrectionState.Context D}
{s : CorrectionState.State D}
{labels : ℕ → Finset ι}
{blocks : ι → CorrectionState.HarmonicBlock D}
{gaussian aliasCoeffs : ι → HarmonicResidual.BlockCoefficients D}
{axis : CorrectionState.MeanVector D}
(hrep : Representation labels blocks gaussian aliasCoeffs s axis)
{n : ℕ}
(h : HarmonicResidual.ExtractionRegular U c s labels blocks gaussian aliasCoeffs n)
{x : D × ℝ}
(hx : x ∈ HarmonicResidual.liftDomain U)
(i : Fin 3)
:
HarmonicResidual.stateFullResidual c s n x i = ∑ l ∈ labels n, (HarmonicResidual.residualBlock c s (blocks l) (gaussian l) (aliasCoeffs l)).oscillation n x i + (HarmonicResidual.stateMeanCoefficientValue labels blocks gaussian aliasCoeffs c s n x.1 i - axis n x.1 i) + s.errors.total n x i
The complete residual retains the actual excluded errors and the corrected mean mode. In particular the independent alias is never silently discarded.
theorem
NavierStokes.LocalResidualGrouping.zero_germ_of_disjoint_on
{D : Type}
[NormedAddCommGroup D]
{U : Set D}
{u v : D → HarmonicCalculus.ComplexVector}
(hd : Disjoint (U ∩ tsupport u) (U ∩ tsupport v))
{x : D}
(hx : x ∈ U)
(hu : u x ≠ 0)
:
A local separation of closed supports gives an actual zero germ of the right field whenever the left field is nonzero at the point.
theorem
NavierStokes.LocalResidualGrouping.transport_zero_of_disjoint_on
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(R : D → ℝ)
(Vr Vθ Vz : D → D)
{U : Set D}
{u v : D → HarmonicCalculus.ComplexVector}
(hd : Disjoint (U ∩ tsupport u) (U ∩ tsupport v))
{x : D}
(hx : x ∈ U)
:
theorem
NavierStokes.LocalResidualGrouping.transport_sum_self
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{ι : Type u_1}
(s : Finset ι)
(R : D → ℝ)
(Vr Vθ Vz : D → D)
(u : ι → D → HarmonicCalculus.ComplexVector)
{U : Set D}
{x : D}
(hu : ∀ l ∈ s, ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => u l y i) x)
(hdisj : ∀ l ∈ s, ∀ j ∈ s, l ≠ j → Disjoint (U ∩ tsupport (u l)) (U ∩ tsupport (u j)))
(hx : x ∈ U)
:
LinearWaveResidual.transport R Vr Vθ Vz (∑ l ∈ s, u l) (∑ l ∈ s, u l) x = ∑ l ∈ s, LinearWaveResidual.transport R Vr Vθ Vz (u l) (u l) x
theorem
NavierStokes.LocalResidualGrouping.nonlinearResidual_sum
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{ι : Type u_1}
(s : Finset ι)
{U : Set D}
(hU : IsOpen U)
(ε : ℝ)
(R : D → ℝ)
{Vr Vθ Vz : D → D}
(Vt : D → D)
(hr : ContDiffOn ℝ (↑⊤) Vr U)
(hθ : ContDiffOn ℝ (↑⊤) Vθ U)
(hz : ContDiffOn ℝ (↑⊤) Vz U)
(B : D → HarmonicCalculus.ComplexVector)
(u : ι → D → HarmonicCalculus.ComplexVector)
(p : ι → D → ℂ)
(hu : ∀ l ∈ s, ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => u l y i) U)
(hp : ∀ l ∈ s, ContDiffOn ℝ (↑⊤) (p l) U)
(hdisj : ∀ l ∈ s, ∀ j ∈ s, l ≠ j → Disjoint (U ∩ tsupport (u l)) (U ∩ tsupport (u j)))
{x : D}
(hx : x ∈ U)
:
HarmonicResidual.Actual.nonlinearResidual ε R Vr Vθ Vz Vt B (∑ l ∈ s, u l) (∑ l ∈ s, p l) x = ∑ l ∈ s, HarmonicResidual.Actual.nonlinearResidual ε R Vr Vθ Vz Vt B (u l) (p l) x
Only the nonlinear transport uses separation; all remaining terms use the already proved linear finite-sum identity on the open chart.
theorem
NavierStokes.LocalResidualGrouping.goodResidual_grouped
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{ι : Type u_1}
(labels : Finset ι)
(data : ι → HarmonicResidual.LabelData D)
{U : Set D}
(hU : IsOpen U)
{g : HarmonicResidual.Frame D}
(hg : g.Regular U)
(B M : D → HarmonicCalculus.ComplexVector)
(p : D → ℂ)
(virtual : D → Fin 3 → ℝ)
(hB : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => B y i) U)
(hM : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => M y i) U)
(hp : ContDiffOn ℝ (↑⊤) p U)
(hd : ∀ l ∈ labels, (data l).Regular U)
(hdisj :
∀ l ∈ labels,
∀ j ∈ labels,
l ≠ j →
Disjoint (HarmonicResidual.liftDomain U ∩ tsupport (data l).wave)
(HarmonicResidual.liftDomain U ∩ tsupport (data j).wave))
{x : D × ℝ}
(hx : x ∈ HarmonicResidual.liftDomain U)
(i : Fin 3)
:
HarmonicResidual.goodResidual labels data g B M p virtual x i = ((HarmonicResidual.meanCoefficients g B M p i).coeff 0 x.1).re + virtual x.1 i + ∑ l ∈ labels,
(HarmonicFields.field ((data l).residualCoefficients g B M i) (data l).frequency (data l).phase
(data l).angularFrequency x).re
The coefficient formula is unchanged; the actual wave supports are separated only inside the lifted valid domain.
theorem
NavierStokes.LocalResidualGrouping.goodResidual_angularMean
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{ι : Type u_1}
(labels : Finset ι)
(data : ι → HarmonicResidual.LabelData D)
{U : Set D}
(hU : IsOpen U)
{g : HarmonicResidual.Frame D}
(hg : g.Regular U)
(B M : D → HarmonicCalculus.ComplexVector)
(p : D → ℂ)
(virtual : D → Fin 3 → ℝ)
(hB : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => B y i) U)
(hM : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => M y i) U)
(hp : ContDiffOn ℝ (↑⊤) p U)
(hd : ∀ l ∈ labels, (data l).Regular U)
(hdisj :
∀ l ∈ labels,
∀ j ∈ labels,
l ≠ j →
Disjoint (HarmonicResidual.liftDomain U ∩ tsupport (data l).wave)
(HarmonicResidual.liftDomain U ∩ tsupport (data j).wave))
(hkp : ∀ l ∈ labels, (data l).angularFrequency ≠ 0)
{x : D}
(hx : x ∈ U)
(i : Fin 3)
:
(HarmonicResidual.realAngularMean fun (θ : ℝ) => HarmonicResidual.goodResidual labels data g B M p virtual (x, θ) i) = HarmonicResidual.meanResidualValue labels data g B M p virtual x i
theorem
NavierStokes.LocalResidualGrouping.goodWaveResidual_grouped
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{ι : Type u_1}
(labels : Finset ι)
(data : ι → HarmonicResidual.LabelData D)
{U : Set D}
(hU : IsOpen U)
{g : HarmonicResidual.Frame D}
(hg : g.Regular U)
(B M : D → HarmonicCalculus.ComplexVector)
(p : D → ℂ)
(virtual : D → Fin 3 → ℝ)
(hB : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => B y i) U)
(hM : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D) => M y i) U)
(hp : ContDiffOn ℝ (↑⊤) p U)
(hd : ∀ l ∈ labels, (data l).Regular U)
(hdisj :
∀ l ∈ labels,
∀ j ∈ labels,
l ≠ j →
Disjoint (HarmonicResidual.liftDomain U ∩ tsupport (data l).wave)
(HarmonicResidual.liftDomain U ∩ tsupport (data j).wave))
(hkp : ∀ l ∈ labels, (data l).angularFrequency ≠ 0)
{x : D × ℝ}
(hx : x ∈ HarmonicResidual.liftDomain U)
(i : Fin 3)
:
HarmonicResidual.goodWaveResidual labels data g B M p virtual x i = ∑ l ∈ labels,
(HarmonicFields.field ((data l).waveResidualCoefficients g B M i) (data l).frequency (data l).phase
(data l).angularFrequency x).re
structure
NavierStokes.LocalResidualGrouping.ExtractionRegular
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{ι : Type u_1}
(U : Set D)
(c : CorrectionState.Context D)
(s : CorrectionState.State D)
(labels : ℕ → Finset ι)
(blockFamily : ι → CorrectionState.HarmonicBlock D)
(gaussianCoeffs aliasCoeffs : ι → HarmonicResidual.BlockCoefficients D)
(n : ℕ)
:
The regularity needed for actual extraction, with separation only inside the valid lifted open domain.
- frame : (HarmonicResidual.contextFrame c n).Regular U
- base (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (x : D) => HarmonicResidual.contextBase c n x i) U
- mean (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (x : D) => HarmonicResidual.stateMean s n x i) U
- pressure : ContDiffOn ℝ (↑⊤) (s.pressure n) U
- blocks (l : ι) : l ∈ labels n → (HarmonicResidual.ofBlock (blockFamily l) (gaussianCoeffs l) (aliasCoeffs l) n).Regular U
- gaussian (l : ι) : l ∈ labels n → ∀ (i : Fin 3), HarmonicResidual.SmoothCoefficients U (gaussianCoeffs l n i)
- aliasError (l : ι) : l ∈ labels n → ∀ (i : Fin 3), HarmonicResidual.SmoothCoefficients U (aliasCoeffs l n i)
- disjoint (l : ι) : l ∈ labels n → ∀ j ∈ labels n, l ≠ j → Disjoint (HarmonicResidual.liftDomain U ∩ tsupport ((blockFamily l).oscillation n)) (HarmonicResidual.liftDomain U ∩ tsupport ((blockFamily j).oscillation n))
- angular_nonzero (l : ι) : l ∈ labels n → (blockFamily l).angularFrequency n ≠ 0
Instances For
theorem
NavierStokes.LocalResidualGrouping.ExtractionRegular.dataDisjoint
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{ι : Type u_1}
{U : Set D}
{c : CorrectionState.Context D}
{s : CorrectionState.State D}
{labels : ℕ → Finset ι}
{blocks : ι → CorrectionState.HarmonicBlock D}
{gaussian aliasCoeffs : ι → HarmonicResidual.BlockCoefficients D}
{n : ℕ}
(h : ExtractionRegular U c s labels blocks gaussian aliasCoeffs n)
(l : ι)
:
l ∈ labels n →
∀ j ∈ labels n,
l ≠ j →
Disjoint
(HarmonicResidual.liftDomain U ∩ tsupport (HarmonicResidual.ofBlock (blocks l) (gaussian l) (aliasCoeffs l) n).wave)
(HarmonicResidual.liftDomain U ∩ tsupport (HarmonicResidual.ofBlock (blocks j) (gaussian j) (aliasCoeffs j) n).wave)
theorem
NavierStokes.LocalResidualGrouping.ExtractionRegular.erase
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{ι : Type u_1}
{U : Set D}
{c : CorrectionState.Context D}
{s : CorrectionState.State D}
{labels : ℕ → Finset ι}
{blocks : ι → CorrectionState.HarmonicBlock D}
{gaussian aliasCoeffs : ι → HarmonicResidual.BlockCoefficients D}
{n : ℕ}
(h : ExtractionRegular U c s labels blocks gaussian aliasCoeffs n)
(axis : CorrectionState.MeanVector D)
:
ExtractionRegular U c (AxisymmetricResidualGrouping.eraseAxisymmetricAlias s axis) labels blocks gaussian aliasCoeffs n
theorem
NavierStokes.LocalResidualGrouping.represented_goodResidual_angular_continuous
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{ι : Type u_1}
{U : Set D}
(hU : IsOpen U)
{c : CorrectionState.Context D}
{s : CorrectionState.State D}
{labels : ℕ → Finset ι}
{blocks : ι → CorrectionState.HarmonicBlock D}
{gaussian aliasCoeffs : ι → HarmonicResidual.BlockCoefficients D}
(hrep : HarmonicResidual.BlockRepresentation labels blocks gaussian aliasCoeffs s)
{n : ℕ}
(h : ExtractionRegular U c s labels blocks gaussian aliasCoeffs n)
{x : D}
(hx : x ∈ U)
(i : Fin 3)
:
Continuous fun (θ : ℝ) => HarmonicResidual.stateGoodResidual c s n (x, θ) i
theorem
NavierStokes.LocalResidualGrouping.stateGoodWaveResidual_grouped_of_blockRepresentation
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{ι : Type u_1}
{U : Set D}
(hU : IsOpen U)
{c : CorrectionState.Context D}
{s : CorrectionState.State D}
{labels : ℕ → Finset ι}
{blocks : ι → CorrectionState.HarmonicBlock D}
{gaussian aliasCoeffs : ι → HarmonicResidual.BlockCoefficients D}
(hrep : HarmonicResidual.BlockRepresentation labels blocks gaussian aliasCoeffs s)
{n : ℕ}
(h : ExtractionRegular U c s labels blocks gaussian aliasCoeffs n)
{x : D × ℝ}
(hx : x ∈ HarmonicResidual.liftDomain U)
(i : Fin 3)
:
HarmonicResidual.stateGoodWaveResidual c s n x i = ∑ l ∈ labels n, (HarmonicResidual.residualBlock c s (blocks l) (gaussian l) (aliasCoeffs l)).oscillation n x i
theorem
NavierStokes.LocalResidualGrouping.stateMeanCoefficientValue_eq_average
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{ι : Type u_1}
{U : Set D}
(hU : IsOpen U)
{c : CorrectionState.Context D}
{s : CorrectionState.State D}
{labels : ℕ → Finset ι}
{blocks : ι → CorrectionState.HarmonicBlock D}
{gaussian aliasCoeffs : ι → HarmonicResidual.BlockCoefficients D}
(hrep : HarmonicResidual.BlockRepresentation labels blocks gaussian aliasCoeffs s)
{n : ℕ}
(h : ExtractionRegular U c s labels blocks gaussian aliasCoeffs n)
{x : D}
(hx : x ∈ U)
(i : Fin 3)
:
HarmonicResidual.stateMeanCoefficientValue labels blocks gaussian aliasCoeffs c s n x i = CorrectionState.angularAverage (fun (m : ℕ) (y : D × ℝ) => HarmonicResidual.stateGoodResidual c s m y i) n x
theorem
NavierStokes.LocalResidualGrouping.stateGoodWaveResidual_grouped
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{ι : Type u_1}
{U : Set D}
(hU : IsOpen U)
{c : CorrectionState.Context D}
{s : CorrectionState.State D}
{labels : ℕ → Finset ι}
{blocks : ι → CorrectionState.HarmonicBlock D}
{gaussian aliasCoeffs : ι → HarmonicResidual.BlockCoefficients D}
{axis : CorrectionState.MeanVector D}
(hrep : AxisymmetricResidualGrouping.Representation labels blocks gaussian aliasCoeffs s axis)
{n : ℕ}
(h : ExtractionRegular U c s labels blocks gaussian aliasCoeffs n)
{x : D × ℝ}
(hx : x ∈ HarmonicResidual.liftDomain U)
(i : Fin 3)
:
HarmonicResidual.stateGoodWaveResidual c s n x i = ∑ l ∈ labels n, (HarmonicResidual.residualBlock c s (blocks l) (gaussian l) (aliasCoeffs l)).oscillation n x i
Actual nonconstant grouping with local support separation and an arbitrary independent axisymmetric alias.
theorem
NavierStokes.LocalResidualGrouping.stateGoodResidual_angularAverage
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{ι : Type u_1}
{U : Set D}
(hU : IsOpen U)
{c : CorrectionState.Context D}
{s : CorrectionState.State D}
{labels : ℕ → Finset ι}
{blocks : ι → CorrectionState.HarmonicBlock D}
{gaussian aliasCoeffs : ι → HarmonicResidual.BlockCoefficients D}
{axis : CorrectionState.MeanVector D}
(hrep : AxisymmetricResidualGrouping.Representation labels blocks gaussian aliasCoeffs s axis)
{n : ℕ}
(h : ExtractionRegular U c s labels blocks gaussian aliasCoeffs n)
{x : D}
(hx : x ∈ U)
(i : Fin 3)
:
CorrectionState.angularAverage (fun (m : ℕ) (y : D × ℝ) => HarmonicResidual.stateGoodResidual c s m y i) n x = HarmonicResidual.stateMeanCoefficientValue labels blocks gaussian aliasCoeffs c s n x i - axis n x i
theorem
NavierStokes.LocalResidualGrouping.stateFullResidual_reconstructed
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{ι : Type u_1}
{U : Set D}
(hU : IsOpen U)
{c : CorrectionState.Context D}
{s : CorrectionState.State D}
{labels : ℕ → Finset ι}
{blocks : ι → CorrectionState.HarmonicBlock D}
{gaussian aliasCoeffs : ι → HarmonicResidual.BlockCoefficients D}
{axis : CorrectionState.MeanVector D}
(hrep : AxisymmetricResidualGrouping.Representation labels blocks gaussian aliasCoeffs s axis)
{n : ℕ}
(h : ExtractionRegular U c s labels blocks gaussian aliasCoeffs n)
{x : D × ℝ}
(hx : x ∈ HarmonicResidual.liftDomain U)
(i : Fin 3)
:
HarmonicResidual.stateFullResidual c s n x i = ∑ l ∈ labels n, (HarmonicResidual.residualBlock c s (blocks l) (gaussian l) (aliasCoeffs l)).oscillation n x i + (HarmonicResidual.stateMeanCoefficientValue labels blocks gaussian aliasCoeffs c s n x.1 i - axis n x.1 i) + s.errors.total n x i