LeanPool.NavierStokesAndEuler.NavierStokes.ActualInitialCoherence

theorem NavierStokes.ActualInitialCoherence.sum_eq_mul_sum_of_support {ι : Type} (s t : Finset ι) (f g : ι → ℝ) (a : ℝ) (hf : ∀ i ∉ s, f i = 0) (hg : ∀ i ∉ t, g i = 0) (he : ∀ (i : ι), f i = a * g i) :

∑ i ∈ s, f i = a * ∑ i ∈ t, g i

source

noncomputable def NavierStokes.ActualInitialCoherence.phase {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (n : ℕ) (x : Point) :

ℝ

Phase, given by (pieces B N0 l).coefficients.phase n (x, 0).

Equations

NavierStokes.ActualInitialCoherence.phase l n x = (NavierStokes.ActualInitialCoherence.pieces B N0 l).coefficients.phase n (x, 0)

Instances For

source

noncomputable def NavierStokes.ActualInitialCoherence.angularMode {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (_n : ℕ) :

ℤ

Angular mode, given by PrimaryGeometryAssembly.angularMode certificate modulation (choice B N0).prepared l.2 l.1.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def NavierStokes.ActualInitialCoherence.primaryBlock {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) :

CorrectionState.HarmonicBlock Point

Primary block, given by (pieces B N0 l).harmonicBlock (phase l) (angularMode l).

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def NavierStokes.ActualInitialCoherence.gaussianBlock {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) :

CorrectionState.HarmonicBlock Point

Gaussian block, given by (pieces B N0 l).excludedBlock (phase l) (angularMode l).

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem NavierStokes.ActualInitialCoherence.angularMode_ne {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (n : ℕ) :

angularMode l n ≠ 0

source

theorem NavierStokes.ActualInitialCoherence.phase_split {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (n : ℕ) (x : Point) (θ : ℝ) :

(pieces B N0 l).coefficients.frequency n * (pieces B N0 l).coefficients.phase n (x, θ) = (pieces B N0 l).coefficients.frequency n * phase l n x + ↑(angularMode l n) * θ

source

theorem NavierStokes.ActualInitialCoherence.exact_amplitude_angle {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) :

ErrorHarmonics.AngleIndependent (pieces B N0 l).exactCoefficients.amplitude

source

theorem NavierStokes.ActualInitialCoherence.exact_pressure_angle {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) :

ErrorHarmonics.AngleIndependent (pieces B N0 l).exactCoefficients.pressure

source

theorem NavierStokes.ActualInitialCoherence.primaryBlock_represents {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) :

(primaryBlock l).oscillation = (pieces B N0 l).velocity ∧ (primaryBlock l).oscillatoryPressure = (pieces B N0 l).pressure

source

theorem NavierStokes.ActualInitialCoherence.gaussianBlock_represents {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) :

(gaussianBlock l).oscillation = (pieces B N0 l).excluded

source

theorem NavierStokes.ActualInitialCoherence.block_phase_band {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (x : Point) :

(primaryBlock l).frequency n * (primaryBlock l).phase n x = (primaryBlock l).frequency m * (primaryBlock l).phase m ((GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) x)

Exact carrier equality follows from the actual inverse-cover chart map. Torus periodicity, when needed, uses the separate active-index inequality.

source

theorem NavierStokes.ActualInitialCoherence.seed_velocity_periodic (B N0 n : ℕ) (R : ℝ) (s : Plane) (θ : ℝ) :

FourierAlias.TorusPeriodic fun (Y : TorusInverse.Plane) => (seed B N0).oscillation n ((R, s, Y), θ)

source

theorem NavierStokes.ActualInitialCoherence.covariance_periodic_of_periodic {U : Set Plane} {u : CorrectionState.Oscillation Point} (hu : ∀ (n : ℕ) (θ : ℝ) (i : Fin 3), PhysicalMeanDomain.PeriodicOn U fun (x : PressureStream.Lift Plane) => u n (x, θ) i) (i j : Fin 3) :

MeanStateRegularity.Periodic U (CorrectionState.bilinearCovariance u u i j)

source

theorem NavierStokes.ActualInitialCoherence.seed_covariance_periodic (B N0 : ℕ) (i j : Fin 3) :

MeanStateRegularity.Periodic CorrectionInitialization.ActualPrimary.standardRegion.carrier ((seed B N0).covariance i j)

source

theorem NavierStokes.ActualInitialCoherence.seed_primitive (B N0 : ℕ) :

MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer (CorrectionInitialization.ActualPrimary.commonContext B) (seed B N0)

source

theorem NavierStokes.ActualInitialCoherence.seed_band (B N0 n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) {V : Set Plane} (hsub : V ⊆ CorrectionInitialization.ActualPrimary.standardRegion.carrier) (hmap : Set.MapsTo (⇑(GaugeStateCoherence.bandSlowEquiv CorrectionInitialization.ActualPrimary.h n m)) V CorrectionInitialization.ActualPrimary.standardRegion.carrier) :

PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) (GaugeStateCoherence.bandScale n m) (seed B N0) (seed B N0) n m

source

theorem NavierStokes.ActualInitialCoherence.primary_primitive (B N0 : ℕ) :

MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer (CorrectionInitialization.ActualPrimary.commonContext B) (primary B N0)

source

theorem NavierStokes.ActualInitialCoherence.temporal_primitive (B N0 : ℕ) :

MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer (CorrectionInitialization.ActualPrimary.commonContext B) (temporal B N0)

source

theorem NavierStokes.ActualInitialCoherence.ranked_primitive (B N0 : ℕ) :

MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer (CorrectionInitialization.ActualPrimary.commonContext B) (ranked B N0)

source

theorem NavierStokes.ActualInitialCoherence.initialized_primitive (B N0 : ℕ) :

MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer (CorrectionInitialization.ActualPrimary.commonContext B) (initialized B N0)

source

theorem NavierStokes.ActualInitialCoherence.initialized_aliases (B N0 : ℕ) :

(initialized B N0).errors.aliasError = VariableGaugeMean.temporalAliasState CorrectionInitialization.ActualPrimary.commonGauge CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h) (CorrectionInitialization.ActualPrimary.commonContext B) (primary B N0) + VariableGaugeMean.pressureAliasState CorrectionInitialization.ActualPrimary.commonGauge (CorrectionInitialization.ActualPrimary.commonContext B) (ranked B N0)

The two retained aliases are the actual temporal and reconstructed-pressure aliases.

source

theorem NavierStokes.ActualInitialCoherence.initialized_band (B N0 n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) {V : Set Plane} (hV : IsOpen V) (hsub : V ⊆ CorrectionInitialization.ActualPrimary.standardRegion.carrier) (hmap : Set.MapsTo (⇑(GaugeStateCoherence.bandSlowEquiv CorrectionInitialization.ActualPrimary.h n m)) V CorrectionInitialization.ActualPrimary.standardRegion.carrier) :

PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) (GaugeStateCoherence.bandScale n m) (initialized B N0) (initialized B N0) n m

Full radial, angular, and free auxiliary fibers over every common chart region.

source

noncomputable def NavierStokes.ActualInitialCoherence.overlap (n m : ℕ) :

Set Plane

Overlap, given by standardRegion.carrier ∩ (bandSlowEquiv h n m) ⁻¹' standardRegion.carrier.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem NavierStokes.ActualInitialCoherence.overlap_open (n m : ℕ) :

IsOpen (overlap n m)

source

theorem NavierStokes.ActualInitialCoherence.initialized_on_overlap (B N0 n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) :

PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain (overlap n m)) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) (GaugeStateCoherence.bandScale n m) (initialized B N0) (initialized B N0) n m

source

theorem NavierStokes.ActualInitialCoherence.initialized_alias_band (B N0 n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) {x : Point} (hx : x.2.1 ∈ overlap n m) (θ : ℝ) (i : Fin 3) :

Documentation

LeanPool.NavierStokesAndEuler.NavierStokes.ActualInitialCoherence

Coherence of the literal initialized state #