Regularity of covariances of the actual harmonic state

Finite harmonic fields are assembled before taking their actual angular integral. Smoothness of that integral follows from local compact domination of its genuine parameter derivatives. No covariance regularity or covariance formula is an input.

noncomputable def NavierStokes.WaveStateRegularity.AngularSmooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (Ω : Set D) (u : CorrectionState.Oscillation D) : Prop

Angular smooth, given by ∀ n i, ContDiffOn ℝ ∞ (fun p => u n p i) (HarmonicResidual.liftDomain Ω).

Equations

• NavierStokes.WaveStateRegularity.AngularSmooth Ω u = ∀ (n : ℕ) (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (p : D × ℝ) => u n p i) (NavierStokes.HarmonicResidual.liftDomain Ω)

theorem NavierStokes.WaveStateRegularity.AngularSmooth.add {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {Ω : Set D} {u v : CorrectionState.Oscillation D} (hu : AngularSmooth Ω u) (hv : AngularSmooth Ω v) : AngularSmooth Ω (u + v)

theorem NavierStokes.WaveStateRegularity.compactIntegral_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [ProperSpace D] {Ω : Set D} (hΩ : IsOpen Ω) {F : D × ℝ → ℝ} (hF : ContDiffOn ℝ (↑⊤) F (HarmonicResidual.liftDomain Ω)) (a b : ℝ) (hab : a ≤ b) : ContDiffOn ℝ (↑⊤) (fun (x : D) => ∫ (θ : ℝ) in a..b, F (x, θ)) Ω

Joint local smoothness gives continuous actual parameter jets. Compactness of the angular interval then supplies their local majorants.

theorem NavierStokes.WaveStateRegularity.angularAverage_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [ProperSpace D] {Ω : Set D} (hΩ : IsOpen Ω) {f : CorrectionState.OscillatoryScalar D} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (HarmonicResidual.liftDomain Ω)) : MeanIncrementBounds.SmoothOn Ω (CorrectionState.angularAverage f)

theorem NavierStokes.WaveStateRegularity.bilinearCovariance_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [ProperSpace D] {Ω : Set D} (hΩ : IsOpen Ω) {u v : CorrectionState.Oscillation D} (hu : AngularSmooth Ω u) (hv : AngularSmooth Ω v) (i j : Fin 3) : MeanIncrementBounds.SmoothOn Ω (CorrectionState.bilinearCovariance u v i j)

theorem NavierStokes.WaveStateRegularity.covarianceIncrement_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [ProperSpace D] {Ω : Set D} (hΩ : IsOpen Ω) {u w : CorrectionState.Oscillation D} (hu : AngularSmooth Ω u) (hw : AngularSmooth Ω w) (i j : Fin 3) : MeanIncrementBounds.SmoothOn Ω (SignedMeanGain.covarianceIncrement u w i j)

Smoothness from the actual local harmonic coefficients

theorem NavierStokes.WaveStateRegularity.field_zero_germ {D : Type} [NormedAddCommGroup D] {c : HarmonicFields.Coefficients D} (k : ℝ) (Φ : D → ℝ) (kp : ℤ) {x : D} (θ : ℝ) (hz : ∀ (j : ℤ), c.coeff j =ᶠ[nhds x] fun (x : D) => 0) : HarmonicFields.field c k Φ kp =ᶠ[nhds (x, θ)] fun (x : D × ℝ) => 0

theorem NavierStokes.WaveStateRegularity.field_smoothOn_of_germs {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {Ω C : Set D} (hΩ : IsOpen Ω) (hC : IsOpen C) {c : HarmonicFields.Coefficients D} (hc : HarmonicResidual.SmoothCoefficients (Ω ∩ C) c) {Φ : D → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ (Ω ∩ C)) (k : ℝ) (kp : ℤ) (hz : ∀ x ∈ Ω, x ∉ C → ∀ (j : ℤ), c.coeff j =ᶠ[nhds x] fun (x : D) => 0) : ContDiffOn ℝ (↑⊤) (HarmonicFields.field c k Φ kp) (HarmonicResidual.liftDomain Ω)

structure NavierStokes.WaveStateRegularity.LocalData {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (Ω : Set D) (labels : ℕ → Finset ι) (blocks : ι → CorrectionState.HarmonicBlock D) (C : ℕ → ι → Set D) : Prop

Primitive local data for every active block. Harmonics are the actual finite group-algebra coefficients, including harmonic zero.

• patch_open (n : ℕ) (l : ι) : l ∈ labels n → IsOpen (C n l)
• coefficient (n : ℕ) (l : ι) : l ∈ labels n → ∀ (i : Fin 3), HarmonicResidual.SmoothCoefficients (Ω ∩ C n l) ((blocks l).velocity n i)
• phase (n : ℕ) (l : ι) : l ∈ labels n → ContDiffOn ℝ (↑⊤) ((blocks l).phase n) (Ω ∩ C n l)
• off_patch (n : ℕ) (l : ι) : l ∈ labels n → ∀ x ∈ Ω, x ∉ C n l → ∀ (i : Fin 3) (j : ℤ), ((blocks l).velocity n i).coeff j =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.WaveStateRegularity.LocalData.of_global {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {Ω : Set D} {labels : ℕ → Finset ι} {blocks : ι → CorrectionState.HarmonicBlock D} (hc : ∀ (n : ℕ), ∀ l ∈ labels n, ∀ (i : Fin 3), HarmonicResidual.SmoothCoefficients Ω ((blocks l).velocity n i)) (hΦ : ∀ (n : ℕ), ∀ l ∈ labels n, ContDiffOn ℝ (↑⊤) ((blocks l).phase n) Ω) : LocalData Ω labels blocks fun (x : ℕ) (x_1 : ι) => Set.univ

theorem NavierStokes.WaveStateRegularity.LocalData.block_smooth {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {Ω : Set D} {labels : ℕ → Finset ι} {blocks : ι → CorrectionState.HarmonicBlock D} {C : ℕ → ι → Set D} (h : LocalData Ω labels blocks C) (hΩ : IsOpen Ω) (n : ℕ) (l : ι) (hl : l ∈ labels n) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (p : D × ℝ) => (blocks l).oscillation n p i) (HarmonicResidual.liftDomain Ω)

theorem NavierStokes.WaveStateRegularity.LocalData.fieldSum_smooth {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {Ω : Set D} {labels : ℕ → Finset ι} {blocks : ι → CorrectionState.HarmonicBlock D} {C : ℕ → ι → Set D} (h : LocalData Ω labels blocks C) (hΩ : IsOpen Ω) : AngularSmooth Ω (LabelSumBounds.fieldSum labels fun (l : ι) => (blocks l).oscillation)

Actual support in the moving radial annulus

@[reducible, inline]

abbrev NavierStokes.WaveStateRegularity.Plane : Type

Plane: an abbreviation for GaugeDebtIncrement.Plane.

Equations

• NavierStokes.WaveStateRegularity.Plane = NavierStokes.GaugeDebtIncrement.Plane

@[reducible, inline]

abbrev NavierStokes.WaveStateRegularity.Point : Type

Point: an abbreviation for GaugeDebtIncrement.Point.

Equations

• NavierStokes.WaveStateRegularity.Point = NavierStokes.GaugeDebtIncrement.Point

noncomputable def NavierStokes.WaveStateRegularity.WaveSupport {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (a b : ℝ) (u : CorrectionState.Oscillation Point) : Prop

Wave support, given by ∀ n θ i, VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength coord) U.carrier (fun x => u n (x, θ) i).

Equations

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

theorem NavierStokes.WaveStateRegularity.WaveSupport.add {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {u v : CorrectionState.Oscillation Point} (hu : WaveSupport U a b u) (hv : WaveSupport U a b v) : WaveSupport U a b (u + v)

theorem NavierStokes.WaveStateRegularity.angularAverage_supported {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : CorrectionState.OscillatoryScalar Point} (hs : ∀ (n : ℕ) (θ : ℝ), VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength coord) U.carrier fun (x : PressureStream.Lift TorusInverse.Plane) => f n (x, θ)) (n : ℕ) : VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength coord) U.carrier (CorrectionState.angularAverage f n)

theorem NavierStokes.WaveStateRegularity.bilinearCovariance_regular {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) {u v : CorrectionState.Oscillation Point} (hu : AngularSmooth (PhysicalMeanDomain.slowDomain U.carrier) u) (hv : AngularSmooth (PhysicalMeanDomain.slowDomain U.carrier) v) (hs : WaveSupport U a b u) (i j : Fin 3) : GaugeDebtIncrement.Regular U a b (CorrectionState.bilinearCovariance u v i j)

theorem NavierStokes.WaveStateRegularity.covarianceIncrement_regular {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) {u w : CorrectionState.Oscillation Point} (hu : AngularSmooth (PhysicalMeanDomain.slowDomain U.carrier) u) (hw : AngularSmooth (PhysicalMeanDomain.slowDomain U.carrier) w) (hs : WaveSupport U a b w) (i j : Fin 3) : GaugeDebtIncrement.Regular U a b (SignedMeanGain.covarianceIncrement u w i j)

Only the new wave needs annular support: outside it the old covariance cancels in the literal difference of angular integrals.

noncomputable def NavierStokes.WaveStateRegularity.CoefficientSupport {ι : Type u_1} {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (a b : ℝ) (labels : ℕ → Finset ι) (blocks : ι → CorrectionState.HarmonicBlock Point) : Prop

Geometric support of the actual complex coefficient functions. This includes the zero harmonic and imposes no covariance condition.

Equations

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

theorem NavierStokes.WaveStateRegularity.field_eq_zero_of_coefficients {D : Type} {c : HarmonicFields.Coefficients D} (k : ℝ) (Φ : D → ℝ) (kp : ℤ) (x : D) (θ : ℝ) (hz : ∀ (j : ℤ), c.coeff j x = 0) : HarmonicFields.field c k Φ kp (x, θ) = 0

theorem NavierStokes.WaveStateRegularity.fieldSum_support_of_coefficients {ι : Type u_1} {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {labels : ℕ → Finset ι} {blocks : ι → CorrectionState.HarmonicBlock Point} (hs : CoefficientSupport U a b labels blocks) : WaveSupport U a b (LabelSumBounds.fieldSum labels fun (l : ι) => (blocks l).oscillation)

theorem NavierStokes.WaveStateRegularity.fieldSum_support {ι : Type u_1} {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {labels : ℕ → Finset ι} {u : ι → CorrectionState.Oscillation Point} (hs : ∀ (n : ℕ), ∀ l ∈ labels n, ∀ (θ : ℝ) (i : Fin 3), VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength coord) U.carrier fun (x : PressureStream.Lift TorusInverse.Plane) => u l n (x, θ) i) : WaveSupport U a b (LabelSumBounds.fieldSum labels u)

Concrete finite-active state adapters

theorem NavierStokes.WaveStateRegularity.fieldSum_covariance_regular {ι : Type u_1} {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) {labels₀ : ℕ → Finset ι} {blocks₀ : ι → CorrectionState.HarmonicBlock Point} {C₀ : ℕ → ι → Set Point} (h : LocalData (PhysicalMeanDomain.slowDomain U.carrier) labels₀ blocks₀ C₀) (hs : CoefficientSupport U a b labels₀ blocks₀) (i j : Fin 3) : GaugeDebtIncrement.Regular U a b (CorrectionState.bilinearCovariance (LabelSumBounds.fieldSum labels₀ fun (l : ι) => (blocks₀ l).oscillation) (LabelSumBounds.fieldSum labels₀ fun (l : ι) => (blocks₀ l).oscillation) i j)

theorem NavierStokes.WaveStateRegularity.fieldSum_covarianceIncrement_regular {ι : Type u_1} {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) {labels₀ labels₁ : ℕ → Finset ι} {blocks₀ blocks₁ : ι → CorrectionState.HarmonicBlock Point} {C₀ C₁ : ℕ → ι → Set Point} (h₀ : LocalData (PhysicalMeanDomain.slowDomain U.carrier) labels₀ blocks₀ C₀) (h₁ : LocalData (PhysicalMeanDomain.slowDomain U.carrier) labels₁ blocks₁ C₁) (hs₁ : CoefficientSupport U a b labels₁ blocks₁) (i j : Fin 3) : GaugeDebtIncrement.Regular U a b (SignedMeanGain.covarianceIncrement (LabelSumBounds.fieldSum labels₀ fun (l : ι) => (blocks₀ l).oscillation) (LabelSumBounds.fieldSum labels₁ fun (l : ι) => (blocks₁ l).oscillation) i j)

theorem NavierStokes.WaveStateRegularity.state_covariance_regular {ι : Type u_1} {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) {labels₀ : ℕ → Finset ι} {blocks₀ : ι → CorrectionState.HarmonicBlock Point} {C₀ : ℕ → ι → Set Point} (u : CorrectionState.State Point) (hu : u.oscillation = LabelSumBounds.fieldSum labels₀ fun (l : ι) => (blocks₀ l).oscillation) (h : LocalData (PhysicalMeanDomain.slowDomain U.carrier) labels₀ blocks₀ C₀) (hs : CoefficientSupport U a b labels₀ blocks₀) (i j : Fin 3) : GaugeDebtIncrement.Regular U a b (u.covariance i j)

theorem NavierStokes.WaveStateRegularity.state_covarianceIncrement_regular {ι : Type u_1} {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) {labels₀ labels₁ : ℕ → Finset ι} {blocks₀ blocks₁ : ι → CorrectionState.HarmonicBlock Point} {C₀ C₁ : ℕ → ι → Set Point} (u : CorrectionState.State Point) (hu : u.oscillation = LabelSumBounds.fieldSum labels₀ fun (l : ι) => (blocks₀ l).oscillation) (h₀ : LocalData (PhysicalMeanDomain.slowDomain U.carrier) labels₀ blocks₀ C₀) (h₁ : LocalData (PhysicalMeanDomain.slowDomain U.carrier) labels₁ blocks₁ C₁) (hs₁ : CoefficientSupport U a b labels₁ blocks₁) (i j : Fin 3) : GaugeDebtIncrement.Regular U a b (SignedMeanGain.covarianceIncrement u.oscillation (LabelSumBounds.fieldSum labels₁ fun (l : ι) => (blocks₁ l).oscillation) i j)

theorem NavierStokes.WaveStateRegularity.waveStage_covariance_regular {ι : Type u_1} {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) {labels₀ labels₁ : ℕ → Finset ι} {blocks₀ blocks₁ : ι → CorrectionState.HarmonicBlock Point} {C₀ C₁ : ℕ → ι → Set Point} (g : VariableGaugeMean.GaugeData Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (hu : u.oscillation = LabelSumBounds.fieldSum labels₀ fun (l : ι) => (blocks₀ l).oscillation) (h₀ : LocalData (PhysicalMeanDomain.slowDomain U.carrier) labels₀ blocks₀ C₀) (h₁ : LocalData (PhysicalMeanDomain.slowDomain U.carrier) labels₁ blocks₁ C₁) (hs₀ : CoefficientSupport U a b labels₀ blocks₀) (hs₁ : CoefficientSupport U a b labels₁ blocks₁) (q : CorrectionState.OscillatoryScalar Point) (gaussian : CorrectionState.Oscillation Point) (i j : Fin 3) : GaugeDebtIncrement.Regular U a b ((SignedMeanGain.waveStage g c u (LabelSumBounds.fieldSum labels₁ fun (l : ι) => (blocks₁ l).oscillation) q gaussian).covariance i j)