Base estimates imply the actual pulse geometry #
The inputs concern normalized base fields and frozen representative data. Normal, damping, and moving-basis errors are conclusions. The dyadic cutoff is chosen after all fixed constants and before the band or slow point.
Zeroth-order bounds for the actual primary covariance #
The covariance is the same normalized-slot integral used by
PrimaryPulseBounds. Compact model cone margins, actual Gaussian pulse
integrals, and the native chart scales produce the determinant and inverse
weight bounds. Flat target weights are retained as factors.
@[reducible, inline]
Datum type used in primary covariance bounds.
Equations
Instances For
@[instance_reducible]
Use the entrywise matrix norm inherited from the finite function space.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[instance_reducible]
Scalar multiplication is the pointwise real vector-space structure on matrices.
Equations
Instances For
theorem
NavierStokes.PrimaryCovarianceBounds.compact_model_margins
{X : Type u_1}
[TopologicalSpace X]
{K : Set X}
(hK : IsCompact K)
(H0 : X → Mat2)
(T0 : X → Vec2)
(hH0 : ∀ (i j : Fin 2), ContinuousOn (fun (p : X) => H0 p i j) K)
(hT0 : ∀ (i : Fin 2), ContinuousOn (fun (p : X) => T0 p i) K)
(hcone : ∀ p ∈ K, SmoothCovariance.StrictCone (H0 p) (T0 p))
:
The same compact model cone supplies quantitative margins for every nearby actual matrix, without assuming continuity of the competing family.
theorem
NavierStokes.PrimaryCovarianceBounds.normalized_columns
(R : ℝ)
(H : Mat2)
(c : Vec2)
:
PrimaryPulseBounds.normalizedMatrix R (FlatCovariance.columns H c) = FlatCovariance.columns H fun (j : Fin 2) => R * c j
theorem
NavierStokes.PrimaryCovarianceBounds.column_scale_bounds
(H : Mat2)
(T c : Vec2)
{R lo hi delta M zeta : ℝ}
(hR : 0 < R)
(hlo : 0 < lo)
(hhi : 0 < hi)
(hdelta : 0 < delta)
(hzeta : 0 ≤ zeta)
(hc : ∀ (j : Fin 2), lo ≤ R * c j ∧ R * c j ≤ hi)
(hdet : delta ≤ |Matrix.det H|)
(hw : ∀ (j : Fin 2), delta ≤ SmoothCovariance.weights H T j)
(hentry : ∀ (i j : Fin 2), |H i j| ≤ M)
:
lo ^ 2 * delta ≤ |Matrix.det (PrimaryPulseBounds.normalizedMatrix R (FlatCovariance.columns H c))| ∧ (∀ (i j : Fin 2), |R * FlatCovariance.columns H c i j| ≤ hi * M) ∧ ∀ (j : Fin 2),
delta / hi * R * zeta ≤ SmoothCovariance.weights (FlatCovariance.columns H c) (FlatCovariance.scaledTarget zeta T) j
Column factors of size 1/R turn the model margins into an actual
normalized determinant gap and an inverse lower bound proportional to
R*zeta. No positive minimum of the flat factor is used.
Native chart scale and the positive scalar column sizes #
theorem
NavierStokes.PrimaryCovarianceBounds.slotLength_pos
{r0 : ℝ}
(hr0 : 0 < r0)
(h : ℝ)
(n : ℕ)
:
theorem
NavierStokes.PrimaryCovarianceBounds.slotRadius_pos
{r0 : ℝ}
(hr0 : 0 < r0)
(h : ℝ)
(n : ℕ)
:
theorem
NavierStokes.PrimaryCovarianceBounds.slotRadius_sq
{r0 : ℝ}
(hr0 : 0 < r0)
(h : ℝ)
(n : ℕ)
:
theorem
NavierStokes.PrimaryCovarianceBounds.chart_scalar_factor_bounds
{r0 h : ℝ}
(hr0 : 0 < r0)
(hh : 0 ≤ h)
{n : ℕ}
(hn : 4 ≤ n)
:
√(2 * r0 / ChartScales.Tg) ≤ √(ChartScales.S n) * ChartScales.timeCoefficient h n * slotRadius r0 h n ∧ √(ChartScales.S n) * ChartScales.timeCoefficient h n * slotRadius r0 h n ≤ √(2 * r0)
Scalar lower, given by kappa * PulseCovariance.PulseBounds.lowerMassConstant a B * Real.sqrt (2 * r0 / ChartScales.Tg).
Equations
- NavierStokes.PrimaryCovarianceBounds.scalarLower kappa r0 a B = kappa * NavierStokes.PulseCovariance.PulseBounds.lowerMassConstant a B * √(2 * r0 / NavierStokes.ChartScales.Tg)
Instances For
theorem
NavierStokes.PrimaryCovarianceBounds.scalarLower_pos
{kappa r0 a B : ℝ}
(hkappa : 0 < kappa)
(hr0 : 0 < r0)
(ha : 0 < a)
:
theorem
NavierStokes.PrimaryCovarianceBounds.chart_column_mass_bounds
{r0 h kappa a A b B : ℝ}
(hr0 : 0 < r0)
(hh : 0 ≤ h)
(hkappa : 0 < kappa)
{n : ℕ}
(hn : 4 ≤ n)
{psi x : ℝ → ℝ}
(hp : PulseCovariance.PulseBounds (slotRadius r0 h n) a A b B psi x)
:
scalarLower kappa r0 a B ≤ √(ChartScales.S n) * (kappa * ChartScales.timeCoefficient h n * PulseCovariance.mass psi x) ∧ √(ChartScales.S n) * (kappa * ChartScales.timeCoefficient h n * PulseCovariance.mass psi x) ≤ scalarUpper kappa r0 A b
The actual pair matrix #
noncomputable def
NavierStokes.PrimaryCovarianceBounds.normalizedPair
(P : Fin 2 → PartitionedCovariance.Pulse)
:
Normalized pair, defined pointwise by PulseCovariance.normalizedColumn (P j).ψ (P j).x (P j).t i.
Equations
- NavierStokes.PrimaryCovarianceBounds.normalizedPair P i j = NavierStokes.PulseCovariance.normalizedColumn (P j).ψ (P j).x (P j).t i
Instances For
noncomputable def
NavierStokes.PrimaryCovarianceBounds.pairScales
(kappa : ℝ)
(ci : Vec2)
(P : Fin 2 → PartitionedCovariance.Pulse)
:
Pair scales, defined pointwise by kappa * ci j * PulseCovariance.mass (P j).ψ (P j).x.
Equations
- NavierStokes.PrimaryCovarianceBounds.pairScales kappa ci P j = kappa * ci j * NavierStokes.PulseCovariance.mass (P j).ψ (P j).x
Instances For
theorem
NavierStokes.PrimaryCovarianceBounds.pairMatrix_factorization
{r a A b B : ℝ}
(P : Fin 2 → PartitionedCovariance.Pulse)
(hP : ∀ (j : Fin 2), PulseCovariance.PulseBounds r a A b B (P j).ψ (P j).x)
(vr vt : TorusInverse.Plane)
(r0 : ℝ)
(ci : Vec2)
:
PartitionedCovariance.pairMatrix vr vt r0 ci P = FlatCovariance.columns (normalizedPair P) (pairScales (PartitionedCovariance.nativePrefactor vr vt r0) ci P)
theorem
NavierStokes.PrimaryCovarianceBounds.normalizedPair_entry_error
{r a A b B E D : ℝ}
(P : Fin 2 → PartitionedCovariance.Pulse)
(hP : ∀ (j : Fin 2), PulseCovariance.PulseBounds r a A b B (P j).ψ (P j).x)
(H0 : Mat2)
(hE : 0 ≤ E)
(hD : 0 ≤ D)
(hratio :
∀ (j i : Fin 2),
∀ v ∈ Set.Icc 0 (r ^ 2), |(P j).t v i / (P j).x v - H0 i j| ≤ E / r ^ 2 + D * |v - r ^ 2 / 2| / r ^ 2)
(i j : Fin 2)
:
structure
NavierStokes.PrimaryCovarianceBounds.ZeroOrderBounds
(R detGap entryBound inverseLower zeta : ℝ)
(H : Mat2)
(T : Vec2)
:
Precisely the zeroth-order inputs used by PrimaryPulseBounds, with
the stronger inverse lower bound retaining the factor R.
Instances For
theorem
NavierStokes.PrimaryCovarianceBounds.ZeroOrderBounds.weight_lower
{R detGap entryBound inverseLower zeta : ℝ}
{H : Mat2}
{T : Vec2}
(h : ZeroOrderBounds R detGap entryBound inverseLower zeta H T)
(hR : 1 ≤ R)
(ha : 0 ≤ inverseLower)
(hzeta : 0 ≤ zeta)
(j : Fin 2)
:
theorem
NavierStokes.PrimaryCovarianceBounds.ZeroOrderBounds.det_ne_zero
{R detGap entryBound inverseLower zeta : ℝ}
{H : Mat2}
{T : Vec2}
(h : ZeroOrderBounds R detGap entryBound inverseLower zeta H T)
(hgap : 0 < detGap)
:
theorem
NavierStokes.PrimaryCovarianceBounds.ZeroOrderBounds.weights_pos
{R detGap entryBound inverseLower zeta : ℝ}
{H : Mat2}
{T : Vec2}
(h : ZeroOrderBounds R detGap entryBound inverseLower zeta H T)
(hR : 0 < R)
(ha : 0 < inverseLower)
(hzeta : 0 < zeta)
(j : Fin 2)
:
theorem
NavierStokes.PrimaryCovarianceBounds.ZeroOrderBounds.strictCone
{R detGap entryBound inverseLower zeta : ℝ}
{H : Mat2}
{T : Vec2}
(h : ZeroOrderBounds R detGap entryBound inverseLower zeta H T)
(hR : 0 < R)
(ha : 0 < inverseLower)
(hzeta : 0 < zeta)
:
theorem
NavierStokes.PrimaryCovarianceBounds.ZeroOrderBounds.primary_weight_lower
{n : ℕ}
{detGap entryBound inverseLower zeta : ℝ}
{H : Mat2}
{T : Vec2}
(h : ZeroOrderBounds (√(ChartScales.S n)) detGap entryBound inverseLower zeta H T)
(hn : 1 ≤ n)
(ha : 0 ≤ inverseLower)
(hzeta : 0 ≤ zeta)
(j : Fin 2)
:
The weaker inverse bound required by the square-root jet theorem is an immediate consequence, without losing the flat target factor.
theorem
NavierStokes.PrimaryCovarianceBounds.compact_chart_pair_bounds
{X : Type u_1}
[TopologicalSpace X]
{K : Set X}
(hK : IsCompact K)
(H0 : X → Mat2)
(T0 : X → Vec2)
(hH0 : ∀ (i j : Fin 2), ContinuousOn (fun (p : X) => H0 p i j) K)
(hT0 : ∀ (i : Fin 2), ContinuousOn (fun (p : X) => T0 p i) K)
(hcone : ∀ p ∈ K, SmoothCovariance.StrictCone (H0 p) (T0 p))
(vr vt : TorusInverse.Plane)
(hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0)
{r0 h a A b B E D : ℝ}
(hr0 : 0 < r0)
(hh : 0 ≤ h)
(ha : 0 < a)
(hA : 0 < A)
(hb : 0 < b)
(hE : 0 ≤ E)
(hD : 0 ≤ D)
:
∃ (N : ℕ),
4 ≤ N ∧ ∃ (detGap : ℝ) (entryBound : ℝ) (inverseLower : ℝ),
0 < detGap ∧ 1 ≤ entryBound ∧ 0 < inverseLower ∧ ∀ (n : ℕ),
N ≤ n →
∀ p ∈ K,
∀ (P : Fin 2 → PartitionedCovariance.Pulse),
(∀ (j : Fin 2), PulseCovariance.PulseBounds (slotRadius r0 h n) a A b B (P j).ψ (P j).x) →
(∀ (j i : Fin 2),
∀ v ∈ Set.Icc 0 (ChartScales.slotLength r0 h n),
|(P j).t v i / (P j).x v - H0 p i j| ≤ E / ChartScales.slotLength r0 h n + D * |v - ChartScales.slotLength r0 h n / 2| / ChartScales.slotLength r0 h n) →
∀ (zeta : ℝ),
0 ≤ zeta →
ZeroOrderBounds (√(ChartScales.S n)) detGap entryBound inverseLower zeta
(PartitionedCovariance.pairMatrix vr vt r0
(fun (x : Fin 2) => ChartScales.timeCoefficient h n) P)
(FlatCovariance.scaledTarget zeta (T0 p))
For the actual native pair, all uniform zeroth-order constants are chosen before the band. Only pointwise pulse and normalized-direction estimates are inputs; no integrated matrix margin is assumed.
Uniform constants for the actual reference envelopes #
theorem
NavierStokes.PrimaryCovarianceBounds.compact_reference_bounds
{X : Type u_1}
[TopologicalSpace X]
{K : Set X}
(hK : IsCompact K)
(lam u : X → ℝ)
(hlam : ContinuousOn lam K)
(hu : ContinuousOn u K)
(hlampos : ∀ p ∈ K, 0 < lam p)
(hupos : ∀ p ∈ K, 0 < u p)
:
∃ (gap : ℝ) (b : ℝ) (B : ℝ),
0 < gap ∧ 0 < b ∧ 0 < B ∧ ∀ p ∈ K,
∀ (L : ℝ),
0 < L →
∀ v ∈ Set.Icc 0 L,
gap ≤ ViscousPropagator.referenceEigenvalue (lam p) (u p) L v ∧ Real.exp (-B * (v - L / 2) ^ 2 / L) ≤ PrimaryPulseBounds.referenceP (lam p) (u p) L v ∧ PrimaryPulseBounds.referenceP (lam p) (u p) L v ≤ Real.exp (-b * (v - L / 2) ^ 2 / L)
Compact positive reference parameters give one spectral gap and two Gaussian constants, chosen independently of every slot length.
theorem
NavierStokes.PrimaryCovarianceBounds.canonicalPrimaryPulse_x_radial
{Q : Type}
[NormedAddCommGroup Q]
(d : PrimaryODE.FrameData Q)
(lam u : ℝ)
{L : ℝ}
(hL : 0 < L)
(U : Set Q)
(hA : ContinuousOn (d.coefficient 1) (U ×ˢ Set.Icc 0 L))
(p : Q)
(hp : p ∈ U)
(hk : d.Kinematics p (Set.Icc 0 L))
{v : ℝ}
(hv : v ∈ Set.Icc 0 L)
:
(PrimaryPulseBounds.canonicalPrimaryPulse d lam u hL U hA p hp hk).x v = PrimaryODE.radialPrimary ⋯ d (fun (z : Q × ℝ) => PrimaryPulseBounds.referenceP lam u L z.2) p v
theorem
NavierStokes.PrimaryCovarianceBounds.canonicalPrimaryPulse_ratio
{Q : Type}
[NormedAddCommGroup Q]
(d : PrimaryODE.FrameData Q)
(lam u : ℝ)
{L : ℝ}
(hL : 0 < L)
(U : Set Q)
(hA : ContinuousOn (d.coefficient 1) (U ×ˢ Set.Icc 0 L))
(p : Q)
(hp : p ∈ U)
(hk : d.Kinematics p (Set.Icc 0 L))
{v : ℝ}
(hv : v ∈ Set.Icc 0 L)
(i : Fin 2)
:
(PrimaryPulseBounds.canonicalPrimaryPulse d lam u hL U hA p hp hk).t v i / (PrimaryPulseBounds.canonicalPrimaryPulse d lam u hL U hA p hp hk).x v = (PrimaryPulseBounds.normalizedPulse d lam u L (p, v / L)).ofLp i.succ / (PrimaryPulseBounds.normalizedPulse d lam u L (p, v / L)).ofLp 0
theorem
NavierStokes.PrimaryCovarianceBounds.canonicalPrimaryPulse_bounds
{Q : Type}
[NormedAddCommGroup Q]
(d : PrimaryODE.FrameData Q)
(lam u : ℝ)
{L r : ℝ}
(hL : 0 < L)
(hr : 1 ≤ r)
(hrsq : r ^ 2 = L)
(U : Set Q)
(hA : ContinuousOn (d.coefficient 1) (U ×ˢ Set.Icc 0 L))
(p : Q)
(hp : p ∈ U)
(hk : d.Kinematics p (Set.Icc 0 L))
{gap b B S C D K : ℝ}
(hgap : 0 < gap)
(hb : 0 < b)
(hB : 0 < B)
(hC : 0 ≤ C)
(hD : 0 ≤ D)
(hS : 0 < S)
(hlarge : 2 * GrowingMode.coneConstant gap C ≤ S)
(hslot : L ≤ K * S)
(heigen : ∀ v ∈ Set.Icc 0 L, d.eigenvalue (p, v) = ViscousPropagator.referenceEigenvalue lam u L v)
(herr :
∀ v ∈ Set.Icc 0 L,
|d.error11 (p, v)| ≤ C / S ∧ |d.error12 (p, v)| ≤ C / S ∧ |d.error21 (p, v)| ≤ C / S ∧ |d.error22 (p, v)| ≤ C / S)
(hvisc : ∀ v ∈ Set.Icc 0 L, |d.viscosity (p, v) - ViscousPropagator.referenceViscosity lam u L v| ≤ D / S)
(hreference :
∀ v ∈ Set.Icc 0 L,
gap ≤ ViscousPropagator.referenceEigenvalue lam u L v ∧ Real.exp (-B * (v - L / 2) ^ 2 / L) ≤ PrimaryPulseBounds.referenceP lam u L v ∧ PrimaryPulseBounds.referenceP lam u L v ≤ Real.exp (-b * (v - L / 2) ^ 2 / L))
:
PulseCovariance.PulseBounds r (primaryLower C D K) (primaryUpper C D K) b B
(PrimaryPulseBounds.canonicalPrimaryPulse d lam u hL U hA p hp hk).ψ
(PrimaryPulseBounds.canonicalPrimaryPulse d lam u hL U hA p hp hk).x
The cutoff and the radial component of the canonical primary satisfy the covariance pulse bounds. The radial estimate is derived from the actual homogeneous ODE, using only its coefficient errors and the scalar reference envelope.
structure
NavierStokes.PrimaryCovarianceBounds.CoefficientControl
{Q : Type}
(d : PrimaryODE.FrameData Q)
(lam u L S C D : ℝ)
(p : Q)
:
Pointwise input estimates on the actual moving-frame coefficient. These are coefficient hypotheses, not bounds on a solution or covariance.
- eigenvalue (v : ℝ) : v ∈ Set.Icc 0 L → d.eigenvalue (p, v) = ViscousPropagator.referenceEigenvalue lam u L v
Instances For
noncomputable def
NavierStokes.PrimaryCovarianceBounds.nativePrimaryCovariance
{Q : Type}
(vr vt : TorusInverse.Plane)
(r0 h : ℝ)
(d : Fin 2 → ℕ → PrimaryODE.FrameData Q)
(lam u : Fin 2 → ℕ → ℝ)
(n : ℕ)
(p : Q)
:
The literal primaryCovariance with the native chart prefactor and
slot length; the integrands still use the actual constructed ODE solution.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.PrimaryCovarianceBounds.compact_native_primary_bounds
{Q : Type}
[NormedAddCommGroup Q]
{K : Set Q}
(hK : IsCompact K)
(H0 : Q → Mat2)
(T0 : Q → Vec2)
(hH0 : ∀ (i j : Fin 2), ContinuousOn (fun (p : Q) => H0 p i j) K)
(hT0 : ∀ (i : Fin 2), ContinuousOn (fun (p : Q) => T0 p i) K)
(hcone : ∀ p ∈ K, SmoothCovariance.StrictCone (H0 p) (T0 p))
{R : Set (ℝ × ℝ)}
(hR : IsCompact R)
(hRpos : ∀ z ∈ R, 0 < z.1 ∧ 0 < z.2)
(vr vt : TorusInverse.Plane)
(hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0)
{r0 h C D E F : ℝ}
(hr0 : 0 < r0)
(hh : 0 ≤ h)
(hC : 0 ≤ C)
(hD : 0 ≤ D)
(hE : 0 ≤ E)
(hF : 0 ≤ F)
:
∃ (N : ℕ),
4 ≤ N ∧ ∃ (detGap : ℝ) (entryBound : ℝ) (inverseLower : ℝ),
0 < detGap ∧ 1 ≤ entryBound ∧ 0 < inverseLower ∧ ∀ (n : ℕ),
N ≤ n →
∀ (d : Fin 2 → ℕ → PrimaryODE.FrameData Q) (lam u : Fin 2 → ℕ → ℝ) (U : Set Q),
(∀ (c : Fin 2),
ContinuousOn ((d c n).coefficient 1) (U ×ˢ Set.Icc 0 (ChartScales.slotLength r0 h n))) →
∀ p ∈ K,
p ∈ U →
(∀ (c : Fin 2), (d c n).Kinematics p (Set.Icc 0 (ChartScales.slotLength r0 h n))) →
(∀ (c : Fin 2), (lam c n, u c n) ∈ R) →
(∀ (c : Fin 2),
CoefficientControl (d c n) (lam c n) (u c n) (ChartScales.slotLength r0 h n)
(ChartScales.S n) C D p) →
(∀ (c i : Fin 2),
∀ v ∈ Set.Icc 0 (ChartScales.slotLength r0 h n),
|(PrimaryPulseBounds.normalizedPulse (d c n) (lam c n) (u c n)
(ChartScales.slotLength r0 h n)
(p, v / ChartScales.slotLength r0 h n)).ofLp
i.succ / (PrimaryPulseBounds.normalizedPulse (d c n) (lam c n) (u c n)
(ChartScales.slotLength r0 h n)
(p, v / ChartScales.slotLength r0 h n)).ofLp
0 - H0 p i c| ≤ E / ChartScales.slotLength r0 h n + F * |v - ChartScales.slotLength r0 h n / 2| / ChartScales.slotLength r0 h n) →
∀ (zeta : ℝ),
0 ≤ zeta →
ZeroOrderBounds (√(ChartScales.S n)) detGap entryBound inverseLower zeta
(nativePrimaryCovariance vr vt r0 h d lam u n p)
(FlatCovariance.scaledTarget zeta (T0 p))
Uniform zeroth-order bounds for the same actual primary covariance
used in PrimaryPulseBounds. All constants and the band threshold are
chosen from the fixed compact model, reference range, and coefficient
error constants. In particular they are chosen before the band, the
particular ODE coefficients, and the possibly flat target factor zeta.
The only directional input is a pointwise ratio estimate for the actual uncut primary. Gaussian size, positive column masses, determinant gap, and inverse-weight lower bounds are derived in the proof.
Scalar-cone input adapter #
theorem
NavierStokes.PrimaryCovarianceBounds.scalar_cone_model
{X : Type u_1}
[TopologicalSpace X]
{K : Set X}
{c₀ u m t : X → ℝ}
(hc₀ : ContinuousOn c₀ K)
(hu : ContinuousOn u K)
(hm : ContinuousOn m K)
(ht : ContinuousOn t K)
(hc₀neg : ∀ p ∈ K, c₀ p < 0)
(hupos : ∀ p ∈ K, 0 < u p)
(hcone : ∀ p ∈ K, |Covariance.normalMagnitude (c₀ p) (u p) * t p| < u p * m p)
:
(∀ (i j : Fin 2), ContinuousOn (fun (p : X) => PulseCovariance.signedModel (c₀ p) (u p) i j) K) ∧ (∀ (i : Fin 2), ContinuousOn (fun (p : X) => Covariance.target (m p) (t p) i) K) ∧ ∀ p ∈ K, SmoothCovariance.StrictCone (PulseCovariance.signedModel (c₀ p) (u p)) (Covariance.target (m p) (t p))
The manuscript's two signed model columns satisfy all model-side
inputs of compact_native_primary_bounds directly from the scalar cone.
The actual pulse directions may be compared to these columns using the
ratio hypothesis of that theorem.
The normalized base error Q^(2h) is exactly the squared native small
parameter used by the phase estimates.
Reference scale, given by Real.sqrt (lam / (viscosity * dampingDenominator u)).
Equations
- NavierStokes.BasePhaseGeometry.referenceScale lam viscosity u = √(lam / (viscosity * NavierStokes.BasePhaseGeometry.dampingDenominator u))
Instances For
theorem
NavierStokes.BasePhaseGeometry.referenceScale_pos
{lam viscosity u : ℝ}
(hlam : 0 < lam)
(hv : 0 < viscosity)
:
theorem
NavierStokes.BasePhaseGeometry.referenceScale_normalization
{lam viscosity u : ℝ}
(hlam : 0 < lam)
(hv : 0 < viscosity)
:
theorem
NavierStokes.BasePhaseGeometry.referenceScale_bounds
{lam l M viscosity u : ℝ}
(hl : 0 < l)
(hlam : l ≤ lam)
(hM : lam ≤ M)
(hvlo : 1 ≤ viscosity)
(hvhi : viscosity ≤ 4)
:
√(l / (4 * dampingDenominator u)) ≤ referenceScale lam viscosity u ∧ referenceScale lam viscosity u ≤ √M
Uniform scale bounds are derived from the actual rounded viscosity factor, rather than imposed on the chosen phase normal.
theorem
NavierStokes.BasePhaseGeometry.dyadic_referenceScale_normalization
(h u : ℝ)
{lam : ℝ}
(hlam : 0 < lam)
(n : ℕ)
:
ChartScales.epsilon h n * ↑(ChartScales.carrier h n) ^ 2 * referenceScale lam (ChartScales.epsilon h n * ↑(ChartScales.carrier h n) ^ 2) u ^ 2 = lam / dampingDenominator u
theorem
NavierStokes.BasePhaseGeometry.localBase_mono
{F G F0 G0 : Slow → ℝ}
{U : Set Slow}
{M T ε : ℝ}
(h : PhaseEstimates.LocalBaseBounds F G F0 G0 U M ε)
(hMT : M ≤ T)
:
PhaseEstimates.LocalBaseBounds F G F0 G0 U T ε
theorem
NavierStokes.BasePhaseGeometry.derivative_norm_of_error
{F F0 : Slow → ℝ}
{q : Slow}
{M ε : ℝ}
(hM : 0 ≤ M)
(hε : ε ^ 2 ≤ 1)
(href : ‖fderiv ℝ F0 q‖ ≤ M)
(herr : ‖fderiv ℝ F q - fderiv ℝ F0 q‖ ≤ M * ε ^ 2)
:
The norm of an actual base derivative is bounded by the reference derivative and the normalized C1 error.
theorem
NavierStokes.BasePhaseGeometry.localBase_of_normalized_error
{F G F0 G0 : Slow → ℝ}
{U : Set Slow}
{M ε : ℝ}
(hM : 0 ≤ M)
(hε : ε ^ 2 ≤ 1)
(hU : Convex ℝ U)
(hF : ∀ x ∈ U, DifferentiableAt ℝ F x)
(hG : ∀ x ∈ U, DifferentiableAt ℝ G x)
(hF0 : ∀ x ∈ U, DifferentiableAt ℝ F0 x)
(hG0 : ∀ x ∈ U, DifferentiableAt ℝ G0 x)
(hF02 : ∀ x ∈ U, DifferentiableAt ℝ (fderiv ℝ F0) x)
(hG02 : ∀ x ∈ U, DifferentiableAt ℝ (fderiv ℝ G0) x)
(hDF0 : ∀ x ∈ U, ‖fderiv ℝ F0 x‖ ≤ M)
(hDG0 : ∀ x ∈ U, ‖fderiv ℝ G0 x‖ ≤ M)
(hDDF0 : ∀ x ∈ U, ‖fderiv ℝ (fderiv ℝ F0) x‖ ≤ M)
(hDDG0 : ∀ x ∈ U, ‖fderiv ℝ (fderiv ℝ G0) x‖ ≤ M)
(hvalue : ∀ x ∈ U, |F x - F0 x| ≤ M * ε ^ 2)
(hDF : ∀ x ∈ U, ‖fderiv ℝ F x - fderiv ℝ F0 x‖ ≤ M * ε ^ 2)
(hDG : ∀ x ∈ U, ‖fderiv ℝ G x - fderiv ℝ G0 x‖ ≤ M * ε ^ 2)
:
PhaseEstimates.LocalBaseBounds F G F0 G0 U (2 * M) ε
Primitive normalized-base C1 errors and fixed reference C2 bounds give all local hypotheses used by the phase estimate.
theorem
NavierStokes.BasePhaseGeometry.frame_errors_of_normal_close
{n nDot : Space}
{K g g0 : Plane}
{F F0 B s b M A δ η : ℝ}
(hb : 0 < b)
(hbB : b ≤ B)
(hK : ‖K‖ = 1)
(hsmall : δ ≤ B / 2)
(hn : ‖n - MovingFrameODE.pack (B * s) (B • K)‖ ≤ δ)
(hnd : ‖nDot‖ ≤ δ)
(hM : 1 ≤ M)
(hA : 0 ≤ A)
(hs : |s| ≤ A)
(hF0 : |F0| ≤ M)
(hg0 : ‖g0‖ ≤ M)
(horth : inner ℝ K g0 = 0)
(hη : 0 ≤ η)
(hF : |F - F0| ≤ η)
(hg : ‖g - g0‖ ≤ η)
:
have G := M + 2 + 2 * A;
have E := η + 8 * (1 + A) * δ / b;
have R := PrimaryODE.localFrame n;
have r := MovingFrameODE.radialSlope n;
have rd := PhaseEstimates.slopeDerivative n nDot;
have rot := PhaseEstimates.angularVelocity n nDot;
|MovingFrameODE.coeff11 r rd (inner ℝ (R 0) g)| ≤ 16 * G ^ 2 * (1 + G) * E ∧ |MovingFrameODE.coeff12 F ((R 1).ofLp 0) r rot - 2 * F0 * (MovingFrameODE.quarterTurn K).ofLp 0 / (1 + s ^ 2)| ≤ 16 * G ^ 2 * (1 + G) * E ∧ |MovingFrameODE.coeff21 F ((R 1).ofLp 0) (inner ℝ (R 1) g) r rot - -(2 * F0 * (MovingFrameODE.quarterTurn K).ofLp 0 + inner ℝ (MovingFrameODE.quarterTurn K) g0)| ≤ 16 * G ^ 2 * (1 + G) * E
Normal comparison and base comparison imply the three geometric coefficient errors. All changing-frame terms are included.
theorem
NavierStokes.BasePhaseGeometry.damping_error_of_normal_close
{n : Space}
{K : Plane}
{B s A M δ ν : ℝ}
(hK : ‖K‖ = 1)
(hB : 0 < B)
(hBM : B ≤ M)
(hs : |s| ≤ A)
(hsmall : δ ≤ B / 2)
(hn : ‖n - MovingFrameODE.pack (B * s) (B • K)‖ ≤ δ)
(hν0 : 0 ≤ ν)
(hν4 : ν ≤ 4)
:
The damping error is two-sided. It follows from normal comparison and the actual bounded viscosity coefficient, including all high harmonics.
theorem
NavierStokes.BasePhaseGeometry.phase_errors_on_mesh
{F G F0 G0 : Slow → ℝ}
{U : Set Slow}
{q q0 : Slow}
{ε target pz v θ B sigma u L M S k : ℝ}
{K : Plane}
(hbase : PhaseEstimates.LocalBaseBounds F G F0 G0 U M ε)
(hq : q ∈ U)
(hq0 : q0 ∈ U)
(hdiameter : ‖q - q0‖ ≤ 3 / S ^ 3)
(hR : q.1 ≠ 0)
(hR0 : q0.1 ≠ 0)
(hg : PhaseEstimates.shearVector F0 G0 q0 ≠ 0)
(horth : inner ℝ K (PhaseEstimates.shearVector F0 G0 q0) = 0)
(hfreq :
!₂[target / q0.1, pz] = PhaseEstimates.representativeFrequency B sigma u L K (PhaseEstimates.shearVector F0 G0 q0))
(hM : 1 ≤ M)
(hS : 2 ≤ S)
(hk : 1 ≤ k)
(hε : 0 < ε)
(htarget : |target| ≤ M)
(hpz : |pz| ≤ M)
(hB : |B| ≤ M)
(hsigma : |sigma| = 1)
(hu : |u| ≤ M)
(hgi : 1 / ‖PhaseEstimates.shearVector F0 G0 q0‖ ≤ M)
(hL : 1 / |L| ≤ M / S)
(hv : |v| ≤ M * S)
(hRi : |1 / q.1| ≤ M)
(hR0i : |1 / q0.1| ≤ M)
(hε2 : S ^ 2 * ε ^ 2 ≤ 1)
(hk2 : S ^ 2 / k ≤ 1)
(hε1 : ε * S ^ 2 ≤ 1)
:
‖PhaseCalculus.phaseNormal ε (PhaseEstimates.roundedFrequency k target) pz (sigma * B * u / 2) F G (q, θ, v) - PhaseEstimates.referenceNormal B sigma u L v K‖ ≤ normalConstant M / S ∧ ‖PhaseCalculus.normalSlotDerivative ε (PhaseEstimates.roundedFrequency k target) pz F G q‖ ≤ normalConstant M / S
The actual two-mesh enlargement has diameter three mesh units. Using the phase estimate at half the scale retains a fixed, band-independent constant and does not strengthen this geometric input.
theorem
NavierStokes.BasePhaseGeometry.reference_off_diagonal
{lam c0 u L v s a b : ℝ}
(hc : c0 ≠ 0)
(hs : s ^ 2 = PulseGrowth.slotMagnitude u L v ^ 2)
(ha : lam / c0 = a)
(hb : lam * c0 = b)
:
ViscousPropagator.referenceEigenvalue lam u L v / PrimaryODE.referenceProfile c0 u L v = a / (1 + s ^ 2) ∧ ViscousPropagator.referenceEigenvalue lam u L v * PrimaryODE.referenceProfile c0 u L v = b
Exact reference diagonalization; its scalar identities are supplied by the representative eigenpair construction.
theorem
NavierStokes.BasePhaseGeometry.frequencyBound_bounds
{M : ℝ}
(hM : 1 ≤ M)
:
M ≤ frequencyBound M ∧ M * (M + M ^ 4) + 1 ≤ frequencyBound M ∧ M + M ^ 4 ≤ frequencyBound M ∧ M ^ 2 ≤ frequencyBound M ∧ 4 ≤ frequencyBound M
Coordinate constant, given by `16 * (M + 2 + 2 * (3 * M)) ^ 2 * (1 + (M + 2 + 2 * (3 * M)))
- (16 * M ^ 2 + 8 * (1 + 3 * M) * phaseConstant M / normalLower M u)`.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Eigen bound, given by M * (2 + 3 * M).
Equations
- NavierStokes.BasePhaseGeometry.eigenBound M = M * (2 + 3 * M)
Instances For
Modal constant, given by (1 + 2 * eigenBound M) * coordinateConstant M u + 3 * M ^ 3.
Equations
Instances For
Only numerical scale conditions occur here. In particular, no normal, coefficient, solution, or covariance estimate is assumed.
Instances For
theorem
NavierStokes.BasePhaseGeometry.exists_large_band
(h M u T : ℝ)
(hh : 0 < h)
(hM : 1 ≤ M)
(N0 : ℕ)
:
∃ N ≥ N0, ∀ n ≥ N, LargeBand h M u n ∧ T ≤ ChartScales.S n
All constants are fixed before this threshold. An arbitrary previous band cutoff and arbitrary additional slow-scale requirement are allowed.
structure
NavierStokes.BasePhaseGeometry.FamilyData
{ι : Type u_1}
(D : PhaseJetBounds.Domain ι Slow)
(h r0 u M : ℝ)
:
Type u_1
Fixed normalized-base data and frozen representative data. The representative point is selected separately from the actual enlarged mesh; the equality and distance fields are the interface to that proof. All phase quantities below are constructed from this record.
- band : ι → ℕ
Band of
FamilyData, of typeι → ℕ. F of
FamilyData, of typeι → Slow → ℝ.Geometric data of
FamilyData, of typeι → Slow → ℝ.F0 of
FamilyData, of typeι → Slow → ℝ.G0 of
FamilyData, of typeι → Slow → ℝ.U of
FamilyData, of typeι → Set Slow.- q0 : ι → Slow
Q0 of
FamilyData, of typeι → Slow. - K : ι → Plane
K of
FamilyData, of typeι → Plane. - lam : ι → ℝ
Lam of
FamilyData, of typeι → ℝ. - c0 : ι → ℝ
C0 of
FamilyData, of typeι → ℝ. - sigma : ι → ℝ
Sigma of
FamilyData, of typeι → ℝ. - theta : ι → ℝ
Theta of
FamilyData, of typeι → ℝ. - base (i : ι) : PhaseEstimates.LocalBaseBounds (self.F i) (self.G i) (self.F0 i) (self.G0 i) (self.U i) M (ChartScales.epsilon h (self.band i))
- baseF : PhaseJetBounds.PolynomialJets D self.F
- baseG : PhaseJetBounds.PolynomialJets D self.G
Instances For
noncomputable def
NavierStokes.BasePhaseGeometry.FamilyData.length
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(i : ι)
:
Length, given by ChartScales.slotLength r0 h (a.band i).
Equations
- a.length i = NavierStokes.ChartScales.slotLength r0 h (a.band i)
Instances For
noncomputable def
NavierStokes.BasePhaseGeometry.FamilyData.viscosity
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(i : ι)
:
Viscosity, given by ChartScales.epsilon h (a.band i) * (ChartScales.carrier h (a.band i) : ℝ) ^ 2.
Equations
- a.viscosity i = NavierStokes.ChartScales.epsilon h (a.band i) * ↑(NavierStokes.ChartScales.carrier h (a.band i)) ^ 2
Instances For
noncomputable def
NavierStokes.BasePhaseGeometry.FamilyData.B
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(i : ι)
:
B, given by referenceScale (a.lam i) (a.viscosity i) u.
Equations
- a.B i = NavierStokes.BasePhaseGeometry.referenceScale (a.lam i) (a.viscosity i) u
Instances For
noncomputable def
NavierStokes.BasePhaseGeometry.FamilyData.frequency
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(i : ι)
:
Frequency, constructed using PhaseEstimates.representativeFrequency.
Equations
Instances For
noncomputable def
NavierStokes.BasePhaseGeometry.FamilyData.phase
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
:
Phase, bundling epsilon, p, pz, x0 and the required compatibility proofs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.BasePhaseGeometry.FamilyData.frame
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(i : ι)
:
Frame, given by a.phase.frameData a.lam a.c0 (fun _ => u) a.length a.viscosity i.
Instances For
noncomputable def
NavierStokes.BasePhaseGeometry.FamilyData.slot
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(i : ι)
:
Slot, given by Ioo (-(a.length i)) (2 * a.length i).
Instances For
noncomputable def
NavierStokes.BasePhaseGeometry.FamilyData.slope
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(i : ι)
(z : Slow × ℝ)
:
Slope, given by PhaseEstimates.signedSlot (a.sigma i) u (a.length i) z.2.
Equations
- a.slope i z = NavierStokes.PhaseEstimates.signedSlot (a.sigma i) u (a.length i) z.2
Instances For
noncomputable def
NavierStokes.BasePhaseGeometry.FamilyData.angularMode
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(i : ι)
:
The actual angular carrier is a nonzero integer, including the zero-floor case, which is replaced by the integer one.
Equations
- a.angularMode i = NavierStokes.PhaseEstimates.nonzeroRound (↑(NavierStokes.ChartScales.carrier h (a.band i)) * a.target i)
Instances For
theorem
NavierStokes.BasePhaseGeometry.FamilyData.angularMode_ne_zero
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(i : ι)
:
theorem
NavierStokes.BasePhaseGeometry.FamilyData.carrier_mul_angular_frequency
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(i : ι)
:
theorem
NavierStokes.BasePhaseGeometry.FamilyData.angular_rounding_error
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(i : ι)
:
theorem
NavierStokes.BasePhaseGeometry.FamilyData.lambda_pos
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(hM : 1 ≤ M)
(i : ι)
:
theorem
NavierStokes.BasePhaseGeometry.FamilyData.ratio_ne
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(hM : 1 ≤ M)
(i : ι)
:
theorem
NavierStokes.BasePhaseGeometry.FamilyData.B_bounds
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(hh : 0 ≤ h)
(hM : 1 ≤ M)
(i : ι)
:
theorem
NavierStokes.BasePhaseGeometry.FamilyData.B_pos
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(hh : 0 ≤ h)
(hM : 1 ≤ M)
(i : ι)
:
theorem
NavierStokes.BasePhaseGeometry.FamilyData.length_pos
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(hr : 0 < r0)
(i : ι)
:
theorem
NavierStokes.BasePhaseGeometry.FamilyData.magnitude_bound
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(hr : 0 < r0)
(hu : 0 ≤ u)
(huM : u ≤ M)
{i : ι}
{v : ℝ}
(hv : v ∈ a.slot i)
:
theorem
NavierStokes.BasePhaseGeometry.FamilyData.phase_estimates
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(hh : 0 ≤ h)
(hr : 0 < r0)
(hM : 1 ≤ M)
(hu : |u| ≤ M)
(hL : 1 / (2 * r0) ≤ M)
(hslot : 4 * r0 * ChartScales.Tg ≤ M)
(i : ι)
(hn : LargeBand h M u (a.band i))
{q : Slow}
(hq : q ∈ D.carrier i)
{v : ℝ}
(hv : v ∈ a.slot i)
:
Actual phase-normal and normal-motion estimates for every enlarged slot point. These follow from the normalized base error and rounding.
theorem
NavierStokes.BasePhaseGeometry.FamilyData.base_estimates
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(hM : 1 ≤ M)
(i : ι)
(hn : LargeBand h M u (a.band i))
{q : Slow}
(hq : q ∈ D.carrier i)
:
theorem
NavierStokes.BasePhaseGeometry.FamilyData.phase_error_small
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(hh : 0 ≤ h)
(hM : 1 ≤ M)
(i : ι)
(hn : LargeBand h M u (a.band i))
:
theorem
NavierStokes.BasePhaseGeometry.FamilyData.coordinate_errors
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(hh : 0 ≤ h)
(hr : 0 < r0)
(hM : 1 ≤ M)
(hu : 0 < u)
(huM : u ≤ M)
(hL : 1 / (2 * r0) ≤ M)
(hslot : 4 * r0 * ChartScales.Tg ≤ M)
(i : ι)
(hn : LargeBand h M u (a.band i))
{q : Slow}
(hq : q ∈ D.carrier i)
{v : ℝ}
(hv : v ∈ a.slot i)
:
The three coordinate errors of the actual constructed tangent frame are estimated before changing to the moving eigenbasis.
theorem
NavierStokes.BasePhaseGeometry.FamilyData.modal_errors
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(hh : 0 ≤ h)
(hr : 0 < r0)
(hM : 1 ≤ M)
(hu : 0 < u)
(huM : u ≤ M)
(hL : 1 / (2 * r0) ≤ M)
(hslot : 4 * r0 * ChartScales.Tg ≤ M)
(i : ι)
(hn : LargeBand h M u (a.band i))
{q : Slow}
(hq : q ∈ D.carrier i)
{v : ℝ}
(hv : v ∈ a.slot i)
:
theorem
NavierStokes.BasePhaseGeometry.FamilyData.damping_error
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(hh : 0 ≤ h)
(hr : 0 < r0)
(hM : 1 ≤ M)
(hu : 0 < u)
(huM : u ≤ M)
(hL : 1 / (2 * r0) ≤ M)
(hslot : 4 * r0 * ChartScales.Tg ≤ M)
(i : ι)
(hn : LargeBand h M u (a.band i))
{q : Slow}
(hq : q ∈ D.carrier i)
{v : ℝ}
(hv : v ∈ a.slot i)
:
Two-sided comparison with the Gaussian reference viscosity.
theorem
NavierStokes.BasePhaseGeometry.FamilyData.interval_subset_slot
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(hr : 0 < r0)
(i : ι)
:
theorem
NavierStokes.BasePhaseGeometry.FamilyData.normal_nonzero
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(hh : 0 ≤ h)
(hr : 0 < r0)
(hM : 1 ≤ M)
(hu : |u| ≤ M)
(hL : 1 / (2 * r0) ≤ M)
(hslot : 4 * r0 * ChartScales.Tg ≤ M)
(i : ι)
(hn : LargeBand h M u (a.band i))
{q : Slow}
(hq : q ∈ D.carrier i)
{v : ℝ}
(hv : v ∈ a.slot i)
:
theorem
NavierStokes.BasePhaseGeometry.FamilyData.kinematics
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(hh : 0 ≤ h)
(hr : 0 < r0)
(hM : 1 ≤ M)
(hu : |u| ≤ M)
(hL : 1 / (2 * r0) ≤ M)
(hslot : 4 * r0 * ChartScales.Tg ≤ M)
(i : ι)
(hn : LargeBand h M u (a.band i))
{q : Slow}
(hq : q ∈ D.carrier i)
:
(a.frame i).Kinematics q (Set.Icc 0 (a.length i))
theorem
NavierStokes.BasePhaseGeometry.FamilyData.coefficientControl
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(hh : 0 ≤ h)
(hr : 0 < r0)
(hM : 1 ≤ M)
(hu : 0 < u)
(huM : u ≤ M)
(hL : 1 / (2 * r0) ≤ M)
(hslot : 4 * r0 * ChartScales.Tg ≤ M)
(i : ι)
(hn : LargeBand h M u (a.band i))
{q : Slow}
(hq : q ∈ D.carrier i)
:
PrimaryCovarianceBounds.CoefficientControl (a.frame i) (a.lam i) u (a.length i) (D.scale i) (modalConstant M u)
(dampingConstant M) q
theorem
NavierStokes.BasePhaseGeometry.FamilyData.energy_bound
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(hh : 0 ≤ h)
(hr : 0 < r0)
(hM : 1 ≤ M)
(hu : 0 < u)
(huM : u ≤ M)
(hL : 1 / (2 * r0) ≤ M)
(hslot : 4 * r0 * ChartScales.Tg ≤ M)
(i : ι)
(hn : LargeBand h M u (a.band i))
{q : Slow}
(hq : q ∈ D.carrier i)
{v : ℝ}
(hv : v ∈ a.slot i)
{j : ℤ}
(hj : j ≠ 0)
(w : Plane)
:
The actual modal energy bound holds with the same constants for every
nonzero harmonic. The damping discrepancy is not multiplied by j².
Output lower, given by min (normalLower M u / 2) (1 / M).
Equations
Instances For
theorem
NavierStokes.BasePhaseGeometry.FamilyData.outputBound_bounds
{M : ℝ}
(hM : 1 ≤ M)
:
frequencyBound M ≤ outputBound M ∧ 3 * M ≤ outputBound M ∧ M ^ 2 ≤ outputBound M ∧ 4 ≤ outputBound M ∧ M ≤ outputBound M
noncomputable def
NavierStokes.BasePhaseGeometry.FamilyData.construction
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(hh : 0 ≤ h)
(hr : 0 < r0)
(hM : 1 ≤ M)
(hu : 0 < u)
(huM : u ≤ M)
(hL : 1 / (2 * r0) ≤ M)
(hslot : 4 * r0 * ChartScales.Tg ≤ M)
(hlarge : ∀ (i : ι), LargeBand h M u (a.band i))
:
The actual phase family satisfies every order-zero input of the previous primary-pulse theorem. Its normal comparison, modal errors, and damping comparison are proved here from the base and mesh data.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.BasePhaseGeometry.FamilyData.construction_frame
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(hh : 0 ≤ h)
(hr : 0 < r0)
(hM : 1 ≤ M)
(hu : 0 < u)
(huM : u ≤ M)
(hL : 1 / (2 * r0) ≤ M)
(hslot : 4 * r0 * ChartScales.Tg ≤ M)
(hlarge : ∀ (i : ι), LargeBand h M u (a.band i))
:
theorem
NavierStokes.BasePhaseGeometry.FamilyData.frame_jets
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(hh : 0 ≤ h)
(hr : 0 < r0)
(hM : 1 ≤ M)
(hu : 0 < u)
(huM : u ≤ M)
(hL : 1 / (2 * r0) ≤ M)
(hslot : 4 * r0 * ChartScales.Tg ≤ M)
(hlarge : ∀ (i : ι), LargeBand h M u (a.band i))
:
PhaseJetBounds.FrameJets (D.slot a.slot ⋯) a.frame
Every fixed derivative of the actual coefficient is controlled after the derived zeroth-order geometry is inserted.
theorem
NavierStokes.BasePhaseGeometry.FamilyData.pulse_jets
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(hh : 0 ≤ h)
(hr : 0 < r0)
(hM : 1 ≤ M)
(hu : 0 < u)
(huM : u ≤ M)
(hL : 1 / (2 * r0) ≤ M)
(hslot : 4 * r0 * ChartScales.Tg ≤ M)
(hlarge : ∀ (i : ι), LargeBand h M u (a.band i))
:
PrimaryPulseBounds.EnvelopeJets (PrimaryPulseBounds.productDomain D (fun (x : ι) => Set.Ioo 0 1) ⋯)
(fun (i : ι) (z : Slow × ℝ) => PrimaryPulseBounds.referenceP (a.lam i) u (a.length i) (a.length i * z.2))
fun (i : ι) => PrimaryPulseBounds.normalizedPulse (a.frame i) (a.lam i) u (a.length i)
theorem
NavierStokes.BasePhaseGeometry.FamilyData.coefficient_jets
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r0 u M : ℝ}
(a : FamilyData D h r0 u M)
(hh : 0 ≤ h)
(hr : 0 < r0)
(hM : 1 ≤ M)
(hu : 0 < u)
(huM : u ≤ M)
(hL : 1 / (2 * r0) ≤ M)
(hslot : 4 * r0 * ChartScales.Tg ≤ M)
(hlarge : ∀ (i : ι), LargeBand h M u (a.band i))
(j : ℤ)
:
PhaseJetBounds.PolynomialJets (D.slot a.slot ⋯) fun (i : ι) => (a.frame i).coefficient j
theorem
NavierStokes.BasePhaseGeometry.Representatives.normal_inner_shear
{g : Plane}
(hg : g ≠ 0)
:
theorem
NavierStokes.BasePhaseGeometry.Representatives.ordered_constants
{K : Set Slow}
(hK : IsCompact K)
{F0 G0 : Slow → ℝ}
(hF : ContinuousOn F0 K)
(hg : ContinuousOn (PhaseEstimates.shearVector F0 G0) K)
(hR : ∀ q ∈ K, 0 < q.1)
(hc : ∀ q ∈ K, PrimaryRepresentatives.ReferenceCone (F0 q) (PhaseEstimates.shearVector F0 G0 q))
(h r0 u A T : ℝ)
(hh : 0 < h)
(N0 : ℕ)
:
A compact fixed reference profile chooses every uniform constant
before the band threshold. A may include all prescribed base-chart,
derivative, and radial-annulus constants.
theorem
NavierStokes.BasePhaseGeometry.Representatives.ordered_target_constants
{K : Set Slow}
(hK : IsCompact K)
{F0 G0 : Slow → ℝ}
{T0 : Slow → Plane}
(hF : ContinuousOn F0 K)
(hg : ContinuousOn (PhaseEstimates.shearVector F0 G0) K)
(hT : ContinuousOn T0 K)
(hR : ∀ q ∈ K, 0 < q.1)
(hc : ∀ q ∈ K, PrimaryRepresentatives.ReferenceCone (F0 q) (PhaseEstimates.shearVector F0 G0 q))
(ht : ∀ q ∈ K, PrimaryRepresentatives.TargetCone (F0 q) (PhaseEstimates.shearVector F0 G0 q) (T0 q))
(h r0 A Tmin : ℝ)
(hh : 0 < h)
(N0 : ℕ)
:
∃ (u : ℝ) (η : ℝ) (M : ℝ),
0 < u ∧ 0 < η ∧ 1 ≤ M ∧ A ≤ M ∧ u ≤ M ∧ 1 / (2 * r0) ≤ M ∧ 4 * r0 * ChartScales.Tg ≤ M ∧ (∀ q ∈ K, PrimaryRepresentatives.ParameterBounds M q.1 (F0 q) (PhaseEstimates.shearVector F0 G0 q)) ∧ ∃ N ≥ N0,
(∀ n ≥ N, LargeBand h M u n ∧ Tmin ≤ ChartScales.S n) ∧ ∀ (L : PrimaryRepresentatives.ActiveLabel K),
N ≤ (↑L).1 →
∀ q ∈ K,
q ∈ PrimaryRepresentatives.gridBox (↑L).1 (↑L).2 2 →
inner ℝ (T0 q)
(PrimaryRepresentatives.normalDirection
(PhaseEstimates.shearVector F0 G0 (PrimaryRepresentatives.representative K L))) ≤ -η ∧ |PrimaryRepresentatives.c0 (F0 (PrimaryRepresentatives.representative K L))
(PhaseEstimates.shearVector F0 G0
(PrimaryRepresentatives.representative K L)) * inner ℝ (T0 q)
(PrimaryRepresentatives.transverseDirection
(PhaseEstimates.shearVector F0 G0
(PrimaryRepresentatives.representative K L))) / inner ℝ (T0 q)
(PrimaryRepresentatives.normalDirection
(PhaseEstimates.shearVector F0 G0
(PrimaryRepresentatives.representative K L)))| + η ≤ PrimaryRepresentatives.slopeRatio u
One target-cone choice, one compact parameter constant, and then one band threshold. Both the mixed-point target margin and all analytic phase estimates hold after that same threshold.
noncomputable def
NavierStokes.BasePhaseGeometry.Representatives.family
{ι : Type u_1}
(D : PhaseJetBounds.Domain ι Slow)
{K : Set Slow}
(label : ι → PrimaryRepresentatives.ActiveLabel K)
(U : Set Slow)
(F G : ι → Slow → ℝ)
(F0 G0 : Slow → ℝ)
(h r0 u M : ℝ)
(sigma theta : ι → ℝ)
(hM : 1 ≤ M)
(hscale : ∀ (i : ι), D.scale i = ChartScales.S (↑(label i)).1)
(hgrid : ∀ (i : ι), D.carrier i ⊆ PrimaryRepresentatives.gridBox (↑(label i)).1 (↑(label i)).2 2)
(hinside : ∀ (i : ι), D.carrier i ⊆ U)
(hKU : K ⊆ U)
(hbase : ∀ (i : ι), PhaseEstimates.LocalBaseBounds (F i) (G i) F0 G0 U M (ChartScales.epsilon h (↑(label i)).1))
(hF : PhaseJetBounds.PolynomialJets D F)
(hG : PhaseJetBounds.PolynomialJets D G)
(hradius : ∀ q ∈ U, 1 / M ≤ |q.1| ∧ |q.1| ≤ M)
(hR : ∀ q ∈ K, 0 < q.1)
(hc : ∀ q ∈ K, PrimaryRepresentatives.ReferenceCone (F0 q) (PhaseEstimates.shearVector F0 G0 q))
(hp : ∀ q ∈ K, PrimaryRepresentatives.ParameterBounds M q.1 (F0 q) (PhaseEstimates.shearVector F0 G0 q))
(hsigma : ∀ (i : ι), |sigma i| = 1)
:
FamilyData D h r0 u M
The actual selected mesh representatives and their derived compact eigenpairs instantiate the analytic phase data. In particular, neither representative closeness nor eigenpair bounds are fields of the resulting construction that the caller must postulate independently.
Equations
- One or more equations did not get rendered due to their size.