Joint native-copy bounds for the actual particular inverse #
The modal input bounds below quantify their constants before the lattice copy. The velocity is the actual finite-path Volterra solve and pressure is its actual projected pressure coefficient. No output jet estimate is assumed, and no assertion that separate copy classes have uniform constants is used.
structure
NavierStokes.ParticularCopyBounds.ModalControl
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
(s : WeightedClasses.StripData (P × TorusInverse.Plane))
(α : ℝ)
(d : ℕ → PrimaryODE.FrameData (P × ℝ))
(t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space)
(harmonic : ℤ)
(g : ℕ → CommonCoverSolve.Geometry)
(L : ℕ → ℝ)
(envelope : ℕ → ℝ → ℝ)
(cells : ℕ → TorusInverse.Frequency → Set (P × TorusInverse.Plane))
:
Primitive modal bounds on neighborhoods of the native support cells. Every quantitative constant precedes the band and lattice copy.
- neighborhood : ℕ → TorusInverse.Frequency → Set (P × TorusInverse.Plane)
Neighborhood of
ModalControl, of typeℕ → Frequency → Set (P × Plane). - contains (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) : x ∈ s.domain → x ∈ cells n k → x ∈ self.neighborhood n k
Interval of
ModalControl, of typeℕ → Set ℝ.- bridge (n : ℕ) (k : PrimaryCopyBridge.Frequency) : PrimaryCopyBridge.Inputs (d n) (t n) harmonic (g n) k (self.neighborhood n k) 0 (L n)
- coefficient_smooth (n : ℕ) (k : PrimaryCopyBridge.Frequency) : ContDiffOn ℝ (↑⊤) ((PrimaryCopyBridge.copyFrame (d n) (g n) k).coefficient harmonic) (self.neighborhood n k ×ˢ self.interval n)
- forcing_smooth (n : ℕ) (k : PrimaryCopyBridge.Frequency) : ContDiffOn ℝ (↑⊤) ((PrimaryCopyBridge.copyFrame (d n) (g n) k).forcing (PrimaryCopyBridge.copySource (t n).source (g n) k)) (self.neighborhood n k ×ˢ self.interval n)
- columns_smooth (n : ℕ) (k : PrimaryCopyBridge.Frequency) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (PrimaryPulseBounds.synthesisColumn (PrimaryCopyBridge.copyFrame (d n) (g n) k) i) (self.neighborhood n k ×ˢ self.interval n)
- current_slot (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) : x ∈ self.neighborhood n k → ((g n).coordinates k x.2).2 ∈ Set.Ioo 0 (L n)
Rate of
ModalControl, of typeℕ → ℝ → ℝ.Error rate of
ModalControl, of typeℕ → ℝ.- boundConstant : ℝ
Bound constant of
ModalControl, of typeℝ. - coordinatePower : ℕ
Coordinate power of
ModalControl, of typeℕ. - coordinate_bound (n : ℕ) : CommonCoverClass.argumentCost (g n) ≤ self.boundConstant * s.slow n ^ self.coordinatePower
- energy (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) : x ∈ s.domain → x ∈ cells n k → ∀ v ∈ Set.Icc 0 (L n), ∀ (z : PrimaryODE.State), inner ℝ z (((PrimaryCopyBridge.copyFrame (d n) (g n) k).coefficient harmonic (x, v)) z) ≤ (self.rate n v + self.errorRate n) * ‖z‖ ^ 2
- input_jets (N : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (m : ℕ), ∀ (n : ℕ) (k : TorusInverse.Frequency), ∀ x ∈ s.domain, x ∈ cells n k → ∀ j ≤ N, ∀ v ∈ Set.Icc 0 (L n), ‖iteratedFDeriv ℝ j ((PrimaryCopyBridge.copyFrame (d n) (g n) k).coefficient harmonic) (x, v)‖ ≤ C * s.growth n x ^ m ∧ ‖iteratedFDeriv ℝ j ((PrimaryCopyBridge.copyFrame (d n) (g n) k).forcing (PrimaryCopyBridge.copySource (t n).source (g n) k)) (x, v)‖ ≤ s.epsilon n ^ α * √(s.zeta x) * C * s.growth n x ^ m * envelope n v ∧ ∀ (i : Fin 2), ‖iteratedFDeriv ℝ j (PrimaryPulseBounds.synthesisColumn (PrimaryCopyBridge.copyFrame (d n) (g n) k) i) (x, v)‖ ≤ C * s.growth n x ^ m
Instances For
theorem
NavierStokes.ParticularCopyBounds.ModalControl.smooth_at
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{s : WeightedClasses.StripData (P × TorusInverse.Plane)}
{α : ℝ}
{d : ℕ → PrimaryODE.FrameData (P × ℝ)}
{t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space}
{harmonic : ℤ}
{g : ℕ → CommonCoverSolve.Geometry}
{L : ℕ → ℝ}
{envelope : ℕ → ℝ → ℝ}
{cells : ℕ → TorusInverse.Frequency → Set (P × TorusInverse.Plane)}
(h : ModalControl s α d t harmonic g L envelope cells)
(hL : ∀ (n : ℕ), 0 < L n)
{n : ℕ}
{k : TorusInverse.Frequency}
{x : P × TorusInverse.Plane}
(hx : x ∈ s.domain)
(hk : x ∈ cells n k)
:
ContDiffAt ℝ (↑⊤) ((t n).linearData.copySolve (g n) ⋯ k) x
theorem
NavierStokes.ParticularCopyBounds.ModalControl.localJets
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{s : WeightedClasses.StripData (P × TorusInverse.Plane)}
{α : ℝ}
{d : ℕ → PrimaryODE.FrameData (P × ℝ)}
{t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space}
{harmonic : ℤ}
{g : ℕ → CommonCoverSolve.Geometry}
{L : ℕ → ℝ}
{envelope : ℕ → ℝ → ℝ}
{cells : ℕ → TorusInverse.Frequency → Set (P × TorusInverse.Plane)}
(h : ModalControl s α d t harmonic g L envelope cells)
(hL : ∀ (n : ℕ), 0 < L n)
(W : ℕ → P × TorusInverse.Plane → ℝ)
(hW :
∀ (n : ℕ) (k : TorusInverse.Frequency),
∀ x ∈ s.domain, x ∈ cells n k → envelope n ((g n).coordinates k x.2).2 ≤ W n x)
:
PeriodizedWaveBounds.LocalJets s (fun (n : ℕ) (x : P × TorusInverse.Plane) => √(s.zeta x) * W n x) α cells
fun (n : ℕ) (k : TorusInverse.Frequency) => (t n).linearData.copySolve (g n) ⋯ k
The actual finite-path solve has one bound for all lattice copies. The comparison keeps the native Gaussian envelope in the output weight.
theorem
NavierStokes.ParticularCopyBounds.forced_pressureCoefficient
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{cells : ℕ → I → Set D}
{w : ℕ → D → ℝ}
{α : ℝ}
{normal normalDot velocity forcing : ℕ → I → D → ProblemStatement.Space}
{action : ℕ → I → D → ProblemStatement.Space →L[ℝ] ProblemStatement.Space}
(hN : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 cells normal)
(hNd : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 cells normalDot)
(hA : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 cells action)
(hu : PeriodizedWaveBounds.LocalJets s w α cells velocity)
(hf : PeriodizedWaveBounds.LocalJets s w α cells forcing)
(hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x)
{b M : ℝ}
(hb : 0 < b)
(hl : ∀ (n : ℕ) (k : I), ∀ x ∈ s.domain, x ∈ cells n k → b ≤ ‖normal n k x‖)
(hh : ∀ (n : ℕ) (k : I), ∀ x ∈ s.domain, x ∈ cells n k → ‖normal n k x‖ ≤ M)
:
PeriodizedWaveBounds.LocalJets s w α cells fun (n : ℕ) (k : I) (x : D) =>
TangentProjection.pressureCoefficient (normal n k x) (normalDot n k x) (velocity n k x)
((action n k x) (velocity n k x)) (forcing n k x)
The actual forcing contributes its normal projection to pressure.
theorem
NavierStokes.ParticularCopyBounds.forced_projectedPressure
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{cells : ℕ → I → Set D}
{w : ℕ → D → ℝ}
{α : ℝ}
{normal normalDot velocity forcing : ℕ → I → D → ProblemStatement.Space}
{action : ℕ → I → D → ProblemStatement.Space →L[ℝ] ProblemStatement.Space}
(hN : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 cells normal)
(hNd : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 cells normalDot)
(hA : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 cells action)
(hu : PeriodizedWaveBounds.LocalJets s w α cells velocity)
(hf : PeriodizedWaveBounds.LocalJets s w α cells forcing)
(hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x)
{b M : ℝ}
(hb : 0 < b)
(hl : ∀ (n : ℕ) (k : I), ∀ x ∈ s.domain, x ∈ cells n k → b ≤ ‖normal n k x‖)
(hh : ∀ (n : ℕ) (k : I), ∀ x ∈ s.domain, x ∈ cells n k → ‖normal n k x‖ ≤ M)
{frequency : ℕ → ℝ}
(hfrequency : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / frequency n)
:
PeriodizedWaveBounds.LocalJets s w (α + 1 / 2) cells fun (n : ℕ) (k : I) =>
ParticularWaveBounds.projectedPressure (frequency n) (normal n k) (normalDot n k) (velocity n k)
(fun (x : D) => (action n k x) (velocity n k x)) (forcing n k)
theorem
NavierStokes.ParticularCopyBounds.coefficients_jets
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{s : WeightedClasses.StripData (P × TorusInverse.Plane)}
{α : ℝ}
(base : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane))
(t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space)
(source : ℕ → P × TorusInverse.Plane → HarmonicCalculus.ComplexVector)
(g : ℕ → CommonCoverSolve.Geometry)
(L : ℕ → ℝ)
(hL : ∀ (n : ℕ), 0 < L n)
(envelope : ℕ → ℝ → ℝ)
(W : ℕ → P × TorusInverse.Plane → ℝ)
(d : ℕ → PrimaryODE.FrameData (P × ℝ))
(harmonic : ℤ)
(cells : ℕ → TorusInverse.Frequency → Set (P × TorusInverse.Plane))
(hr : ModalControl s α d (fun (n : ℕ) => ParticularWaveBounds.realData (t n) (source n)) harmonic g L envelope cells)
(hi : ModalControl s α d (fun (n : ℕ) => ParticularWaveBounds.imagData (t n) (source n)) harmonic g L envelope cells)
(hW : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W n x)
(hcompare :
∀ (n : ℕ) (k : TorusInverse.Frequency),
∀ x ∈ s.domain, x ∈ cells n k → envelope n ((g n).coordinates k x.2).2 ≤ W n x)
(hN :
PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : P × TorusInverse.Plane) => 1) 0 cells
fun (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) =>
(t n).normal (ParticularWaveBounds.nativePoint (g n) k x))
(hNd :
PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : P × TorusInverse.Plane) => 1) 0 cells
fun (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) =>
(t n).normalDot (ParticularWaveBounds.nativePoint (g n) k x))
(hA :
PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : P × TorusInverse.Plane) => 1) 0 cells
fun (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) =>
(t n).action (ParticularWaveBounds.nativePoint (g n) k x))
(hf :
PeriodizedWaveBounds.LocalJets s (fun (n : ℕ) (x : P × TorusInverse.Plane) => √(s.zeta x) * W n x) α cells
fun (n : ℕ) (x : TorusInverse.Frequency) => source n)
{b M : ℝ}
(hb : 0 < b)
(hl :
∀ (n : ℕ) (k : TorusInverse.Frequency),
∀ x ∈ s.domain, x ∈ cells n k → b ≤ ‖(t n).normal (ParticularWaveBounds.nativePoint (g n) k x)‖)
(hh :
∀ (n : ℕ) (k : TorusInverse.Frequency),
∀ x ∈ s.domain, x ∈ cells n k → ‖(t n).normal (ParticularWaveBounds.nativePoint (g n) k x)‖ ≤ M)
(hfrequency : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / base.frequency n)
:
(PeriodizedWaveBounds.LocalJets s (fun (n : ℕ) (x : P × TorusInverse.Plane) => √(s.zeta x) * W n x) α cells
fun (n : ℕ) (k : TorusInverse.Frequency) =>
(ParticularWaveBounds.complexCopyCoefficients base t source g (fun (x : ℕ) => k) L hL).amplitude n) ∧ PeriodizedWaveBounds.LocalJets s (fun (n : ℕ) (x : P × TorusInverse.Plane) => √(s.zeta x) * W n x) (α + 1 / 2) cells
fun (n : ℕ) (k : TorusInverse.Frequency) =>
(ParticularWaveBounds.complexCopyCoefficients base t source g (fun (x : ℕ) => k) L hL).pressure n
Native bounds for the literal complex particular velocity and its forced pressure, with constants preceding every copy selector.
theorem
NavierStokes.ParticularCopyBounds.coefficients_localized_jets
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{s : WeightedClasses.StripData (P × TorusInverse.Plane)}
{α : ℝ}
(base : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane))
(t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space)
(source : ℕ → P × TorusInverse.Plane → HarmonicCalculus.ComplexVector)
(g : ℕ → CommonCoverSolve.Geometry)
(L : ℕ → ℝ)
(hL : ∀ (n : ℕ), 0 < L n)
(envelope : ℕ → ℝ → ℝ)
(W : ℕ → P × TorusInverse.Plane → ℝ)
(d : ℕ → PrimaryODE.FrameData (P × ℝ))
(harmonic : ℤ)
(cells : ℕ → TorusInverse.Frequency → Set (P × TorusInverse.Plane))
(hr : ModalControl s α d (fun (n : ℕ) => ParticularWaveBounds.realData (t n) (source n)) harmonic g L envelope cells)
(hi : ModalControl s α d (fun (n : ℕ) => ParticularWaveBounds.imagData (t n) (source n)) harmonic g L envelope cells)
(hW : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W n x)
(hcompare :
∀ (n : ℕ) (k : TorusInverse.Frequency),
∀ x ∈ s.domain, x ∈ cells n k → envelope n ((g n).coordinates k x.2).2 ≤ W n x)
(hN :
PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : P × TorusInverse.Plane) => 1) 0 cells
fun (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) =>
(t n).normal (ParticularWaveBounds.nativePoint (g n) k x))
(hNd :
PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : P × TorusInverse.Plane) => 1) 0 cells
fun (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) =>
(t n).normalDot (ParticularWaveBounds.nativePoint (g n) k x))
(hA :
PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : P × TorusInverse.Plane) => 1) 0 cells
fun (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) =>
(t n).action (ParticularWaveBounds.nativePoint (g n) k x))
(hf :
PeriodizedWaveBounds.LocalJets s (fun (n : ℕ) (x : P × TorusInverse.Plane) => √(s.zeta x) * W n x) α cells
fun (n : ℕ) (x : TorusInverse.Frequency) => source n)
{b M : ℝ}
(hb : 0 < b)
(hl :
∀ (n : ℕ) (k : TorusInverse.Frequency),
∀ x ∈ s.domain, x ∈ cells n k → b ≤ ‖(t n).normal (ParticularWaveBounds.nativePoint (g n) k x)‖)
(hh :
∀ (n : ℕ) (k : TorusInverse.Frequency),
∀ x ∈ s.domain, x ∈ cells n k → ‖(t n).normal (ParticularWaveBounds.nativePoint (g n) k x)‖ ≤ M)
(hfrequency : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / base.frequency n)
(cutoff : TorusInverse.Frequency → ℕ → P × TorusInverse.Plane → ℝ)
(hcutoff :
PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : P × TorusInverse.Plane) => 1) 0 cells
fun (n : ℕ) (k : TorusInverse.Frequency) => cutoff k n)
:
(PeriodizedWaveBounds.LocalJets s (fun (n : ℕ) (x : P × TorusInverse.Plane) => √(s.zeta x) * W n x) α cells
fun (n : ℕ) (k : TorusInverse.Frequency) =>
((ParticularWaveBounds.complexCopyCoefficients base t source g (fun (x : ℕ) => k) L hL).withCutoff
(cutoff k)).amplitude
n) ∧ PeriodizedWaveBounds.LocalJets s (fun (n : ℕ) (x : P × TorusInverse.Plane) => √(s.zeta x) * W n x) (α + 1 / 2) cells
fun (n : ℕ) (k : TorusInverse.Frequency) =>
((ParticularWaveBounds.complexCopyCoefficients base t source g (fun (x : ℕ) => k) L hL).withCutoff
(cutoff k)).pressure
n
The common cutoff is applied once, before the periodized sum and the
exact curl. These are the native hypotheses of common_bounds_from_native.
noncomputable def
NavierStokes.ParticularCopyBounds.nativeEnvelope
{P : Type}
[NormedAddCommGroup P]
(K : PeriodizedWaveBounds.Cells (P × TorusInverse.Plane) TorusInverse.Frequency)
(g : ℕ → CommonCoverSolve.Geometry)
(envelope : ℕ → ℝ → ℝ)
(n : ℕ)
(x : P × TorusInverse.Plane)
:
The reference envelope of the unique active native copy. This majorant need not be smooth; the actual fields carry the smoothness.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ParticularCopyBounds.nativeEnvelope_eq
{P : Type}
[NormedAddCommGroup P]
(K : PeriodizedWaveBounds.Cells (P × TorusInverse.Plane) TorusInverse.Frequency)
(g : ℕ → CommonCoverSolve.Geometry)
(envelope : ℕ → ℝ → ℝ)
{n : ℕ}
{k : TorusInverse.Frequency}
{x : P × TorusInverse.Plane}
(hx : x ∈ K.carrier n k)
:
theorem
NavierStokes.ParticularCopyBounds.nativeEnvelope_nonneg
{P : Type}
[NormedAddCommGroup P]
(K : PeriodizedWaveBounds.Cells (P × TorusInverse.Plane) TorusInverse.Frequency)
(g : ℕ → CommonCoverSolve.Geometry)
(envelope : ℕ → ℝ → ℝ)
(he : ∀ (n : ℕ) (v : ℝ), 0 ≤ envelope n v)
(n : ℕ)
(x : P × TorusInverse.Plane)
:
theorem
NavierStokes.ParticularCopyBounds.nativeEnvelope_le_one
{P : Type}
[NormedAddCommGroup P]
(K : PeriodizedWaveBounds.Cells (P × TorusInverse.Plane) TorusInverse.Frequency)
(g : ℕ → CommonCoverSolve.Geometry)
(envelope : ℕ → ℝ → ℝ)
(he : ∀ (n : ℕ) (k : TorusInverse.Frequency), ∀ x ∈ K.carrier n k, envelope n ((g n).coordinates k x.2).2 ≤ 1)
(n : ℕ)
(x : P × TorusInverse.Plane)
:
structure
NavierStokes.ParticularCopyBounds.UniformModalControl
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{Label : Type}
(s : WeightedClasses.StripData (P × TorusInverse.Plane))
(α : ℝ)
(d : Label → ℕ → PrimaryODE.FrameData (P × ℝ))
(t : Label → ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space)
(harmonic : ℤ)
(g : Label → ℕ → CommonCoverSolve.Geometry)
(L : Label → ℕ → ℝ)
(envelope : Label → ℕ → ℝ → ℝ)
(cells : Label → ℕ → TorusInverse.Frequency → Set (P × TorusInverse.Plane))
:
All primitive constants are chosen before the external spatial label as well as the band and native lattice copy.
- neighborhood : Label → ℕ → TorusInverse.Frequency → Set (P × TorusInverse.Plane)
Neighborhood of
UniformModalControl, of typeLabel → ℕ → Frequency → Set (P × Plane). - open_neighborhood (l : Label) (n : ℕ) (k : TorusInverse.Frequency) : IsOpen (self.neighborhood l n k)
- contains (l : Label) (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) : x ∈ s.domain → x ∈ cells l n k → x ∈ self.neighborhood l n k
Interval of
UniformModalControl, of typeLabel → ℕ → Set ℝ.- bridge (l : Label) (n : ℕ) (k : PrimaryCopyBridge.Frequency) : PrimaryCopyBridge.Inputs (d l n) (t l n) harmonic (g l n) k (self.neighborhood l n k) 0 (L l n)
- coefficient_smooth (l : Label) (n : ℕ) (k : PrimaryCopyBridge.Frequency) : ContDiffOn ℝ (↑⊤) ((PrimaryCopyBridge.copyFrame (d l n) (g l n) k).coefficient harmonic) (self.neighborhood l n k ×ˢ self.interval l n)
- forcing_smooth (l : Label) (n : ℕ) (k : PrimaryCopyBridge.Frequency) : ContDiffOn ℝ (↑⊤) ((PrimaryCopyBridge.copyFrame (d l n) (g l n) k).forcing (PrimaryCopyBridge.copySource (t l n).source (g l n) k)) (self.neighborhood l n k ×ˢ self.interval l n)
- columns_smooth (l : Label) (n : ℕ) (k : PrimaryCopyBridge.Frequency) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (PrimaryPulseBounds.synthesisColumn (PrimaryCopyBridge.copyFrame (d l n) (g l n) k) i) (self.neighborhood l n k ×ˢ self.interval l n)
- current_slot (l : Label) (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) : x ∈ self.neighborhood l n k → ((g l n).coordinates k x.2).2 ∈ Set.Ioo 0 (L l n)
Rate of
UniformModalControl, of typeLabel → ℕ → ℝ → ℝ.- envelope_deriv (l : Label) (n : ℕ) (v : ℝ) : HasDerivAt (envelope l n) (self.rate l n v * envelope l n v) v
Error rate of
UniformModalControl, of typeLabel → ℕ → ℝ.- boundConstant : ℝ
Bound constant of
UniformModalControl, of typeℝ. - coordinatePower : ℕ
Coordinate power of
UniformModalControl, of typeℕ. - coordinate_bound (l : Label) (n : ℕ) : CommonCoverClass.argumentCost (g l n) ≤ self.boundConstant * s.slow n ^ self.coordinatePower
- energy (l : Label) (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) : x ∈ s.domain → x ∈ cells l n k → ∀ v ∈ Set.Icc 0 (L l n), ∀ (z : PrimaryODE.State), inner ℝ z (((PrimaryCopyBridge.copyFrame (d l n) (g l n) k).coefficient harmonic (x, v)) z) ≤ (self.rate l n v + self.errorRate l n) * ‖z‖ ^ 2
- input_jets (N : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (m : ℕ), ∀ (l : Label) (n : ℕ) (k : TorusInverse.Frequency), ∀ x ∈ s.domain, x ∈ cells l n k → ∀ j ≤ N, ∀ v ∈ Set.Icc 0 (L l n), ‖iteratedFDeriv ℝ j ((PrimaryCopyBridge.copyFrame (d l n) (g l n) k).coefficient harmonic) (x, v)‖ ≤ C * s.growth n x ^ m ∧ ‖iteratedFDeriv ℝ j ((PrimaryCopyBridge.copyFrame (d l n) (g l n) k).forcing (PrimaryCopyBridge.copySource (t l n).source (g l n) k)) (x, v)‖ ≤ s.epsilon n ^ α * √(s.zeta x) * C * s.growth n x ^ m * envelope l n v ∧ ∀ (i : Fin 2), ‖iteratedFDeriv ℝ j (PrimaryPulseBounds.synthesisColumn (PrimaryCopyBridge.copyFrame (d l n) (g l n) k) i) (x, v)‖ ≤ C * s.growth n x ^ m
Instances For
noncomputable def
NavierStokes.ParticularCopyBounds.UniformModalControl.pull
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{Label : Type}
{s : WeightedClasses.StripData (P × TorusInverse.Plane)}
{α : ℝ}
{d : Label → ℕ → PrimaryODE.FrameData (P × ℝ)}
{t : Label → ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space}
{harmonic : ℤ}
{g : Label → ℕ → CommonCoverSolve.Geometry}
{L : Label → ℕ → ℝ}
{envelope : Label → ℕ → ℝ → ℝ}
{cells : Label → ℕ → TorusInverse.Frequency → Set (P × TorusInverse.Plane)}
(h : UniformModalControl s α d t harmonic g L envelope cells)
(e : ℕ → ℕ × Label)
:
ModalControl (UniformPrimaryWeights.reindexedStrip s e) α (fun (n : ℕ) => d (e n).2 (e n).1)
(fun (n : ℕ) => t (e n).2 (e n).1) harmonic (fun (n : ℕ) => g (e n).2 (e n).1) (fun (n : ℕ) => L (e n).2 (e n).1)
(fun (n : ℕ) => envelope (e n).2 (e n).1) fun (n : ℕ) => cells (e n).2 (e n).1
Pull, bundling neighborhood, open_neighborhood, contains, interval and the required
compatibility proofs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ParticularCopyBounds.UniformModalControl.localJets
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{Label : Type}
{s : WeightedClasses.StripData (P × TorusInverse.Plane)}
{α : ℝ}
{d : Label → ℕ → PrimaryODE.FrameData (P × ℝ)}
{t : Label → ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space}
{harmonic : ℤ}
{g : Label → ℕ → CommonCoverSolve.Geometry}
{L : Label → ℕ → ℝ}
{envelope : Label → ℕ → ℝ → ℝ}
{cells : Label → ℕ → TorusInverse.Frequency → Set (P × TorusInverse.Plane)}
[Countable Label]
[Nonempty Label]
(h : UniformModalControl s α d t harmonic g L envelope cells)
(hL : ∀ (l : Label) (n : ℕ), 0 < L l n)
(W : Label → ℕ → P × TorusInverse.Plane → ℝ)
(hW :
∀ (l : Label) (n : ℕ) (k : TorusInverse.Frequency),
∀ x ∈ s.domain, x ∈ cells l n k → envelope l n ((g l n).coordinates k x.2).2 ≤ W l n x)
:
PeriodizedWaveBounds.UniformLocalJets s (fun (l : Label) (n : ℕ) (x : P × TorusInverse.Plane) => √(s.zeta x) * W l n x)
α cells fun (l : Label) (n : ℕ) (k : TorusInverse.Frequency) => (t l n).linearData.copySolve (g l n) ⋯ k
noncomputable def
NavierStokes.ParticularCopyBounds.reindexedBase
{Label : Type}
{D : Type u_1}
(base : Label → LinearWaveBounds.WaveCoefficients D)
(e : ℕ → ℕ × Label)
:
Reindexed base, 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.ParticularCopyBounds.uniform_coefficients_jets
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{Label : Type}
[Countable Label]
[Nonempty Label]
{s : WeightedClasses.StripData (P × TorusInverse.Plane)}
{α : ℝ}
(base : Label → LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane))
(t : Label → ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space)
(source : Label → ℕ → P × TorusInverse.Plane → HarmonicCalculus.ComplexVector)
(g : Label → ℕ → CommonCoverSolve.Geometry)
(L : Label → ℕ → ℝ)
(hL : ∀ (l : Label) (n : ℕ), 0 < L l n)
(envelope : Label → ℕ → ℝ → ℝ)
(W : Label → ℕ → P × TorusInverse.Plane → ℝ)
(d : Label → ℕ → PrimaryODE.FrameData (P × ℝ))
(harmonic : ℤ)
(cells : Label → ℕ → TorusInverse.Frequency → Set (P × TorusInverse.Plane))
(hr :
UniformModalControl s α d (fun (l : Label) (n : ℕ) => ParticularWaveBounds.realData (t l n) (source l n)) harmonic g L
envelope cells)
(hi :
UniformModalControl s α d (fun (l : Label) (n : ℕ) => ParticularWaveBounds.imagData (t l n) (source l n)) harmonic g L
envelope cells)
(hW : ∀ (l : Label) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W l n x)
(hcompare :
∀ (l : Label) (n : ℕ) (k : TorusInverse.Frequency),
∀ x ∈ s.domain, x ∈ cells l n k → envelope l n ((g l n).coordinates k x.2).2 ≤ W l n x)
(hN :
PeriodizedWaveBounds.UniformLocalJets s (fun (x : Label) (x_1 : ℕ) (x_2 : P × TorusInverse.Plane) => 1) 0 cells
fun (l : Label) (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) =>
(t l n).normal (ParticularWaveBounds.nativePoint (g l n) k x))
(hNd :
PeriodizedWaveBounds.UniformLocalJets s (fun (x : Label) (x_1 : ℕ) (x_2 : P × TorusInverse.Plane) => 1) 0 cells
fun (l : Label) (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) =>
(t l n).normalDot (ParticularWaveBounds.nativePoint (g l n) k x))
(hA :
PeriodizedWaveBounds.UniformLocalJets s (fun (x : Label) (x_1 : ℕ) (x_2 : P × TorusInverse.Plane) => 1) 0 cells
fun (l : Label) (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) =>
(t l n).action (ParticularWaveBounds.nativePoint (g l n) k x))
(hf :
PeriodizedWaveBounds.UniformLocalJets s
(fun (l : Label) (n : ℕ) (x : P × TorusInverse.Plane) => √(s.zeta x) * W l n x) α cells
fun (l : Label) (n : ℕ) (x : TorusInverse.Frequency) => source l n)
{b M : ℝ}
(hb : 0 < b)
(hl :
∀ (l : Label) (n : ℕ) (k : TorusInverse.Frequency),
∀ x ∈ s.domain, x ∈ cells l n k → b ≤ ‖(t l n).normal (ParticularWaveBounds.nativePoint (g l n) k x)‖)
(hh :
∀ (l : Label) (n : ℕ) (k : TorusInverse.Frequency),
∀ x ∈ s.domain, x ∈ cells l n k → ‖(t l n).normal (ParticularWaveBounds.nativePoint (g l n) k x)‖ ≤ M)
(hfrequency : UniformPrimaryWeights.UniformBandBound s (1 / 2) fun (l : Label) (n : ℕ) => 1 / (base l).frequency n)
:
(PeriodizedWaveBounds.UniformLocalJets s (fun (l : Label) (n : ℕ) (x : P × TorusInverse.Plane) => √(s.zeta x) * W l n x)
α cells fun (l : Label) (n : ℕ) (k : TorusInverse.Frequency) =>
(ParticularWaveBounds.complexCopyCoefficients (base l) (t l) (source l) (g l) (fun (x : ℕ) => k) (L l) ⋯).amplitude
n) ∧ PeriodizedWaveBounds.UniformLocalJets s
(fun (l : Label) (n : ℕ) (x : P × TorusInverse.Plane) => √(s.zeta x) * W l n x) (α + 1 / 2) cells
fun (l : Label) (n : ℕ) (k : TorusInverse.Frequency) =>
(ParticularWaveBounds.complexCopyCoefficients (base l) (t l) (source l) (g l) (fun (x : ℕ) => k) (L l) ⋯).pressure n
Uniformity includes external countable spatial labels without changing their envelopes or selecting separate output constants.
theorem
NavierStokes.ParticularCopyBounds.uniform_coefficients_localized_jets
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{Label : Type}
[Countable Label]
[Nonempty Label]
{s : WeightedClasses.StripData (P × TorusInverse.Plane)}
{α : ℝ}
(base : Label → LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane))
(t : Label → ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space)
(source : Label → ℕ → P × TorusInverse.Plane → HarmonicCalculus.ComplexVector)
(g : Label → ℕ → CommonCoverSolve.Geometry)
(L : Label → ℕ → ℝ)
(hL : ∀ (l : Label) (n : ℕ), 0 < L l n)
(envelope : Label → ℕ → ℝ → ℝ)
(W : Label → ℕ → P × TorusInverse.Plane → ℝ)
(d : Label → ℕ → PrimaryODE.FrameData (P × ℝ))
(harmonic : ℤ)
(cells : Label → ℕ → TorusInverse.Frequency → Set (P × TorusInverse.Plane))
(hr :
UniformModalControl s α d (fun (l : Label) (n : ℕ) => ParticularWaveBounds.realData (t l n) (source l n)) harmonic g L
envelope cells)
(hi :
UniformModalControl s α d (fun (l : Label) (n : ℕ) => ParticularWaveBounds.imagData (t l n) (source l n)) harmonic g L
envelope cells)
(hW : ∀ (l : Label) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W l n x)
(hcompare :
∀ (l : Label) (n : ℕ) (k : TorusInverse.Frequency),
∀ x ∈ s.domain, x ∈ cells l n k → envelope l n ((g l n).coordinates k x.2).2 ≤ W l n x)
(hN :
PeriodizedWaveBounds.UniformLocalJets s (fun (x : Label) (x_1 : ℕ) (x_2 : P × TorusInverse.Plane) => 1) 0 cells
fun (l : Label) (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) =>
(t l n).normal (ParticularWaveBounds.nativePoint (g l n) k x))
(hNd :
PeriodizedWaveBounds.UniformLocalJets s (fun (x : Label) (x_1 : ℕ) (x_2 : P × TorusInverse.Plane) => 1) 0 cells
fun (l : Label) (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) =>
(t l n).normalDot (ParticularWaveBounds.nativePoint (g l n) k x))
(hA :
PeriodizedWaveBounds.UniformLocalJets s (fun (x : Label) (x_1 : ℕ) (x_2 : P × TorusInverse.Plane) => 1) 0 cells
fun (l : Label) (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) =>
(t l n).action (ParticularWaveBounds.nativePoint (g l n) k x))
(hf :
PeriodizedWaveBounds.UniformLocalJets s
(fun (l : Label) (n : ℕ) (x : P × TorusInverse.Plane) => √(s.zeta x) * W l n x) α cells
fun (l : Label) (n : ℕ) (x : TorusInverse.Frequency) => source l n)
{b M : ℝ}
(hb : 0 < b)
(hl :
∀ (l : Label) (n : ℕ) (k : TorusInverse.Frequency),
∀ x ∈ s.domain, x ∈ cells l n k → b ≤ ‖(t l n).normal (ParticularWaveBounds.nativePoint (g l n) k x)‖)
(hh :
∀ (l : Label) (n : ℕ) (k : TorusInverse.Frequency),
∀ x ∈ s.domain, x ∈ cells l n k → ‖(t l n).normal (ParticularWaveBounds.nativePoint (g l n) k x)‖ ≤ M)
(hfrequency : UniformPrimaryWeights.UniformBandBound s (1 / 2) fun (l : Label) (n : ℕ) => 1 / (base l).frequency n)
(cutoff : Label → TorusInverse.Frequency → ℕ → P × TorusInverse.Plane → ℝ)
(hcutoff :
PeriodizedWaveBounds.UniformLocalJets s (fun (x : Label) (x_1 : ℕ) (x_2 : P × TorusInverse.Plane) => 1) 0 cells
fun (l : Label) (n : ℕ) (k : TorusInverse.Frequency) => cutoff l k n)
:
(PeriodizedWaveBounds.UniformLocalJets s (fun (l : Label) (n : ℕ) (x : P × TorusInverse.Plane) => √(s.zeta x) * W l n x)
α cells fun (l : Label) (n : ℕ) (k : TorusInverse.Frequency) =>
((ParticularWaveBounds.complexCopyCoefficients (base l) (t l) (source l) (g l) (fun (x : ℕ) => k) (L l)
⋯).withCutoff
(cutoff l k)).amplitude
n) ∧ PeriodizedWaveBounds.UniformLocalJets s
(fun (l : Label) (n : ℕ) (x : P × TorusInverse.Plane) => √(s.zeta x) * W l n x) (α + 1 / 2) cells
fun (l : Label) (n : ℕ) (k : TorusInverse.Frequency) =>
((ParticularWaveBounds.complexCopyCoefficients (base l) (t l) (source l) (g l) (fun (x : ℕ) => k) (L l)
⋯).withCutoff
(cutoff l k)).pressure
n
theorem
NavierStokes.ParticularCopyBounds.jets_of_translate
{E : Type u_1}
{V : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{f g : E → V}
(a : E)
(he : ∀ (y : E), f (y + a) = g y)
(m : ℕ)
(x : E)
:
theorem
NavierStokes.ParticularCopyBounds.velocity_jets_deck
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
(t : CommonCoverSolve.TangentData P ProblemStatement.Space)
(source : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector)
(g : CommonCoverSolve.Geometry)
{a b : ℝ}
(hab : a ≤ b)
(hperiodic : ∀ (p : P), CommonCoverSolve.PeriodicAt source p)
(k q : TorusInverse.Frequency)
(m : ℕ)
(x : P × TorusInverse.Plane)
:
iteratedFDeriv ℝ m (ParticularWaveBounds.complexCopyVelocity t source g hab (k + CommonCoverSolve.coverIndex g.gap q))
(x + (0, TorusAverages.latticePoint q)) = iteratedFDeriv ℝ m (ParticularWaveBounds.complexCopyVelocity t source g hab k) x
Periodic translation preserves every full jet of the actual solution. The copy index moves by the genuine common-cover index map.
theorem
NavierStokes.ParticularCopyBounds.pressure_jets_deck
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
(t : CommonCoverSolve.TangentData P ProblemStatement.Space)
(source : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector)
(g : CommonCoverSolve.Geometry)
{a b : ℝ}
(hab : a ≤ b)
(hperiodic : ∀ (p : P), CommonCoverSolve.PeriodicAt source p)
(frequency : ℝ)
(k q : TorusInverse.Frequency)
(m : ℕ)
(x : P × TorusInverse.Plane)
:
iteratedFDeriv ℝ m
(ParticularWaveBounds.complexCopyPressure t source g hab (k + CommonCoverSolve.coverIndex g.gap q) frequency)
(x + (0, TorusAverages.latticePoint q)) = iteratedFDeriv ℝ m (ParticularWaveBounds.complexCopyPressure t source g hab k frequency) x
theorem
NavierStokes.ParticularCopyBounds.velocity_jets_zero_copy
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
(t : CommonCoverSolve.TangentData P ProblemStatement.Space)
(source : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector)
(g : CommonCoverSolve.Geometry)
(hgap : g.gap = 0)
{a b : ℝ}
(hab : a ≤ b)
(hperiodic : ∀ (p : P), CommonCoverSolve.PeriodicAt source p)
(q : TorusInverse.Frequency)
(m : ℕ)
(x : P × TorusInverse.Plane)
:
iteratedFDeriv ℝ m (ParticularWaveBounds.complexCopyVelocity t source g hab q) (x + (0, TorusAverages.latticePoint q)) = iteratedFDeriv ℝ m (ParticularWaveBounds.complexCopyVelocity t source g hab 0) x
A zero-gap cover permits reduction to the zero copy. For a refined cover the preceding deck theorem retains its actual index subgroup.
theorem
NavierStokes.ParticularCopyBounds.coefficient_jets_deck
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
(d : PrimaryODE.FrameData (P × ℝ))
(g : CommonCoverSolve.Geometry)
(harmonic : ℤ)
(k q : TorusInverse.Frequency)
(m : ℕ)
(x : (P × TorusInverse.Plane) × ℝ)
:
iteratedFDeriv ℝ m ((PrimaryCopyBridge.copyFrame d g (k + CommonCoverSolve.coverIndex g.gap q)).coefficient harmonic)
(x + ((0, TorusAverages.latticePoint q), 0)) = iteratedFDeriv ℝ m ((PrimaryCopyBridge.copyFrame d g k).coefficient harmonic) x
theorem
NavierStokes.ParticularCopyBounds.source_jets_deck
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
(source : P × TorusInverse.Plane → ProblemStatement.Space)
(g : CommonCoverSolve.Geometry)
(hperiodic : ∀ (p : P), CommonCoverSolve.PeriodicAt source p)
(k q : TorusInverse.Frequency)
(m : ℕ)
(x : (P × TorusInverse.Plane) × ℝ)
:
iteratedFDeriv ℝ m (PrimaryCopyBridge.copySource source g (k + CommonCoverSolve.coverIndex g.gap q))
(x + ((0, TorusAverages.latticePoint q), 0)) = iteratedFDeriv ℝ m (PrimaryCopyBridge.copySource source g k) x
theorem
NavierStokes.ParticularCopyBounds.synthesis_jets_deck
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
(d : PrimaryODE.FrameData (P × ℝ))
(g : CommonCoverSolve.Geometry)
(i : Fin 2)
(k q : TorusInverse.Frequency)
(m : ℕ)
(x : (P × TorusInverse.Plane) × ℝ)
:
iteratedFDeriv ℝ m
(PrimaryPulseBounds.synthesisColumn (PrimaryCopyBridge.copyFrame d g (k + CommonCoverSolve.coverIndex g.gap q)) i)
(x + ((0, TorusAverages.latticePoint q), 0)) = iteratedFDeriv ℝ m (PrimaryPulseBounds.synthesisColumn (PrimaryCopyBridge.copyFrame d g k) i) x
theorem
NavierStokes.ParticularCopyBounds.forcing_jets_deck
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
(d : PrimaryODE.FrameData (P × ℝ))
(source : P × TorusInverse.Plane → ProblemStatement.Space)
(g : CommonCoverSolve.Geometry)
(hperiodic : ∀ (p : P), CommonCoverSolve.PeriodicAt source p)
(k q : TorusInverse.Frequency)
(m : ℕ)
(x : (P × TorusInverse.Plane) × ℝ)
:
iteratedFDeriv ℝ m
((PrimaryCopyBridge.copyFrame d g (k + CommonCoverSolve.coverIndex g.gap q)).forcing
(PrimaryCopyBridge.copySource source g (k + CommonCoverSolve.coverIndex g.gap q)))
(x + ((0, TorusAverages.latticePoint q), 0)) = iteratedFDeriv ℝ m ((PrimaryCopyBridge.copyFrame d g k).forcing (PrimaryCopyBridge.copySource source g k)) x