The correction context of the actual slow base #
The native slow order is (T,Z). The explicit linear map slowCoordinates
converts to the (R,(Z,T)) order used by the physical base charts. Every
field below uses one fixed final profile, coefficient family, and schedule.
Initial primary residual classes #
The primary coefficient and its Gaussian error are the actual cutoff/curl construction. The improved nonlinear bound uses the exact divergence of that curl, before projecting the literal residual into its finite harmonics.
noncomputable def
NavierStokes.PrimaryResidualClass.directions
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(c : CorrectionState.Context D)
:
The context's literal graph directions lifted to the explicit angle.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.PrimaryResidualClass.directions_radial
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(c : CorrectionState.Context D)
(n : ℕ)
:
theorem
NavierStokes.PrimaryResidualClass.directions_axial
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(s : WeightedClasses.StripData D)
(c : CorrectionState.Context D)
(hε : s.epsilon = c.operators.epsilon)
(n : ℕ)
:
theorem
NavierStokes.PrimaryResidualClass.directions_time
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(s : WeightedClasses.StripData D)
(c : CorrectionState.Context D)
(hε : s.epsilon = c.operators.epsilon)
(n : ℕ)
:
(LinearWaveResidual.timeDirection ((HarmonicWaveInteraction.productStrip s).epsilon n) ((directions c).fastField n)
fun (x : D × ℝ) => (directions c).slow) = HarmonicResidual.liftDirection (HarmonicResidual.contextFrame c n).time
structure
NavierStokes.PrimaryResidualClass.Matches
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(s : WeightedClasses.StripData D)
(c : CorrectionState.Context D)
(a : LinearWaveBounds.WaveCoefficients (D × ℝ))
:
Matching concerns primitive fields, never a residual or a residual bound.
- base (n : ℕ) : LinearWaveResidual.complexBase (a.radius n) (a.radialBase n) (a.frequencyBase n) (a.axialBase n) = fun (p : D × ℝ) => HarmonicResidual.contextBase c n p.1
Instances For
structure
NavierStokes.PrimaryResidualClass.AngularData
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(a : LinearWaveBounds.WaveCoefficients (D × ℝ))
(ψ : ℕ → D × ℝ → ℝ)
:
Primitive angular translation data for one primary field.
- radialBase (n : ℕ) : CopyAngularInvariance.Invariant (0, 1) (a.radialBase n)
- frequencyBase (n : ℕ) : CopyAngularInvariance.Invariant (0, 1) (a.frequencyBase n)
- cutoff (n : ℕ) : CopyAngularInvariance.Invariant (0, 1) (ψ n)
Instances For
theorem
NavierStokes.PrimaryResidualClass.invariant_fst
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{E : Type}
(f : D → E)
:
theorem
NavierStokes.PrimaryResidualClass.directions_radial_invariant
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(c : CorrectionState.Context D)
(n : ℕ)
:
CopyAngularInvariance.Invariant (0, 1) ((directions c).radialField n)
theorem
NavierStokes.PrimaryResidualClass.AngularData.corrected_amplitude
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
(ha : AngularData a ψ)
(s : WeightedClasses.StripData D)
(c : CorrectionState.Context D)
(n : ℕ)
:
CopyAngularInvariance.Invariant (0, 1)
((a.corrected (HarmonicWaveInteraction.productStrip s) (directions c) ψ).amplitude n)
theorem
NavierStokes.PrimaryResidualClass.AngularData.corrected_pressure
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
(ha : AngularData a ψ)
(s : WeightedClasses.StripData D)
(c : CorrectionState.Context D)
(n : ℕ)
:
CopyAngularInvariance.Invariant (0, 1)
((a.corrected (HarmonicWaveInteraction.productStrip s) (directions c) ψ).pressure n)
theorem
NavierStokes.PrimaryResidualClass.principal_invariant
{X : Type}
[NormedAddCommGroup X]
[NormedSpace ℝ X]
{θ : X}
{R F G : X → ℝ}
{Vr Vθ Vz Vf : X → X}
{Φ : X → ℝ}
{m : ℝ}
{a : X → HarmonicCalculus.ComplexVector}
{p : X → ℂ}
(hR : CopyAngularInvariance.Invariant θ R)
(hF : CopyAngularInvariance.Invariant θ F)
(hG : CopyAngularInvariance.Invariant θ G)
(hr : CopyAngularInvariance.Invariant θ Vr)
(hθ : CopyAngularInvariance.Invariant θ Vθ)
(hz : CopyAngularInvariance.Invariant θ Vz)
(hf : CopyAngularInvariance.Invariant θ Vf)
(hΦ : CopyAngularInvariance.AffinePhase θ m Φ)
(ha : CopyAngularInvariance.Invariant θ a)
(hp : CopyAngularInvariance.Invariant θ p)
(ε k : ℝ)
:
CopyAngularInvariance.Invariant θ (LinearWaveResidual.principal ε k R F G Vr Vθ Vz Vf Φ a p)
theorem
NavierStokes.PrimaryResidualClass.remainder_invariant
{X : Type}
[NormedAddCommGroup X]
[NormedSpace ℝ X]
{θ : X}
{R b F G : X → ℝ}
{Vr Vθ Vz Vf Vs : X → X}
{Φ : X → ℝ}
{m : ℝ}
{a : X → HarmonicCalculus.ComplexVector}
{p : X → ℂ}
(hR : CopyAngularInvariance.Invariant θ R)
(hb : CopyAngularInvariance.Invariant θ b)
(hF : CopyAngularInvariance.Invariant θ F)
(hG : CopyAngularInvariance.Invariant θ G)
(hr : CopyAngularInvariance.Invariant θ Vr)
(hθ : CopyAngularInvariance.Invariant θ Vθ)
(hz : CopyAngularInvariance.Invariant θ Vz)
(hf : CopyAngularInvariance.Invariant θ Vf)
(hs : CopyAngularInvariance.Invariant θ Vs)
(hΦ : CopyAngularInvariance.AffinePhase θ m Φ)
(ha : CopyAngularInvariance.Invariant θ a)
(hp : CopyAngularInvariance.Invariant θ p)
(ε k : ℝ)
:
CopyAngularInvariance.Invariant θ (LinearWaveResidual.remainder ε k R b F G Vr Vθ Vz Vf Vs Φ a p)
theorem
NavierStokes.PrimaryResidualClass.AngularData.constructedGood
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
(ha : AngularData a ψ)
(s : WeightedClasses.StripData D)
(c : CorrectionState.Context D)
(n : ℕ)
:
structure
NavierStokes.PrimaryResidualClass.Inputs
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(s : WeightedClasses.StripData D)
(P : ℕ → D → ℝ)
(κ : ℝ)
(c : CorrectionState.Context D)
(a : LinearWaveBounds.WaveCoefficients (D × ℝ))
(ψ : ℕ → D × ℝ → ℝ)
(kp : ℕ → ℤ)
:
Quantitative and geometric inputs concern the primitive primary wave. In particular neither a good-residual class nor a residual identity is a field.
- matching : Matches s c a
- operators : MeanIncrementBounds.OperatorBounds s c.operators κ
- coefficients : LinearWaveBounds.InputBounds (HarmonicWaveInteraction.productStrip s) (fun (n : ℕ) (p : D × ℝ) => P n p.1) (1 / 2) κ (directions c) a
- cutoff : WeightedClasses.UnweightedClass (HarmonicWaveInteraction.productStrip s) 0 ψ
- angular : AngularData a ψ
- phase_smooth (n : ℕ) : ContDiffOn ℝ (↑⊤) (a.phase n) (HarmonicWaveInteraction.productStrip s).domain
- normal_jets : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain (HarmonicWaveInteraction.productStrip s)) (a.normal (HarmonicWaveInteraction.productStrip s) (directions c))
- inverse_frequency : WeightedClasses.BandBound (HarmonicWaveInteraction.productStrip s) (1 / 2) fun (n : ℕ) => 1 / a.frequency n
- geometry (n : ℕ) : CurlClassBounds.CylindricalGeometry (HarmonicWaveInteraction.productStrip s).domain (a.radius n) ((directions c).radialField n) (fun (x : D × ℝ) => (directions c).angular) ((directions c).axialField (HarmonicWaveInteraction.productStrip s) n)
- tangent (n : ℕ) (p : D × ℝ) : p.1 ∈ s.domain → HarmonicCalculus.normalDot (a.normal (HarmonicWaveInteraction.productStrip s) (directions c) n p) (a.amplitude n p) = 0
- principal_zero (n : ℕ) (p : D × ℝ) : p.1 ∈ s.domain → ψ n p ≠ 0 → a.principal (HarmonicWaveInteraction.productStrip s) (directions c) n p = 0
Instances For
noncomputable def
NavierStokes.PrimaryResidualClass.corrected
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(s : WeightedClasses.StripData D)
(c : CorrectionState.Context D)
(a : LinearWaveBounds.WaveCoefficients (D × ℝ))
(ψ : ℕ → D × ℝ → ℝ)
:
Corrected, given by a.corrected (HarmonicWaveInteraction.productStrip s) (directions c) ψ.
Equations
Instances For
noncomputable def
NavierStokes.PrimaryResidualClass.primaryBlock
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(s : WeightedClasses.StripData D)
(c : CorrectionState.Context D)
(a : LinearWaveBounds.WaveCoefficients (D × ℝ))
(ψ : ℕ → D × ℝ → ℝ)
(kp : ℕ → ℤ)
:
Primary block, given by SignedWaveUpdate.blockOfCoefficients (corrected s c a ψ) kp.
Equations
Instances For
noncomputable def
NavierStokes.PrimaryResidualClass.gaussianCoefficients
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(c : CorrectionState.Context D)
(a : LinearWaveBounds.WaveCoefficients (D × ℝ))
(ψ : ℕ → D × ℝ → ℝ)
:
Gaussian coefficients, defined pointwise by ErrorHarmonics.conjugatePair 1 (fun x => LinearWaveBounds.excludedSlotError (directions c) ψ a.amplitude 0 n (x, 0) i).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.PrimaryResidualClass.goodCoefficients
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(s : WeightedClasses.StripData D)
(c : CorrectionState.Context D)
(a : LinearWaveBounds.WaveCoefficients (D × ℝ))
(ψ : ℕ → D × ℝ → ℝ)
:
Good coefficients, defined pointwise by ErrorHarmonics.conjugatePair 1 (fun x => a.constructedGood (HarmonicWaveInteraction.productStrip s) (directions c) ψ n (x, 0) i).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.PrimaryResidualClass.wave_slice
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{α : ℝ}
{f : ℕ → D × ℝ → E}
(hf : WeightedClasses.WaveClass (HarmonicWaveInteraction.productStrip s) (fun (n : ℕ) (p : D × ℝ) => P n p.1) α f)
:
WeightedClasses.WaveClass s P α fun (n : ℕ) (x : D) => f n (x, 0)
theorem
NavierStokes.PrimaryResidualClass.Inputs.corrected_bounds
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
:
LinearWaveBounds.InputBounds (HarmonicWaveInteraction.productStrip s) (fun (n : ℕ) (p : D × ℝ) => P n p.1) (1 / 2) κ
(directions c) (corrected s c a ψ)
theorem
NavierStokes.PrimaryResidualClass.Inputs.good_class
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
:
WeightedClasses.WaveClass (HarmonicWaveInteraction.productStrip s) (fun (n : ℕ) (p : D × ℝ) => P n p.1) (1 - 3 * κ)
(a.constructedGood (HarmonicWaveInteraction.productStrip s) (directions c) ψ)
theorem
NavierStokes.PrimaryResidualClass.Inputs.good_coefficients_class
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
(j : ℤ)
(i : Fin 3)
:
WeightedClasses.WaveClass s P (1 - 3 * κ) fun (n : ℕ) (x : D) => (goodCoefficients s c a ψ n i).coeff j x
theorem
NavierStokes.PrimaryResidualClass.Inputs.primary_bounds
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
:
CorrectionState.HarmonicBlock.WaveBounds s P (1 / 2) (primaryBlock s c a ψ kp)
theorem
NavierStokes.PrimaryResidualClass.Inputs.primary_pressure
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
:
CorrectionState.HarmonicBlock.PressureBounds s P 1 (primaryBlock s c a ψ kp)
theorem
NavierStokes.PrimaryResidualClass.Inputs.exact_conditions
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
:
theorem
NavierStokes.PrimaryResidualClass.Inputs.normal_ne
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
(n : ℕ)
(p : D × ℝ)
(hp : p.1 ∈ s.domain)
:
theorem
NavierStokes.PrimaryResidualClass.Inputs.corrected_divergence
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
(n : ℕ)
(p : D × ℝ)
(hp : p.1 ∈ s.domain)
:
HarmonicCalculus.cylindricalDivergence (a.radius n) ((directions c).radialField n)
(fun (x : D × ℝ) => (directions c).angular) ((directions c).axialField (HarmonicWaveInteraction.productStrip s) n)
(HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) ((corrected s c a ψ).amplitude n)) p = 0
theorem
NavierStokes.PrimaryResidualClass.Inputs.linear_identity
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
(n : ℕ)
(p : D × ℝ)
(hp : p.1 ∈ s.domain)
:
(corrected s c a ψ).harmonicResidual (HarmonicWaveInteraction.productStrip s) (directions c) n p = HarmonicCalculus.vectorMode (a.frequency n) (a.phase n)
(a.constructedGood (HarmonicWaveInteraction.productStrip s) (directions c) ψ n) p + HarmonicCalculus.vectorMode (a.frequency n) (a.phase n)
(LinearWaveBounds.excludedSlotError (directions c) ψ a.amplitude 0 n) p
Real projection, given by Complex.ofRealCLM.comp Complex.reCLM.
Instances For
@[simp]
theorem
NavierStokes.PrimaryResidualClass.divergence_map
{X : Type}
[NormedAddCommGroup X]
[NormedSpace ℝ X]
(L : ℂ →L[ℝ] ℂ)
(R : X → ℝ)
(Vr Vθ Vz : X → X)
{v : X → HarmonicCalculus.ComplexVector}
{x : X}
(hv : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : X) => v y i) x)
:
HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz (fun (y : X) (i : Fin 3) => L (v y i)) x = L (HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz v x)
theorem
NavierStokes.PrimaryResidualClass.linearResidual_realProjection
{X : Type}
[NormedAddCommGroup X]
[NormedSpace ℝ X]
{U : Set X}
(hU : IsOpen U)
(ε : ℝ)
(R : X → ℝ)
{Vr Vθ Vz : X → X}
(Vt : X → X)
(hVr : ContDiffOn ℝ (↑⊤) Vr U)
(hVθ : ContDiffOn ℝ (↑⊤) Vθ U)
(hVz : ContDiffOn ℝ (↑⊤) Vz U)
{B : X → Fin 3 → ℝ}
{v : X → HarmonicCalculus.ComplexVector}
{p : X → ℂ}
(hv : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : X) => v y i) U)
{x : X}
(hB : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : X) => B y i) x)
(hp : DifferentiableAt ℝ p x)
(hx : x ∈ U)
(i : Fin 3)
:
(LinearWaveResidual.linearResidual ε R Vr Vθ Vz Vt (LinearWaveResidual.realLift B)
(fun (y : X) (j : Fin 3) => realProjection (v y j)) (fun (y : X) => realProjection (p y)) x i).re = (LinearWaveResidual.linearResidual ε R Vr Vθ Vz Vt (LinearWaveResidual.realLift B) v p x i).re
theorem
NavierStokes.PrimaryResidualClass.pair_field_of_invariant
{X : Type}
[NormedAddCommGroup X]
[NormedSpace ℝ X]
{f : X × ℝ → ℂ}
{Φ : X × ℝ → ℝ}
(k : ℝ)
(kp : ℤ)
(hf : CopyAngularInvariance.Invariant (0, 1) f)
(hΦ : ∀ (x : X) (θ : ℝ), k * Φ (x, θ) = k * Φ (x, 0) + ↑kp * θ)
(p : X × ℝ)
:
HarmonicFields.field (ErrorHarmonics.conjugatePair 1 fun (x : X) => f (x, 0)) k (fun (x : X) => Φ (x, 0)) kp p = realProjection (HarmonicCalculus.mode k Φ f p)
theorem
NavierStokes.PrimaryResidualClass.excluded_invariant
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
(ha : AngularData a ψ)
(c : CorrectionState.Context D)
(n : ℕ)
:
theorem
NavierStokes.PrimaryResidualClass.Inputs.primary_field
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
(n : ℕ)
(p : D × ℝ)
(i : Fin 3)
:
HarmonicFields.field ((primaryBlock s c a ψ kp).velocity n i) (a.frequency n) (fun (x : D) => a.phase n (x, 0)) (kp n)
p = realProjection (HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) ((corrected s c a ψ).amplitude n) p i)
theorem
NavierStokes.PrimaryResidualClass.Inputs.pressure_field
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
(n : ℕ)
(p : D × ℝ)
:
HarmonicFields.field ((primaryBlock s c a ψ kp).pressure n) (a.frequency n) (fun (x : D) => a.phase n (x, 0)) (kp n) p = realProjection (HarmonicCalculus.mode (a.frequency n) (a.phase n) ((corrected s c a ψ).pressure n) p)
theorem
NavierStokes.PrimaryResidualClass.Inputs.good_field
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
(n : ℕ)
(p : D × ℝ)
(i : Fin 3)
:
HarmonicFields.field (goodCoefficients s c a ψ n i) (a.frequency n) (fun (x : D) => a.phase n (x, 0)) (kp n) p = realProjection
(HarmonicCalculus.vectorMode (a.frequency n) (a.phase n)
(a.constructedGood (HarmonicWaveInteraction.productStrip s) (directions c) ψ n) p i)
theorem
NavierStokes.PrimaryResidualClass.Inputs.gaussian_field
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
(n : ℕ)
(p : D × ℝ)
(i : Fin 3)
:
HarmonicFields.field (gaussianCoefficients c a ψ n i) (a.frequency n) (fun (x : D) => a.phase n (x, 0)) (kp n) p = realProjection
(HarmonicCalculus.vectorMode (a.frequency n) (a.phase n)
(LinearWaveBounds.excludedSlotError (directions c) ψ a.amplitude 0 n) p i)
theorem
NavierStokes.PrimaryResidualClass.Inputs.phase_slow_smooth
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
(n : ℕ)
:
theorem
NavierStokes.PrimaryResidualClass.Inputs.primary_smooth
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
(n : ℕ)
(i : Fin 3)
:
HarmonicResidual.SmoothCoefficients s.domain ((primaryBlock s c a ψ kp).velocity n i)
theorem
NavierStokes.PrimaryResidualClass.Inputs.pressure_smooth
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
(n : ℕ)
:
HarmonicResidual.SmoothCoefficients s.domain ((primaryBlock s c a ψ kp).pressure n)
theorem
NavierStokes.PrimaryResidualClass.Inputs.raw_velocity_smooth
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
(n : ℕ)
(i : Fin 3)
:
ContDiffOn ℝ (↑⊤)
(fun (p : D × ℝ) => HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) ((corrected s c a ψ).amplitude n) p i)
(HarmonicWaveInteraction.productStrip s).domain
theorem
NavierStokes.PrimaryResidualClass.Inputs.raw_pressure_smooth
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) (HarmonicCalculus.mode (a.frequency n) (a.phase n) ((corrected s c a ψ).pressure n))
(HarmonicWaveInteraction.productStrip s).domain
noncomputable def
NavierStokes.PrimaryResidualClass.linearCoefficients
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(s : WeightedClasses.StripData D)
(c : CorrectionState.Context D)
(a : LinearWaveBounds.WaveCoefficients (D × ℝ))
(ψ : ℕ → D × ℝ → ℝ)
(kp : ℕ → ℤ)
:
Linear coefficients as an element of HarmonicResidual.BlockCoefficients D.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.PrimaryResidualClass.Inputs.base_smooth
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
(n : ℕ)
(i : Fin 3)
:
ContDiffOn ℝ (↑⊤) (fun (x : D) => HarmonicResidual.contextBase c n x i) s.domain
theorem
NavierStokes.PrimaryResidualClass.Inputs.radial_smooth
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) (HarmonicResidual.contextFrame c n).radial s.domain
theorem
NavierStokes.PrimaryResidualClass.Inputs.axial_smooth
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) (HarmonicResidual.contextFrame c n).axial s.domain
theorem
NavierStokes.PrimaryResidualClass.Inputs.primary_amplitude_real
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(n : ℕ)
:
HarmonicMeanInteraction.blockAmplitude (primaryBlock s c a ψ kp) n = (primaryBlock s c a ψ kp).velocity n
theorem
NavierStokes.PrimaryResidualClass.Inputs.primary_pressure_real
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(n : ℕ)
:
HarmonicResidual.realCoefficients ((primaryBlock s c a ψ kp).pressure n) = (primaryBlock s c a ψ kp).pressure n
theorem
NavierStokes.PrimaryResidualClass.Inputs.harmonicResidual_context
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
(n : ℕ)
:
(corrected s c a ψ).harmonicResidual (HarmonicWaveInteraction.productStrip s) (directions c) n = LinearWaveResidual.linearResidual (c.operators.epsilon n) (fun (p : D × ℝ) => c.operators.radius p.1)
(HarmonicResidual.liftDirection (HarmonicResidual.contextFrame c n).radial) HarmonicResidual.angularDirection
(HarmonicResidual.liftDirection (HarmonicResidual.contextFrame c n).axial)
(HarmonicResidual.liftDirection (HarmonicResidual.contextFrame c n).time)
(fun (p : D × ℝ) => HarmonicResidual.contextBase c n p.1)
(HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) ((corrected s c a ψ).amplitude n))
(HarmonicCalculus.mode (a.frequency n) (a.phase n) ((corrected s c a ψ).pressure n))
theorem
NavierStokes.PrimaryResidualClass.Inputs.linear_field_re
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
(n : ℕ)
(p : D × ℝ)
(hp : p.1 ∈ s.domain)
(i : Fin 3)
:
(HarmonicFields.field (linearCoefficients s c a ψ kp n i) (a.frequency n) (fun (x : D) => a.phase n (x, 0)) (kp n)
p).re = ((corrected s c a ψ).harmonicResidual (HarmonicWaveInteraction.productStrip s) (directions c) n p i).re
theorem
NavierStokes.PrimaryResidualClass.Inputs.linear_gaussian_coefficient
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
(n : ℕ)
(x : D)
(hx : x ∈ s.domain)
(i : Fin 3)
(j : ℤ)
:
(HarmonicResidual.realCoefficients (linearCoefficients s c a ψ kp n i - gaussianCoefficients c a ψ n i)).coeff j x = (goodCoefficients s c a ψ n i).coeff j x
theorem
NavierStokes.PrimaryResidualClass.Inputs.full_primary_divergence
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
(n : ℕ)
(p : D × ℝ)
(hp : p.1 ∈ s.domain)
:
HarmonicCalculus.cylindricalDivergence (fun (q : D × ℝ) => c.operators.radius q.1)
(HarmonicResidual.liftDirection (HarmonicResidual.contextFrame c n).radial) HarmonicResidual.angularDirection
(HarmonicResidual.liftDirection (HarmonicResidual.contextFrame c n).axial)
(fun (q : D × ℝ) (i : Fin 3) => ↑((primaryBlock s c a ψ kp).oscillation n q i)) p = 0
theorem
NavierStokes.PrimaryResidualClass.Inputs.primary_modeSolenoidal
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
:
HarmonicWaveInteraction.ModeSolenoidal s c (primaryBlock s c a ψ kp)
theorem
NavierStokes.PrimaryResidualClass.Inputs.primary_band
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
:
(primaryBlock s c a ψ kp).BandLimited 1
theorem
NavierStokes.PrimaryResidualClass.Inputs.primary_zeroMode
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
:
HarmonicWaveInteraction.ZeroMode (primaryBlock s c a ψ kp)
theorem
NavierStokes.PrimaryResidualClass.Inputs.convection_class
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
(j : ℤ)
(i : Fin 3)
:
WeightedClasses.WaveClass s P (1 - κ) fun (n : ℕ) (x : D) =>
(HarmonicResidual.transport (HarmonicResidual.contextFrame c n) (a.frequency n) (fun (y : D) => a.phase n (y, 0))
(kp n) (HarmonicMeanInteraction.blockAmplitude (primaryBlock s c a ψ kp) n)
(HarmonicMeanInteraction.blockAmplitude (primaryBlock s c a ψ kp) n) i).coeff
j x
theorem
NavierStokes.PrimaryResidualClass.Inputs.linear_good_class
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
(j : ℤ)
(i : Fin 3)
:
WeightedClasses.WaveClass s P (1 - 3 * κ) fun (n : ℕ) (x : D) =>
(HarmonicResidual.realCoefficients (linearCoefficients s c a ψ kp n i - gaussianCoefficients c a ψ n i)).coeff j x
theorem
NavierStokes.PrimaryResidualClass.Inputs.initial_residual_class
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
(u : CorrectionState.State D)
(hmean : u.mean = { radial := 0, angular := 0, axial := 0 })
(A : HarmonicResidual.BlockCoefficients D)
(hA : ∀ (n : ℕ) (i : Fin 3) (j : ℤ), j ≠ 0 → (A n i).coeff j = 0)
:
CorrectionState.HarmonicBlock.WaveBounds s P (7 / 10)
(HarmonicResidual.residualBlock c u (primaryBlock s c a ψ kp) (gaussianCoefficients c a ψ) A)
The actual extracted residual of the initial primary wave. The alias is retained in the literal formula; its proved zero-mode property is used only after the nonconstant coefficient is selected.
theorem
NavierStokes.PrimaryResidualClass.Inputs.initial_residual_class_of_zero_mode
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ℕ → D → ℝ}
{κ : ℝ}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(h : Inputs s P κ c a ψ kp)
(u : CorrectionState.State D)
(hmean : u.mean = { radial := 0, angular := 0, axial := 0 })
(A : HarmonicResidual.BlockCoefficients D)
(hA : ∀ (n : ℕ) (i : Fin 3), HarmonicFields.BandLimited (A n i) 0)
:
CorrectionState.HarmonicBlock.WaveBounds s P (7 / 10)
(HarmonicResidual.residualBlock c u (primaryBlock s c a ψ kp) (gaussianCoefficients c a ψ) A)
theorem
NavierStokes.PrimaryResidualClass.Inputs.initial_residual_band
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{c : CorrectionState.Context D}
{a : LinearWaveBounds.WaveCoefficients (D × ℝ)}
{ψ : ℕ → D × ℝ → ℝ}
{kp : ℕ → ℤ}
(u : CorrectionState.State D)
(A : HarmonicResidual.BlockCoefficients D)
(hA : ∀ (n : ℕ) (i : Fin 3), HarmonicFields.BandLimited (A n i) 0)
:
(HarmonicResidual.residualBlock c u (primaryBlock s c a ψ kp) (gaussianCoefficients c a ψ) A).BandLimited 2
The actual primary material-phase defect #
The large axial term in the phase is cancelled by its actual material derivative before estimating any jets. Only the slow coordinate map and slot coordinate require polynomial bounds; the angular coordinate and the unstripped phase itself need no such bound.
structure
NavierStokes.PrimaryMaterialDefect.NativeCoordinates
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(s : WeightedClasses.StripData E)
(d : LinearWaveBounds.GraphDirections E)
(χ : ℕ → E → Slot)
:
First-order chart identities, including the direction annihilated by the physical radial graph derivative. No phase derivative is an input.
Instances For
theorem
NavierStokes.PrimaryMaterialDefect.NativeCoordinates.radialField
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData E}
{d : LinearWaveBounds.GraphDirections E}
{χ : ℕ → E → Slot}
(hχ : NativeCoordinates s d χ)
(n : ℕ)
{x : E}
(hx : x ∈ s.domain)
:
theorem
NavierStokes.PrimaryMaterialDefect.NativeCoordinates.axialField
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData E}
{d : LinearWaveBounds.GraphDirections E}
{χ : ℕ → E → Slot}
(hχ : NativeCoordinates s d χ)
(n : ℕ)
{x : E}
(hx : x ∈ s.domain)
:
theorem
NavierStokes.PrimaryMaterialDefect.NativeCoordinates.timeField
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData E}
{d : LinearWaveBounds.GraphDirections E}
{χ : ℕ → E → Slot}
(hχ : NativeCoordinates s d χ)
(n : ℕ)
{x : E}
(hx : x ∈ s.domain)
:
(fderiv ℝ (χ n) x) (LinearWaveResidual.timeDirection (s.epsilon n) (d.fastField n) (fun (x : E) => d.slow) x) = PhaseCalculus.eV - s.epsilon n • PhaseCalculus.eT
theorem
NavierStokes.PrimaryMaterialDefect.affine_coordinates
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(s : WeightedClasses.StripData E)
(d : LinearWaveBounds.GraphDirections E)
(L : ℕ → E →L[ℝ] Slot)
(c : ℕ → Slot)
(hr : ∀ (n : ℕ), (L n) d.radial = PhaseCalculus.eR)
(ha : ∀ (n : ℕ), (L n) d.auxiliary = 0)
(hθ : ∀ (n : ℕ), (L n) d.angular = PhaseCalculus.eTheta)
(hz : ∀ (n : ℕ), (L n) d.axial = PhaseCalculus.eZ)
(hf : ∀ (n : ℕ), d.fastScale n • (L n) d.fast = PhaseCalculus.eV)
(ht : ∀ (n : ℕ), (L n) d.slow = PhaseCalculus.eT)
:
NativeCoordinates s d fun (n : ℕ) (x : E) => (L n) x + c n
For affine native/common coordinate maps, checking the six images is linear algebra. No differentiability premise is needed.
structure
NavierStokes.PrimaryMaterialDefect.DirectionMatch
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
(s : WeightedClasses.StripData E)
(d : LinearWaveBounds.GraphDirections E)
(s' : WeightedClasses.StripData E')
(d' : LinearWaveBounds.GraphDirections E')
(ψ : ℕ → E' → E)
:
Differential matching for a change from a common chart to a native chart. It concerns the coordinate map, not the phase or its defect.
- maps (n : ℕ) : Set.MapsTo (ψ n) s'.domain s.domain
Instances For
theorem
NavierStokes.PrimaryMaterialDefect.NativeCoordinates.comp
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{s : WeightedClasses.StripData E}
{d : LinearWaveBounds.GraphDirections E}
{χ : ℕ → E → Slot}
(hχ : NativeCoordinates s d χ)
{s' : WeightedClasses.StripData E'}
{d' : LinearWaveBounds.GraphDirections E'}
{ψ : ℕ → E' → E}
(hψ : DirectionMatch s d s' d' ψ)
:
NativeCoordinates s' d' fun (n : ℕ) => χ n ∘ ψ n
theorem
NavierStokes.PrimaryMaterialDefect.differentiableAt_phase
(ε p pz x0 : ℝ)
(F G : Slow → ℝ)
(q : Slot)
(hF : DifferentiableAt ℝ F q.1)
(hG : DifferentiableAt ℝ G q.1)
:
DifferentiableAt ℝ (PhaseCalculus.phase ε p pz x0 F G) q
noncomputable def
NavierStokes.PrimaryMaterialDefect.expression
(ε p pz x0 v b G FR GR FT GT FZ GZ : ℝ)
:
The algebraic expression after exact material cancellation.
Equations
Instances For
theorem
NavierStokes.PrimaryMaterialDefect.material_pullback
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(χ : E → Slot)
(ε p pz x0 : ℝ)
(b F G : Slow → ℝ)
(Vr Vθ Vz Vf Vs : E → E)
{x : E}
(hχ : DifferentiableAt ℝ χ x)
(hε : ε ≠ 0)
(hR : 0 < (χ x).1.1)
(hF : DifferentiableAt ℝ F (χ x).1)
(hG : DifferentiableAt ℝ G (χ x).1)
(hr : (fderiv ℝ χ x) (Vr x) = PhaseCalculus.eR)
(hθ : (fderiv ℝ χ x) (Vθ x) = PhaseCalculus.eTheta)
(hz : (fderiv ℝ χ x) (Vz x) = ε • PhaseCalculus.eZ)
(hf : (fderiv ℝ χ x) (Vf x) = PhaseCalculus.eV)
(hs : (fderiv ℝ χ x) (Vs x) = PhaseCalculus.eT)
:
LinearWaveResidual.materialPhaseDefect (fun (y : E) => (χ y).1.1) (fun (y : E) => b (χ y).1) (fun (y : E) => F (χ y).1)
(fun (y : E) => G (χ y).1) Vr Vθ Vz (LinearWaveResidual.timeDirection ε Vf Vs)
(PhaseCalculus.phase ε p pz x0 F G ∘ χ) x = expression ε p pz x0 (χ x).2.2 (b (χ x).1) (G (χ x).1) (PhaseCalculus.slowR F (χ x).1) (PhaseCalculus.slowR G (χ x).1)
(PhaseCalculus.slowT F (χ x).1) (PhaseCalculus.slowT G (χ x).1) (PhaseCalculus.slowZ F (χ x).1)
(PhaseCalculus.slowZ G (χ x).1)
A chart pullback of the actual phase has exactly the native backward material derivative, using only the chart differential identities.
theorem
NavierStokes.PrimaryMaterialDefect.expression_class
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData E}
{p pz x0 v b G FR GR FT GT FZ GZ : ℕ → E → ℝ}
(hp : WeightedClasses.UnweightedClass s 0 p)
(hpz : WeightedClasses.UnweightedClass s 0 pz)
(hx0 : WeightedClasses.UnweightedClass s 0 x0)
(hv : WeightedClasses.UnweightedClass s 0 v)
(hb : WeightedClasses.UnweightedClass s 1 b)
(hG : WeightedClasses.UnweightedClass s 0 G)
(hFR : WeightedClasses.UnweightedClass s 0 FR)
(hGR : WeightedClasses.UnweightedClass s 0 GR)
(hFT : WeightedClasses.UnweightedClass s 0 FT)
(hGT : WeightedClasses.UnweightedClass s 0 GT)
(hFZ : WeightedClasses.UnweightedClass s 0 FZ)
(hGZ : WeightedClasses.UnweightedClass s 0 GZ)
:
WeightedClasses.UnweightedClass s 1 fun (n : ℕ) (x : E) =>
expression (s.epsilon n) (p n x) (pz n x) (x0 n x) (v n x) (b n x) (G n x) (FR n x) (GR n x) (FT n x) (GT n x)
(FZ n x) (GZ n x)
Direct class estimate for the exact expression. The six derivatives here are scalar coefficient families; the primary specialization below derives their classes from actual base-field jets.
theorem
NavierStokes.PrimaryMaterialDefect.polynomial_comp_unweighted
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData E}
{U : PhaseJetBounds.Domain ℕ Slow}
{f : ℕ → Slow → ℝ}
(hf : PhaseJetBounds.PolynomialJets U f)
{c : ℕ → E → Slow}
(hc : PhaseJetBounds.PolynomialJets (PrimaryPulseBounds.phaseDomain s) c)
(hscale : ∀ (n : ℕ), U.scale n = s.slow n)
(hmap : ∀ (n : ℕ), Set.MapsTo (c n) s.domain (U.carrier n))
:
WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : E) => f n (c n x)
Polynomial base jets compose with the actual slow coordinate map. The angular coordinate is absent from this quantitative hypothesis.
theorem
NavierStokes.PrimaryMaterialDefect.polynomial_comp_with_edges
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData E}
{U : PhaseJetBounds.Domain ℕ Slow}
{f : ℕ → Slow → ℝ}
(hf : PhaseJetBounds.PolynomialJets U f)
{c : ℕ → E → Slow}
(hc : WeightedClasses.UnweightedClass s 0 c)
(hscale : ∀ (n : ℕ), U.scale n = s.slow n)
(hmap : ∀ (n : ℕ), Set.MapsTo (c n) s.domain (U.carrier n))
:
WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : E) => f n (c n x)
The same composition result allows polynomial inverse-edge losses in the slow chart itself. This is a quantitative chain-rule estimate, not an assumption about the pulled-back base derivatives.
theorem
NavierStokes.PrimaryMaterialDefect.affine_slot_class
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(s : WeightedClasses.StripData E)
(L : ℕ → E →L[ℝ] ℝ)
(c : ℕ → ℝ)
{C : ℝ}
{m : ℕ}
(hC : 1 ≤ C)
(hL : ∀ (n : ℕ), ‖L n‖ ≤ C * s.slow n ^ m)
(hv : ∀ (n : ℕ), ∀ x ∈ s.domain, |(L n) x + c n| ≤ C * s.slow n ^ m)
:
WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : E) => (L n) x + c n
The actual affine clock has polynomial jets from its value and linear coefficient bounds. This supplies the slot-coordinate class in either native or common coordinates.
noncomputable def
NavierStokes.PrimaryMaterialDefect.pulledPhase
{E : Type u_1}
{U : PhaseJetBounds.Domain ℕ Slow}
(P : PrimaryPulseBounds.PhaseConstruction U)
(χ : ℕ → E → Slot)
(n : ℕ)
(x : E)
:
Pulled phase, given by PhaseCalculus.phase (P.phase.epsilon n) (P.phase.p n) (P.phase.pz n) (P.phase.x0 n) (P.phase.F n) (P.phase.G n) (χ n x).
Equations
Instances For
noncomputable def
NavierStokes.PrimaryMaterialDefect.coefficients
{E : Type u_1}
{U : PhaseJetBounds.Domain ℕ Slow}
(P : PrimaryPulseBounds.PhaseConstruction U)
(b : ℕ → Slow → ℝ)
(χ : ℕ → E → Slot)
(amplitude : ℕ → E → HarmonicCalculus.ComplexVector)
(pressure : ℕ → E → ℂ)
(frequency : ℕ → ℝ)
:
Canonical raw geometry with arbitrary amplitude/pressure. Those two
fields do not enter the material defect. The angular base field here is
the frequency F, as required by LinearWaveResidual, not R*F.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.PrimaryMaterialDefect.defect_formula
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{U : PhaseJetBounds.Domain ℕ Slow}
(P : PrimaryPulseBounds.PhaseConstruction U)
(s : WeightedClasses.StripData E)
(d : LinearWaveBounds.GraphDirections E)
(χ : ℕ → E → Slot)
(b : ℕ → Slow → ℝ)
(amplitude : ℕ → E → HarmonicCalculus.ComplexVector)
(pressure : ℕ → E → ℂ)
(frequency : ℕ → ℝ)
(hχ : NativeCoordinates s d χ)
(hmap : ∀ (n : ℕ), Set.MapsTo (fun (x : E) => (χ n x).1) s.domain (U.carrier n))
(heps : ∀ (n : ℕ), P.phase.epsilon n = s.epsilon n)
(n : ℕ)
{x : E}
(hx : x ∈ s.domain)
(hR : 0 < (χ n x).1.1)
:
(coefficients P b χ amplitude pressure frequency).defect s d n x = expression (s.epsilon n) (P.phase.p n) (P.phase.pz n) (P.phase.x0 n) (χ n x).2.2 (b n (χ n x).1)
(P.phase.G n (χ n x).1) (PhaseCalculus.slowR (P.phase.F n) (χ n x).1) (PhaseCalculus.slowR (P.phase.G n) (χ n x).1)
(PhaseCalculus.slowT (P.phase.F n) (χ n x).1) (PhaseCalculus.slowT (P.phase.G n) (χ n x).1)
(PhaseCalculus.slowZ (P.phase.F n) (χ n x).1) (PhaseCalculus.slowZ (P.phase.G n) (χ n x).1)
theorem
NavierStokes.PrimaryMaterialDefect.frozen_classes
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{U : PhaseJetBounds.Domain ℕ Slow}
(P : PrimaryPulseBounds.PhaseConstruction U)
(s : WeightedClasses.StripData E)
:
(WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : E) => P.phase.p n) ∧ (WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : E) => P.phase.pz n) ∧ WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : E) => P.phase.x0 n
theorem
NavierStokes.PrimaryMaterialDefect.defect_class
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{U : PhaseJetBounds.Domain ℕ Slow}
(P : PrimaryPulseBounds.PhaseConstruction U)
(s : WeightedClasses.StripData E)
(d : LinearWaveBounds.GraphDirections E)
(χ : ℕ → E → Slot)
(b : ℕ → Slow → ℝ)
(amplitude : ℕ → E → HarmonicCalculus.ComplexVector)
(pressure : ℕ → E → ℂ)
(frequency : ℕ → ℝ)
(hχ : NativeCoordinates s d χ)
(hslow : PhaseJetBounds.PolynomialJets (PrimaryPulseBounds.phaseDomain s) fun (n : ℕ) (x : E) => (χ n x).1)
(hslot : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : E) => (χ n x).2.2)
(hscale : ∀ (n : ℕ), U.scale n = s.slow n)
(hmap : ∀ (n : ℕ), Set.MapsTo (fun (x : E) => (χ n x).1) s.domain (U.carrier n))
(heps : ∀ (n : ℕ), P.phase.epsilon n = s.epsilon n)
(hR : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 < (χ n x).1.1)
(hb : WeightedClasses.UnweightedClass s 1 fun (n : ℕ) (x : E) => b n (χ n x).1)
:
WeightedClasses.UnweightedClass s 1 ((coefficients P b χ amplitude pressure frequency).defect s d)
Actual all-order defect bounds from base jets and primitive chart data. The six base-derivative classes are derived in the proof.
theorem
NavierStokes.PrimaryMaterialDefect.defect_class_of_mean
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{U : PhaseJetBounds.Domain ℕ Slow}
(P : PrimaryPulseBounds.PhaseConstruction U)
(s : WeightedClasses.StripData E)
(d : LinearWaveBounds.GraphDirections E)
(χ : ℕ → E → Slot)
(b : ℕ → Slow → ℝ)
(amplitude : ℕ → E → HarmonicCalculus.ComplexVector)
(pressure : ℕ → E → ℂ)
(frequency : ℕ → ℝ)
(hχ : NativeCoordinates s d χ)
(hslow : PhaseJetBounds.PolynomialJets (PrimaryPulseBounds.phaseDomain s) fun (n : ℕ) (x : E) => (χ n x).1)
(hslot : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : E) => (χ n x).2.2)
(hscale : ∀ (n : ℕ), U.scale n = s.slow n)
(hmap : ∀ (n : ℕ), Set.MapsTo (fun (x : E) => (χ n x).1) s.domain (U.carrier n))
(heps : ∀ (n : ℕ), P.phase.epsilon n = s.epsilon n)
(hR : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 < (χ n x).1.1)
(hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1)
(hb : WeightedClasses.MeanClass s 1 fun (n : ℕ) (x : E) => b n (χ n x).1)
:
WeightedClasses.UnweightedClass s 1 ((coefficients P b χ amplitude pressure frequency).defect s d)
theorem
NavierStokes.PrimaryMaterialDefect.defect_class_of_fields
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{U : PhaseJetBounds.Domain ℕ Slow}
(P : PrimaryPulseBounds.PhaseConstruction U)
(s : WeightedClasses.StripData E)
(d : LinearWaveBounds.GraphDirections E)
(χ : ℕ → E → Slot)
(b : ℕ → Slow → ℝ)
(a : LinearWaveBounds.WaveCoefficients E)
(hχ : NativeCoordinates s d χ)
(hslow : PhaseJetBounds.PolynomialJets (PrimaryPulseBounds.phaseDomain s) fun (n : ℕ) (x : E) => (χ n x).1)
(hslot : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : E) => (χ n x).2.2)
(hscale : ∀ (n : ℕ), U.scale n = s.slow n)
(hmap : ∀ (n : ℕ), Set.MapsTo (fun (x : E) => (χ n x).1) s.domain (U.carrier n))
(heps : ∀ (n : ℕ), P.phase.epsilon n = s.epsilon n)
(hR : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 < (χ n x).1.1)
(hb : WeightedClasses.UnweightedClass s 1 fun (n : ℕ) (x : E) => b n (χ n x).1)
(hbfield : a.radialBase = fun (n : ℕ) (x : E) => b n (χ n x).1)
(hFfield : a.frequencyBase = fun (n : ℕ) (x : E) => P.phase.F n (χ n x).1)
(hGfield : a.axialBase = fun (n : ℕ) (x : E) => P.phase.G n (χ n x).1)
(hphase : a.phase = pulledPhase P χ)
:
WeightedClasses.UnweightedClass s 1 (a.defect s d)
Field matching binds an existing wave record to the exact phase. It does not assume equality or bounds of its material defect.
theorem
NavierStokes.PrimaryMaterialDefect.finite_jet_bounds
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : WeightedClasses.StripData E}
{f : ℕ → E → ℝ}
(hf : WeightedClasses.UnweightedClass s 1 f)
(m : ℕ)
:
One finite-prefix constant and one polynomial degree work for every band and point. This is the explicit jet form of the order-one class.
Common index, given by ChartScales.nativeIndex h n.
Equations
Instances For
Reconstruction, bundling exponent, inner, outer, inner_lt_outer and the required
compatibility proofs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Operators, constructed using CorrectionState.graphOperators.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
Physical point, given by BaseChartJets.bandPoint h (ChartScales.Q n) (slowCoordinates x).
Equations
Instances For
theorem
NavierStokes.BaseContextAssembly.physicalPoint_time
(h : ℝ)
(n : ℕ)
{x : Point}
(hT : 0 < x.2.1.1)
:
theorem
NavierStokes.BaseContextAssembly.physicalPoint_smooth
(h : ℝ)
(n : ℕ)
:
ContDiff ℝ (↑⊤) (physicalPoint h n)
theorem
NavierStokes.BaseContextAssembly.operators_match_physical
(h a b : ℝ)
(hab : a < b)
(n : ℕ)
:
PhysicalResidualTZ.MatchesAtTZ (operators h a b hab)
(PhysicalResidualBridge.commonGraph (ChartScales.Q n) h (commonIndex h n)) n
theorem
NavierStokes.BaseContextAssembly.radialCoefficient_uniform
(h : ℝ)
(hh : 0 ≤ h)
:
∃ (C : ℝ), 1 ≤ C ∧ ∀ (n : ℕ), ‖ChartScales.radialCoefficient h n‖ ≤ C * ChartScales.epsilon h n ^ (-ChartScales.kappa)
noncomputable def
NavierStokes.BaseContextAssembly.movingStrip
{h : ℝ}
(hh : 0 ≤ h)
(U : LocalSignedRequest.SlowRegion (2 * h))
(a b cL cR : ℝ)
(ha : 0 < a)
(hcL : 0 < cL)
(hcR : 0 < cR)
:
Moving strip, constructed using LocalSignedRequest.movingStripData.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.BaseContextAssembly.positive_radial_unweighted
{s : WeightedClasses.StripData Point}
{a b : ℝ}
(ha : 0 < a)
(hr : ∀ x ∈ s.domain, x.1 ∈ Set.Icc a b)
{g : ℝ → ℝ}
(hg : ContDiffOn ℝ (↑⊤) g (Set.Ioi 0))
:
WeightedClasses.UnweightedClass s 0 fun (x : ℕ) (x_1 : Point) => g x_1.1
theorem
NavierStokes.BaseContextAssembly.movingStrip_radial_bounds
{h : ℝ}
(hh : 0 ≤ h)
(U : LocalSignedRequest.SlowRegion (2 * h))
(a b cL cR : ℝ)
(ha : 0 < a)
(hcL : 0 < cL)
(hcR : 0 < cR)
{x : Point}
(hx : x ∈ (movingStrip hh U a b cL cR ha hcL hcR).domain)
:
theorem
NavierStokes.BaseContextAssembly.operators_local
{h a b : ℝ}
(hab : a < b)
(U : Set Plane)
:
LocalRankDefect.LocalOperators U (operators h a b hab)
theorem
NavierStokes.BaseContextAssembly.operator_bounds
{h : ℝ}
(hh : 0 ≤ h)
(U : LocalSignedRequest.SlowRegion (2 * h))
{a b cL cR : ℝ}
(ha : 0 < a)
(hab : a < b)
(hcL : 0 < cL)
(hcR : 0 < cR)
:
MeanIncrementBounds.OperatorBounds (movingStrip hh U a b cL cR ha hcL hcR) (operators h a b hab) ChartScales.kappa
noncomputable def
NavierStokes.BaseContextAssembly.nativeStrip
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
:
Native strip, constructed using movingStrip.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.BaseContextAssembly.nativeStrip_mem
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
(x : Point)
:
x ∈ (nativeStrip W U).domain ↔ x.2.1 ∈ U.carrier ∧ PrimaryTargetBounds.profileRadius F.data.h (slowCoordinates x) ∈ Set.Ioo (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W)
theorem
NavierStokes.BaseContextAssembly.nativeStrip_radius
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
{x : Point}
(hx : x ∈ (nativeStrip W U).domain)
:
theorem
NavierStokes.BaseContextAssembly.nativeStrip_time
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
{x : Point}
(hx : x ∈ (nativeStrip W U).domain)
:
theorem
NavierStokes.BaseContextAssembly.nativeStrip_active
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
{x : Point}
(hx : x ∈ (nativeStrip W U).domain)
:
theorem
NavierStokes.BaseContextAssembly.nativeStrip_weight
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
{x : Point}
(hx : x ∈ (nativeStrip W U).domain)
:
(nativeStrip W U).zeta x = FinalSlowBase.weight W (BaseChartJets.normalizedCoordinates F.data.h (slowCoordinates x)).2
noncomputable def
NavierStokes.BaseContextAssembly.slowCarrier
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
:
Slow carrier, given by insertSlow ⁻¹' (nativeStrip W U).domain.
Equations
Instances For
theorem
NavierStokes.BaseContextAssembly.slowCarrier_open
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
:
IsOpen (slowCarrier W U)
noncomputable def
NavierStokes.BaseContextAssembly.phaseDomain
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
(ι : Type u_1)
:
Phase domain, given by BaseChartJets.oneDomain ι (fun _ => slowCarrier W U) (fun _ => slowCarrier_open W U).
Equations
- NavierStokes.BaseContextAssembly.phaseDomain W U ι = NavierStokes.BaseChartJets.oneDomain ι (fun (x : ι) => NavierStokes.BaseContextAssembly.slowCarrier W U) ⋯
Instances For
theorem
NavierStokes.BaseContextAssembly.slowCoordinates_maps
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
:
Set.MapsTo (⇑slowCoordinates) (nativeStrip W U).domain (slowCarrier W U)
noncomputable def
NavierStokes.BaseContextAssembly.geometryRadius
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
:
Geometry radius, given by Real.sqrt U.qlo * PrimaryTargetBounds.leftRadius W.
Equations
Instances For
noncomputable def
NavierStokes.BaseContextAssembly.geometryUpper
{F : OutgoingProfile.Profile}
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
:
Geometry upper, given by max 1 U.qhi + 1.
Equations
Instances For
noncomputable def
NavierStokes.BaseContextAssembly.geometryBound
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
:
Geometry bound, constructed using max.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.BaseContextAssembly.geometryRadius_pos
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
:
theorem
NavierStokes.BaseContextAssembly.geometryUpper_pos
{F : OutgoingProfile.Profile}
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
:
theorem
NavierStokes.BaseContextAssembly.one_le_geometryBound
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
:
theorem
NavierStokes.BaseContextAssembly.native_geometry
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
(ι : Type u_1)
:
BaseChartJets.GeometryBounds (phaseDomain W U ι) F.data.h (geometryRadius W U) (geometryBound W U) (U.qlo / 2)
(geometryUpper U) (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W)
theorem
NavierStokes.BaseContextAssembly.unweighted_polynomial_pullback
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(s : WeightedClasses.StripData Point)
{D : PhaseJetBounds.Domain ℕ Slow}
{f : ℕ → Slow → E}
(hf : PhaseJetBounds.PolynomialJets (BaseChartJets.unitScale D) f)
(hmap : ∀ (n : ℕ), Set.MapsTo (⇑slowCoordinates) s.domain (D.carrier n))
:
WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : Point) => f n (slowCoordinates x)
theorem
NavierStokes.BaseContextAssembly.envelope_pullback
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(s : WeightedClasses.StripData Point)
{D : PhaseJetBounds.Domain ℕ Slow}
{f : ℕ → Slow → E}
{w : ℕ → ℝ}
(hf : PrimaryPulseBounds.EnvelopeJets (BaseChartJets.unitScale D) (fun (n : ℕ) (x : Slow) => w n) f)
(hmap : ∀ (n : ℕ), Set.MapsTo (⇑slowCoordinates) s.domain (D.carrier n))
{alpha : ℝ}
(hw : ∀ (n : ℕ), w n = s.epsilon n ^ alpha)
:
WeightedClasses.UnweightedClass s alpha fun (n : ℕ) (x : Point) => f n (slowCoordinates x)
noncomputable def
NavierStokes.BaseContextAssembly.radialBase
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B n : ℕ)
(x : Point)
:
Radial base, given by ChartScales.Q n ^ CoordinateAlgebra.A F.data.h * FinalSlowBase.velocity H v upper B (physicalPoint F.data.h n x) 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.BaseContextAssembly.frequencyBase
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B n : ℕ)
(x : Point)
:
Frequency base, constructed using BaseChartJets.frequency.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.BaseContextAssembly.axialBase
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B n : ℕ)
(x : Point)
:
Axial base, constructed using BaseChartJets.axial.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.BaseContextAssembly.base
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
:
Base, bundling radial, angular, axial.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.BaseContextAssembly.rawStress
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B n : ℕ)
(x : Point)
:
Raw stress as an element of ℝ × ℝ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.BaseContextAssembly.virtualStress
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B n : ℕ)
(x : Point)
:
The physical stress on positive radius, extended by zero to the other half-line. Its actual inner zero region makes this extension smooth.
Equations
- NavierStokes.BaseContextAssembly.virtualStress H v upper B n x = if 0 < x.1 then NavierStokes.BaseContextAssembly.rawStress H v upper B n x else 0
Instances For
@[simp]
theorem
NavierStokes.BaseContextAssembly.virtualStress_eq_raw
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B n : ℕ)
{x : Point}
(hR : 0 < x.1)
:
@[simp]
theorem
NavierStokes.BaseContextAssembly.virtualStress_eq_zero
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B n : ℕ)
{x : Point}
(hR : x.1 ≤ 0)
:
noncomputable def
NavierStokes.BaseContextAssembly.context
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(a b : ℝ)
(hab : a < b)
:
Context, bundling operators, base, virtualTheta, virtualAxial.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.BaseContextAssembly.axialBase_physical
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B n : ℕ)
{x : Point}
(hT : 0 < x.2.1.1)
:
axialBase H v upper B n x = ChartScales.Q n ^ CoordinateAlgebra.A F.data.h * (FinalSlowBase.velocity H v upper B (physicalPoint F.data.h n x)).ofLp 2
theorem
NavierStokes.BaseContextAssembly.angularBase_physical
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B n : ℕ)
{x : Point}
(hT : 0 < x.2.1.1)
(hR : 0 < x.1)
:
(base H v upper B).angular n x = ChartScales.Q n ^ CoordinateAlgebra.A F.data.h * (FinalSlowBase.velocity H v upper B (physicalPoint F.data.h n x)).ofLp 1
theorem
NavierStokes.BaseContextAssembly.physicalComponent_smoothAt
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B n : ℕ)
(i : Fin 3)
{x : Point}
(hT : 0 < x.2.1.1)
:
ContDiffAt ℝ (↑⊤)
(fun (y : Point) =>
ChartScales.Q n ^ CoordinateAlgebra.A F.data.h * (FinalSlowBase.velocity H v upper B (physicalPoint F.data.h n y)).ofLp i)
x
theorem
NavierStokes.BaseContextAssembly.base_smooth
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(U : Set Plane)
(hT : ∀ p ∈ U, 0 < p.1)
:
MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U) (base H v upper B)
theorem
NavierStokes.BaseContextAssembly.native_estimates
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
:
BaseChartJets.Estimates (phaseDomain W U ℕ) ChartScales.Q (FinalSlowBase.scales H v upper B) F.data.h
W.axis.normalization (FinalSlowBase.coefficients H v)
theorem
NavierStokes.BaseContextAssembly.frequencyBase_unweighted
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
:
WeightedClasses.UnweightedClass (nativeStrip W U) 0 (frequencyBase H v upper B)
theorem
NavierStokes.BaseContextAssembly.axialBase_unweighted
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
:
WeightedClasses.UnweightedClass (nativeStrip W U) 0 (axialBase H v upper B)
theorem
NavierStokes.BaseContextAssembly.radialBase_unweighted
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
:
WeightedClasses.UnweightedClass (nativeStrip W U) 1 (radialBase H v upper B)
theorem
NavierStokes.BaseContextAssembly.base_bounds
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
:
MeanIncrementBounds.BaseBounds (nativeStrip W U) (base H v upper B)
theorem
NavierStokes.BaseContextAssembly.rawStress_smooth
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(U : Set Plane)
(hT : ∀ p ∈ U, 0 < p.1)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) (rawStress H v upper B n) (PhysicalMeanDomain.slowDomain U)
theorem
NavierStokes.BaseContextAssembly.rawStress_periodic
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(U : Set Plane)
(n : ℕ)
:
(PhysicalMeanDomain.PeriodicOn U fun (x : PressureStream.Lift Plane) => (rawStress H v upper B n x).1) ∧ PhysicalMeanDomain.PeriodicOn U fun (x : PressureStream.Lift Plane) => (rawStress H v upper B n x).2
theorem
NavierStokes.BaseContextAssembly.rawStress_normalized
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B n : ℕ)
{x : Point}
(hT : 0 < x.2.1.1)
:
rawStress H v upper B n x = (ChartScales.epsilon F.data.h n * (BaseChartJets.normalizedCoordinates F.data.h (slowCoordinates x)).1 ^ (-CoordinateAlgebra.A F.data.h - 1 / 2)) • FinalSlowBase.normalizedStress H v upper B
((SlowBorelBase.scaleMap (ChartScales.Q n)) (BaseChartJets.normalizedCoordinates F.data.h (slowCoordinates x)))
theorem
NavierStokes.BaseContextAssembly.rawStress_zero_inner
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B n : ℕ)
{x : Point}
(hT : 0 < x.2.1.1)
(hX : (BaseChartJets.normalizedCoordinates F.data.h (slowCoordinates x)).2.1 ≤ NominalConeAssembly.activeLeft W)
:
theorem
NavierStokes.BaseContextAssembly.rawStress_zero_near_axis
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B n : ℕ)
{x : Point}
(hT : 0 < x.2.1.1)
(hR : x.1 = 0)
:
theorem
NavierStokes.BaseContextAssembly.virtualStress_smooth
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(U : Set Plane)
(hT : ∀ p ∈ U, 0 < p.1)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) (virtualStress H v upper B n) (PhysicalMeanDomain.slowDomain U)
theorem
NavierStokes.BaseContextAssembly.virtualStress_periodic
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(U : Set Plane)
(n : ℕ)
:
(PhysicalMeanDomain.PeriodicOn U fun (x : PressureStream.Lift Plane) => (virtualStress H v upper B n x).1) ∧ PhysicalMeanDomain.PeriodicOn U fun (x : PressureStream.Lift Plane) => (virtualStress H v upper B n x).2
theorem
NavierStokes.BaseContextAssembly.virtualStress_normalized
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B n : ℕ)
{x : Point}
(hT : 0 < x.2.1.1)
(hR : 0 < x.1)
:
virtualStress H v upper B n x = (ChartScales.epsilon F.data.h n * (BaseChartJets.normalizedCoordinates F.data.h (slowCoordinates x)).1 ^ (-CoordinateAlgebra.A F.data.h - 1 / 2)) • FinalSlowBase.normalizedStress H v upper B
((SlowBorelBase.scaleMap (ChartScales.Q n)) (BaseChartJets.normalizedCoordinates F.data.h (slowCoordinates x)))
theorem
NavierStokes.BaseContextAssembly.virtualStress_support
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
(n : ℕ)
{x : Point}
(hx : x.2.1 ∈ U.carrier)
(hn : virtualStress H v upper B n x ≠ 0)
:
(LocalSignedRequest.profileMap (2 * F.data.h) x).1 ∈ Set.Icc (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W)
theorem
NavierStokes.BaseContextAssembly.virtualStress_movingSupport
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
(n : ℕ)
:
(LocalSignedRequest.MovingSupport (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W) (2 * F.data.h)
U.carrier fun (x : LocalSignedRequest.Point) => (virtualStress H v upper B n x).1) ∧ LocalSignedRequest.MovingSupport (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W) (2 * F.data.h)
U.carrier fun (x : LocalSignedRequest.Point) => (virtualStress H v upper B n x).2
noncomputable def
NavierStokes.BaseContextAssembly.leadingVirtualStress
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(n : ℕ)
(x : Point)
:
Leading virtual stress, with branches according to 0 < x.1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.BaseContextAssembly.leadingVirtualStress_eq
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(n : ℕ)
{x : Point}
(hT : 0 < x.2.1.1)
(hR : 0 < x.1)
:
leadingVirtualStress H v n x = (ChartScales.epsilon F.data.h n * (BaseChartJets.normalizedCoordinates F.data.h (slowCoordinates x)).1 ^ (-CoordinateAlgebra.A F.data.h - 1 / 2)) • FinalSlowBase.leadingStress v (BaseChartJets.normalizedCoordinates F.data.h (slowCoordinates x)).2
noncomputable def
NavierStokes.BaseContextAssembly.waveCoefficients
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(phase : ℕ → Point × ℝ → ℝ)
(amplitude : ℕ → Point × ℝ → HarmonicCalculus.ComplexVector)
(pressure : ℕ → Point × ℝ → ℂ)
(frequency : ℕ → ℝ)
:
Wave coefficients, bundling radius, radialBase, frequencyBase, axialBase and the
required compatibility proofs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.BaseContextAssembly.waveCoefficients_match
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
{a b cL cR : ℝ}
(ha : 0 < a)
(hab : a < b)
(hcL : 0 < cL)
(hcR : 0 < cR)
(phase : ℕ → Point × ℝ → ℝ)
(amplitude : ℕ → Point × ℝ → HarmonicCalculus.ComplexVector)
(pressure : ℕ → Point × ℝ → ℂ)
(frequency : ℕ → ℝ)
:
PrimaryResidualClass.Matches (movingStrip ⋯ U a b cL cR ha hcL hcR) (context H v upper B a b hab)
(waveCoefficients H v upper B phase amplitude pressure frequency)
noncomputable def
NavierStokes.BaseContextAssembly.radialSlow
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B n : ℕ)
(p : Slow)
:
Radial slow, constructed using BaseRadialJets.radial.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.BaseContextAssembly.frequencySlow
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B n : ℕ)
:
Frequency slow, constructed using BaseChartJets.frequency.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.BaseContextAssembly.axialSlow
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B n : ℕ)
:
Axial slow, given by BaseChartJets.axial (FinalSlowBase.scales H v upper B) F.data.h (FinalSlowBase.coefficients H v) (ChartScales.Q n).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.BaseContextAssembly.radialSlow_pullback
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B n : ℕ)
(x : Point)
:
theorem
NavierStokes.BaseContextAssembly.radialBase_stream
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B n : ℕ)
{x : Point}
(hT : 0 < x.2.1.1)
:
radialBase H v upper B n x = -(ChartScales.epsilon F.data.h n * x.1 / 2) * PhaseCalculus.slowZ
(BaseRadialJets.normalizedStream (FinalSlowBase.scales H v upper B) F.data.h (FinalSlowBase.coefficients H v)
(ChartScales.Q n))
(slowCoordinates x)
theorem
NavierStokes.BaseContextAssembly.radialSlow_smoothAt
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B n : ℕ)
{p : Slow}
(hp : 0 < p.2.2)
:
ContDiffAt ℝ (↑⊤) (radialSlow H v upper B n) p
noncomputable def
NavierStokes.BaseContextAssembly.nativeCoordinates
(clock : ℕ → Point → ℝ)
(n : ℕ)
(x : Point × ℝ)
:
The slot clock can vary with the native construction. Its slow and angular coordinates stay literal, so no phase estimate enters the binding.
Equations
- NavierStokes.BaseContextAssembly.nativeCoordinates clock n x = (NavierStokes.BaseContextAssembly.slowCoordinates x.1, x.2, clock n x.1)
Instances For
theorem
NavierStokes.BaseContextAssembly.primaryCoefficients_match
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
{D : PhaseJetBounds.Domain ℕ Slow}
(P : PrimaryPulseBounds.PhaseConstruction D)
(hF : P.phase.F = frequencySlow H v upper B)
(hG : P.phase.G = axialSlow H v upper B)
(chi : ℕ → Point × ℝ → PhaseCalculus.Slot)
(hchi : ∀ (n : ℕ) (x : Point × ℝ), (chi n x).1 = slowCoordinates x.1)
(amplitude : ℕ → Point × ℝ → HarmonicCalculus.ComplexVector)
(pressure : ℕ → Point × ℝ → ℂ)
(frequency : ℕ → ℝ)
:
PrimaryResidualClass.Matches (nativeStrip W U)
(context H v upper B (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W) ⋯)
(PrimaryMaterialDefect.coefficients P (radialSlow H v upper B) chi amplitude pressure frequency)
theorem
NavierStokes.BaseContextAssembly.nativeCoefficients_match
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
{D : PhaseJetBounds.Domain ℕ Slow}
(P : PrimaryPulseBounds.PhaseConstruction D)
(hF : P.phase.F = frequencySlow H v upper B)
(hG : P.phase.G = axialSlow H v upper B)
(clock : ℕ → Point → ℝ)
(amplitude : ℕ → Point × ℝ → HarmonicCalculus.ComplexVector)
(pressure : ℕ → Point × ℝ → ℂ)
(frequency : ℕ → ℝ)
:
PrimaryResidualClass.Matches (nativeStrip W U)
(context H v upper B (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W) ⋯)
(PrimaryMaterialDefect.coefficients P (radialSlow H v upper B) (nativeCoordinates clock) amplitude pressure frequency)
theorem
NavierStokes.BaseContextAssembly.radialSlow_productClass
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
(chi : ℕ → Point × ℝ → PhaseCalculus.Slot)
(hchi : ∀ (n : ℕ) (x : Point × ℝ), (chi n x).1 = slowCoordinates x.1)
:
WeightedClasses.UnweightedClass (HarmonicWaveInteraction.productStrip (nativeStrip W U)) 1
fun (n : ℕ) (x : Point × ℝ) => radialSlow H v upper B n (chi n x).1
noncomputable def
NavierStokes.BaseContextAssembly.nativeContext
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
:
Native context, given by context H v upper B (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W) (PrimaryTargetBounds.radii_ordered W).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.BaseContextAssembly.native_operator_bounds
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
:
MeanIncrementBounds.OperatorBounds (nativeStrip W U) (nativeContext H v upper B).operators ChartScales.kappa
theorem
NavierStokes.BaseContextAssembly.native_base_bounds
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
:
MeanIncrementBounds.BaseBounds (nativeStrip W U) (nativeContext H v upper B).base
theorem
NavierStokes.BaseContextAssembly.native_operators_local
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(U : Set Plane)
:
LocalRankDefect.LocalOperators U (nativeContext H v upper B).operators
theorem
NavierStokes.BaseContextAssembly.native_base_smooth
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
:
MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U.carrier) (nativeContext H v upper B).base
theorem
NavierStokes.BaseContextAssembly.native_radial_isSlow
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(U : Set Plane)
:
LocalRankDefect.IsSlowOn U (nativeContext H v upper B).base.radial
theorem
NavierStokes.BaseContextAssembly.native_angular_isSlow
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(U : Set Plane)
:
LocalRankDefect.IsSlowOn U (nativeContext H v upper B).base.angular
theorem
NavierStokes.BaseContextAssembly.native_axial_isSlow
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(U : Set Plane)
:
LocalRankDefect.IsSlowOn U (nativeContext H v upper B).base.axial
theorem
NavierStokes.BaseContextAssembly.native_matches_physical
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B n : ℕ)
:
PhysicalResidualTZ.MatchesAtTZ (nativeContext H v upper B).operators
(PhysicalResidualBridge.commonGraph (ChartScales.Q n) F.data.h (commonIndex F.data.h n)) n
theorem
NavierStokes.BaseContextAssembly.native_stress_properties
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(U : LocalSignedRequest.SlowRegion (2 * F.data.h))
(n : ℕ)
:
ContDiffOn ℝ (↑⊤)
(fun (x : Point) => ((nativeContext H v upper B).virtualTheta n x, (nativeContext H v upper B).virtualAxial n x))
(PhysicalMeanDomain.slowDomain U.carrier) ∧ PhysicalMeanDomain.PeriodicOn U.carrier ((nativeContext H v upper B).virtualTheta n) ∧ PhysicalMeanDomain.PeriodicOn U.carrier ((nativeContext H v upper B).virtualAxial n) ∧ LocalSignedRequest.MovingSupport (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W)
(2 * F.data.h) U.carrier ((nativeContext H v upper B).virtualTheta n) ∧ LocalSignedRequest.MovingSupport (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W)
(2 * F.data.h) U.carrier ((nativeContext H v upper B).virtualAxial n)
Constructed context, given by nativeContext FinalSlowBase.actualProfile.certificate FinalSlowBase.actualProfile.modulation upper B.
Equations
Instances For
theorem
NavierStokes.BaseContextAssembly.constructed_context_bounds
(upper : ℝ)
(B : ℕ)
(U : LocalSignedRequest.SlowRegion (2 * FinalSlowBase.actualProfile.outgoing.data.h))
:
MeanIncrementBounds.OperatorBounds (nativeStrip FinalSlowBase.actualProfile.nominal U)
(constructedContext upper B).operators ChartScales.kappa ∧ MeanIncrementBounds.BaseBounds (nativeStrip FinalSlowBase.actualProfile.nominal U) (constructedContext upper B).base ∧ LocalRankDefect.LocalOperators U.carrier (constructedContext upper B).operators ∧ MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U.carrier) (constructedContext upper B).base