Documentation

LeanPool.NavierStokesAndEuler.NavierStokes.ActualInitialMeanEquation

The actual initialized mean equation and incompressibility #

This module works with the literal initialized state before the final initialization consumer. No MeanHypotheses or divergence statement is an input.

@[reducible, inline]

abbrev NavierStokes.ActualInitialMeanEquation.Point :

Point: an abbreviation for PressureStream.Lift PressureStream.Plane.

Equations

NavierStokes.ActualInitialMeanEquation.Point = NavierStokes.PressureStream.Lift NavierStokes.PressureStream.Plane

Instances For

@[reducible, inline]

abbrev NavierStokes.ActualInitialMeanEquation.Full :

Full: an abbreviation for Point × ℝ.

Equations

NavierStokes.ActualInitialMeanEquation.Full = (NavierStokes.ActualInitialMeanEquation.Point × ℝ)

Instances For

noncomputable def NavierStokes.ActualInitialMeanEquation.strip :

WeightedClasses.StripData Point

Strip, given by BaseContextAssembly.nativeStrip nominal standardRegion.

Equations

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

Instances For

theorem NavierStokes.ActualInitialMeanEquation.strip_to_slow {x : Point} (hx : x ∈ strip.domain) :

x ∈ PhysicalMeanDomain.slowDomain CorrectionInitialization.ActualPrimary.standardRegion.carrier

theorem NavierStokes.ActualInitialMeanEquation.strip_radius {x : Point} (hx : x ∈ strip.domain) :

0 < x.1

theorem NavierStokes.ActualInitialMeanEquation.strip_time {x : Point} (hx : x ∈ strip.domain) :

0 < x.2.1.1

A reusable local mean-equation interface #

structure NavierStokes.ActualInitialMeanEquation.AngularData (V : Set Point) (u : CorrectionState.State Point) :

Angular regularity of the actual fields. The mean coefficients and their pressure are supplied separately by the primitive invariant.

velocity_smooth (n : ℕ) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (p : Point × ℝ) => u.oscillation n p i) (LiftedMeanResidual.cylinder V)
pressure_smooth (n : ℕ) : ContDiffOn ℝ (↑⊤) (u.oscillatoryPressure n) (LiftedMeanResidual.cylinder V)
velocity_periodic (n : ℕ) (i : Fin 3) : LiftedMeanResidual.PeriodicOn V fun (p : Point × ℝ) => u.oscillation n p i
pressure_periodic (n : ℕ) : LiftedMeanResidual.PeriodicOn V (u.oscillatoryPressure n)
velocity_mean_zero (n : ℕ) (x : Point) : x ∈ V → ∀ (i : Fin 3), CorrectionState.angularAverage (fun (k : ℕ) (p : Point × ℝ) => u.oscillation k p i) n x = 0
pressure_mean_zero (n : ℕ) (x : Point) : x ∈ V → CorrectionState.angularAverage u.oscillatoryPressure n x = 0
base_error_continuous (n : ℕ) (x : Point) : x ∈ V → ∀ (i : Fin 3), Continuous fun (θ : ℝ) => u.errors.base n (x, θ) i
excluded_continuous (n : ℕ) (x : Point) : x ∈ V → ∀ (i : Fin 3), Continuous fun (θ : ℝ) => u.errors.total n (x, θ) i

Instances For

theorem NavierStokes.ActualInitialMeanEquation.totalVelocity_smooth_of_primitive {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {c : CorrectionState.Context Point} {u : CorrectionState.State Point} (HP : MeanStateRegularity.PrimitiveData U a b c u) {V : Set Point} (hsub : V ⊆ LocalRankDefect.positiveDomain U.carrier) (hw : ∀ (n : ℕ) (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (p : Point × ℝ) => u.oscillation n p i) (LiftedMeanResidual.cylinder V)) (n : ℕ) (i : Fin 3) :

ContDiffOn ℝ (↑⊤) (fun (p : Point × ℝ) => u.totalVelocity c n p i) (LiftedMeanResidual.cylinder V)

theorem NavierStokes.ActualInitialMeanEquation.meanHypotheses_of_primitive {coord : ℝ} {U : LocalSignedRequest.SlowRegion coord} {g : VariableGaugeMean.GaugeData PressureStream.Plane} {c : CorrectionState.Context Point} {u : CorrectionState.State Point} (HP : MeanStateRegularity.PrimitiveData U g.radial.inner g.radial.outer c u) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (hfixed : (VariableGaugeMean.reconstructState g c u).pressure = u.pressure) {V : Set Point} (hV : IsOpen V) (hsub : V ⊆ LocalRankDefect.positiveDomain U.carrier) (HA : AngularData V u) (hbase : ∀ (n : ℕ), ∀ p ∈ LiftedMeanResidual.cylinder V, LiftedMeanResidual.realDivergence (LiftedMeanResidual.liftScalar c.operators.radius) (LiftedMeanResidual.radialDirection c n) LiftedMeanResidual.angularDirection (LiftedMeanResidual.axialDirection c n) (LiftedMeanResidual.baseLift c n) p = 0) (hdiv : ∀ (n : ℕ), ∀ p ∈ LiftedMeanResidual.cylinder V, CorrectionStep.fullDivergence c u n p = 0) :

LiftedMeanResidual.MeanHypotheses V c u

theorem NavierStokes.ActualInitialMeanEquation.temporalIncrement_meanDivergence_zero_local {coord : ℝ} {U : LocalSignedRequest.SlowRegion coord} {g : VariableGaugeMean.GaugeData PressureStream.Plane} {c : CorrectionState.Context Point} {u : CorrectionState.State Point} (HP : MeanStateRegularity.PrimitiveData U g.radial.inner g.radial.outer c u) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (hfixed : (VariableGaugeMean.reconstructState g c u).pressure = u.pressure) (htime : ℝ) (index : ℕ → ℕ) (axial slowTime : PressureStream.Plane × PressureStream.Plane) (temporal : PressureStream.Plane) (hcompat : c.operators = CorrectionState.graphOperators g.radial c.operators.epsilon c.operators.fastCoefficient axial slowTime temporal) (n : ℕ) {x : Point} (hx : x.2.1 ∈ U.carrier) (hr : x.1 ≠ 0) :

CorrectionStep.meanDivergence c (VariableGaugeMean.temporalIncrementState g htime index axial c u) n x = 0

theorem NavierStokes.ActualInitialMeanEquation.rankIncrement_meanDivergence_zero_local {coord : ℝ} {U : LocalSignedRequest.SlowRegion coord} {g : VariableGaugeMean.GaugeData PressureStream.Plane} {c : CorrectionState.Context Point} {u : CorrectionState.State Point} {r : CorrectionState.RankData PressureStream.Plane} (hg : LocalRankDefect.RankGeometry g r U.carrier c u) (hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (axial slowTime : PressureStream.Plane × PressureStream.Plane) (temporal : PressureStream.Plane) (hcompat : c.operators = CorrectionState.graphOperators g.radial c.operators.epsilon c.operators.fastCoefficient axial slowTime temporal) (n : ℕ) {x : Point} (hx : x.2.1 ∈ U.carrier) (hr : x.1 ≠ 0) :

CorrectionStep.meanDivergence c (VariableGaugeMean.rankIncrementState g r axial c u) n x = 0

theorem NavierStokes.ActualInitialMeanEquation.temporalStage_fullDivergence_local {coord : ℝ} {U : LocalSignedRequest.SlowRegion coord} {g : VariableGaugeMean.GaugeData PressureStream.Plane} {c : CorrectionState.Context Point} {u : CorrectionState.State Point} (HP : MeanStateRegularity.PrimitiveData U g.radial.inner g.radial.outer c u) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (hfixed : (VariableGaugeMean.reconstructState g c u).pressure = u.pressure) (htime : ℝ) (index : ℕ → ℕ) (axial slowTime : PressureStream.Plane × PressureStream.Plane) (temporal : PressureStream.Plane) (hcompat : c.operators = CorrectionState.graphOperators g.radial c.operators.epsilon c.operators.fastCoefficient axial slowTime temporal) (n : ℕ) {x : Point} (hx : x.2.1 ∈ U.carrier) (hr : x.1 ≠ 0) (θ : ℝ) (hu : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : Point × ℝ) => u.totalVelocity c n y i) (x, θ)) :

CorrectionStep.fullDivergence c (VariableGaugeMean.temporalStageState g htime index axial c u) n (x, θ) = CorrectionStep.fullDivergence c u n (x, θ)

theorem NavierStokes.ActualInitialMeanEquation.rankStage_fullDivergence_local {coord : ℝ} {U : LocalSignedRequest.SlowRegion coord} {g : VariableGaugeMean.GaugeData PressureStream.Plane} {c : CorrectionState.Context Point} {u : CorrectionState.State Point} {r : CorrectionState.RankData PressureStream.Plane} (hg : LocalRankDefect.RankGeometry g r U.carrier c u) (hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (axial slowTime : PressureStream.Plane × PressureStream.Plane) (temporal : PressureStream.Plane) (hcompat : c.operators = CorrectionState.graphOperators g.radial c.operators.epsilon c.operators.fastCoefficient axial slowTime temporal) (n : ℕ) {x : Point} (hx : x.2.1 ∈ U.carrier) (hr : x.1 ≠ 0) (θ : ℝ) (hu : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : Point × ℝ) => u.totalVelocity c n y i) (x, θ)) :

CorrectionStep.fullDivergence c (VariableGaugeMean.rankStageState g r axial c u) n (x, θ) = CorrectionStep.fullDivergence c u n (x, θ)

First derivatives of the actual physical base #

noncomputable def NavierStokes.ActualInitialMeanEquation.componentDivergence {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vθ Vz : E → E) (a : E → Fin 3 → ℝ) (x : E) :

Component divergence, given by along Vr (fun y => a y 0) x + a x 0 / R x + along Vθ (fun y => a y 1) x / R x + along Vz (fun y => a y 2) x.

Equations

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

Instances For

theorem NavierStokes.ActualInitialMeanEquation.componentDivergence_of_complex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vθ Vz : E → E) {a : E → Fin 3 → ℝ} {x : E} (ha : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : E) => a y i) x) (hz : HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz (fun (y : E) (i : Fin 3) => ↑(a y i)) x = 0) :

componentDivergence R Vr Vθ Vz a x = 0

theorem NavierStokes.ActualInitialMeanEquation.componentDivergence_sum {E ι : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (J : Finset ι) (R : E → ℝ) (Vr Vθ Vz : E → E) {a : ι → E → Fin 3 → ℝ} {x : E} (ha : ∀ j ∈ J, ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : E) => a j y i) x) :

componentDivergence R Vr Vθ Vz (fun (y : E) (i : Fin 3) => ∑ j ∈ J, a j y i) x = ∑ j ∈ J, componentDivergence R Vr Vθ Vz (a j) x

theorem NavierStokes.ActualInitialMeanEquation.componentDivergence_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (hU : IsOpen U) (R : E → ℝ) (Vr Vθ Vz : E → E) {a b : E → Fin 3 → ℝ} (he : Set.EqOn a b U) {x : E} (hx : x ∈ U) :

componentDivergence R Vr Vθ Vz a x = componentDivergence R Vr Vθ Vz b x

theorem NavierStokes.ActualInitialMeanEquation.componentDivergence_pullback {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : Set E} {U : Set F} {Γ : E → F} {l v : ℝ} {R : F → ℝ} {Vr Vθ Vz Vt : F → F} {Sr Sθ Sz St : E → E} {r : E → ℝ} (G : PhysicalResidualBridge.PullbackData Ω U Γ l v R Vr Vθ Vz Vt Sr Sθ Sz St r) (hl : l ≠ 0) {a : F → Fin 3 → ℝ} (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : F) => a y i) U) {x : E} (hx : x ∈ Ω) (hr : r x ≠ 0) :

componentDivergence r Sr Sθ Sz (fun (y : E) (i : Fin 3) => v * a (Γ y) i) x = v * l * componentDivergence R Vr Vθ Vz a (Γ x)

theorem NavierStokes.ActualInitialMeanEquation.coordinate_divergence_eq {a : ProblemStatement.SpaceTime → ProblemStatement.Space} {t : ℝ} {q : ProblemStatement.Space} (ha : DifferentiableAt ℝ a (t, q)) :

componentDivergence LinearWaveResidual.coordinateRadius (LinearWaveResidual.spaceDirection 0) (LinearWaveResidual.spaceDirection 1) (LinearWaveResidual.spaceDirection 2) (fun (z : ProblemStatement.SpaceTime) (i : Fin 3) => (a z).ofLp i) (t, q) = CylindricalResidual.vectorDivergence (fun (y : ProblemStatement.Space) => a (t, y)) q

theorem NavierStokes.ActualInitialMeanEquation.radialDirection_match {c : CorrectionState.Context Point} {G : PhysicalResidualBridge.ScaledGraph} {n : ℕ} (H : PhysicalResidualTZ.MatchesAtTZ c.operators G n) :

LiftedMeanResidual.radialDirection c n = PhysicalResidualTZ.graphRadialTZ G

theorem NavierStokes.ActualInitialMeanEquation.axialDirection_match {c : CorrectionState.Context Point} {G : PhysicalResidualBridge.ScaledGraph} {n : ℕ} (H : PhysicalResidualTZ.MatchesAtTZ c.operators G n) :

LiftedMeanResidual.axialDirection c n = PhysicalResidualTZ.graphAxialTZ G

theorem NavierStokes.ActualInitialMeanEquation.scaled_base_divergence (B n : ℕ) {x : Full} (hx : x ∈ ActualBaseResidual.domain) :

The actual primary sum is divergence free #

theorem NavierStokes.ActualInitialMeanEquation.strip_to_positive {x : Point} (hx : x ∈ strip.domain) :

x ∈ LocalRankDefect.positiveDomain CorrectionInitialization.ActualPrimary.standardRegion.carrier

theorem NavierStokes.ActualInitialMeanEquation.piece_divergence {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (n : ℕ) {x : Full} (hx : x ∈ ActualPrimaryCoherence.positiveRadialChart) :

componentDivergence (fun (y : Full) => y.1.1) (LiftedMeanResidual.radialDirection (CorrectionInitialization.ActualPrimary.commonContext B) n) LiftedMeanResidual.angularDirection (LiftedMeanResidual.axialDirection (CorrectionInitialization.ActualPrimary.commonContext B) n) ((ActualInitialCoherence.pieces B N0 l).velocity n) x = 0

theorem NavierStokes.ActualInitialMeanEquation.primary_oscillation (B N0 : ℕ) :

(ActualInitialCoherence.primary B N0).oscillation = (ActualInitialCoherence.seed B N0).oscillation

theorem NavierStokes.ActualInitialMeanEquation.temporal_oscillation (B N0 : ℕ) :

(ActualInitialCoherence.temporal B N0).oscillation = (ActualInitialCoherence.seed B N0).oscillation

theorem NavierStokes.ActualInitialMeanEquation.initialized_oscillation (B N0 : ℕ) :

(ActualInitialCoherence.initialized B N0).oscillation = (ActualInitialCoherence.seed B N0).oscillation

theorem NavierStokes.ActualInitialMeanEquation.primary_fullDivergence (B N0 n : ℕ) {x : Full} (hx : x ∈ LiftedMeanResidual.cylinder strip.domain) :

CorrectionStep.fullDivergence (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialCoherence.primary B N0) n x = 0

theorem NavierStokes.ActualInitialMeanEquation.initialized_fullDivergence (B N0 n : ℕ) {x : Full} (hx : x ∈ LiftedMeanResidual.cylinder strip.domain) :

CorrectionStep.fullDivergence (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialCoherence.initialized B N0) n x = 0

Literal angular harmonics and the retained errors #

theorem NavierStokes.ActualInitialMeanEquation.piece_velocity_angularContinuous {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (n : ℕ) (x : Point) (i : Fin 3) :

Continuous fun (θ : ℝ) => (ActualInitialCoherence.pieces B N0 l).velocity n (x, θ) i

theorem NavierStokes.ActualInitialMeanEquation.piece_pressure_angularContinuous {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (n : ℕ) (x : Point) :

Continuous fun (θ : ℝ) => (ActualInitialCoherence.pieces B N0 l).pressure n (x, θ)

theorem NavierStokes.ActualInitialMeanEquation.piece_excluded_angularContinuous {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (n : ℕ) (x : Point) (i : Fin 3) :

Continuous fun (θ : ℝ) => (ActualInitialCoherence.pieces B N0 l).excluded n (x, θ) i

theorem NavierStokes.ActualInitialMeanEquation.piece_velocity_angularPeriodic {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (n : ℕ) (x : Point) (i : Fin 3) :

Function.Periodic (fun (θ : ℝ) => (ActualInitialCoherence.pieces B N0 l).velocity n (x, θ) i) (2 * Real.pi)

theorem NavierStokes.ActualInitialMeanEquation.piece_pressure_angularPeriodic {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (n : ℕ) (x : Point) :

Function.Periodic (fun (θ : ℝ) => (ActualInitialCoherence.pieces B N0 l).pressure n (x, θ)) (2 * Real.pi)

theorem NavierStokes.ActualInitialMeanEquation.piece_velocity_mean_zero {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (n : ℕ) (x : Point) (i : Fin 3) :

CorrectionState.angularAverage (fun (k : ℕ) (p : ActualInitialCoherence.Point × ℝ) => (ActualInitialCoherence.pieces B N0 l).velocity k p i) n x = 0

theorem NavierStokes.ActualInitialMeanEquation.piece_pressure_mean_zero {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (n : ℕ) (x : Point) :

CorrectionState.angularAverage (ActualInitialCoherence.pieces B N0 l).pressure n x = 0

theorem NavierStokes.ActualInitialMeanEquation.seed_velocity_mean_zero (B N0 n : ℕ) (x : Point) (i : Fin 3) :

CorrectionState.angularAverage (fun (k : ℕ) (p : ActualInitialCoherence.Point × ℝ) => (ActualInitialCoherence.seed B N0).oscillation k p i) n x = 0

theorem NavierStokes.ActualInitialMeanEquation.seed_pressure_mean_zero (B N0 n : ℕ) (x : Point) :

CorrectionState.angularAverage (ActualInitialCoherence.seed B N0).oscillatoryPressure n x = 0

theorem NavierStokes.ActualInitialMeanEquation.initialized_oscillatoryPressure (B N0 : ℕ) :

(ActualInitialCoherence.initialized B N0).oscillatoryPressure = (ActualInitialCoherence.seed B N0).oscillatoryPressure

theorem NavierStokes.ActualInitialMeanEquation.initialized_errors_angularContinuous (B N0 n : ℕ) {x : Point} (hT : 0 < x.2.1.1) (i : Fin 3) :

(Continuous fun (θ : ℝ) => (ActualInitialCoherence.initialized B N0).errors.base n (x, θ) i) ∧ Continuous fun (θ : ℝ) => (ActualInitialCoherence.initialized B N0).errors.total n (x, θ) i

theorem NavierStokes.ActualInitialMeanEquation.initialized_angularData (B N0 : ℕ) :

AngularData strip.domain (ActualInitialCoherence.initialized B N0)

theorem NavierStokes.ActualInitialMeanEquation.initialized_meanHypotheses (B N0 : ℕ) :

LiftedMeanResidual.MeanHypotheses strip.domain (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialCoherence.initialized B N0)

The literal initializer satisfies the local hypotheses of the nonlinear angular-mean identity. No PDE or divergence premise is supplied.

theorem NavierStokes.ActualInitialMeanEquation.initialized_angularMean_fullGoodResidual (B N0 n : ℕ) {x : Point} (hx : x ∈ strip.domain) (i : Fin 3) :

CorrectionStep.angularMeanVector (CorrectionStep.fullGoodResidual (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialCoherence.initialized B N0)) n x i = (ActualInitialCoherence.initialized B N0).meanGoodResidual (CorrectionInitialization.ActualPrimary.commonContext B) n x i

Exact mean equation, with the same Gaussian and alias errors retained by initializedBands.