Uniform estimates for the chosen primary waves

All fields below use ActualPrimary.choice. The estimates retain the moving edge weight and the actual pulse envelope. Constants precede the orientation, spatial label, band, and lattice copy.

@[reducible, inline]

abbrev NavierStokes.ActualPrimaryBounds.Native : Type

Native: an abbreviation for ActualSignedGeometry.Native.

Equations

• NavierStokes.ActualPrimaryBounds.Native = NavierStokes.ActualSignedGeometry.Native

@[reducible, inline]

abbrev NavierStokes.ActualPrimaryBounds.Point : Type

Point: an abbreviation for LocalSignedRequest.Point.

Equations

• NavierStokes.ActualPrimaryBounds.Point = NavierStokes.LocalSignedRequest.Point

noncomputable def NavierStokes.ActualPrimaryBounds.region : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)

Region, given by ActualSignedGeometry.standardSlowRegion ActualPrimary.outgoing.data.h_pos ActualPrimary.outgoing.data.h_lt_half.

Equations

• NavierStokes.ActualPrimaryBounds.region = NavierStokes.ActualSignedGeometry.standardSlowRegion NavierStokes.ActualPrimaryBounds.region._proof_1 NavierStokes.ActualPrimaryBounds.region._proof_3

noncomputable def NavierStokes.ActualPrimaryBounds.strip : WeightedClasses.StripData Point

Strip, given by BaseContextAssembly.nativeStrip ActualPrimary.nominal region.

Equations

• NavierStokes.ActualPrimaryBounds.strip = NavierStokes.BaseContextAssembly.nativeStrip NavierStokes.CorrectionInitialization.ActualPrimary.nominal NavierStokes.ActualPrimaryBounds.region

noncomputable def NavierStokes.ActualPrimaryBounds.nativeStrip : WeightedClasses.StripData Native

Native strip, given by ActualSignedGeometry.viewStrip ActualPrimary.nominal region id.

Equations

• NavierStokes.ActualPrimaryBounds.nativeStrip = NavierStokes.ActualSignedGeometry.viewStrip NavierStokes.CorrectionInitialization.ActualPrimary.nominal NavierStokes.ActualPrimaryBounds.region id

@[reducible, inline]

abbrev NavierStokes.ActualPrimaryBounds.SignedLabel (B N0 : ℕ) : Type

Signed label: an abbreviation for Fin 2 × ActualPrimary.Label B N0.

Equations

• NavierStokes.ActualPrimaryBounds.SignedLabel B N0 = (Fin 2 × NavierStokes.CorrectionInitialization.ActualPrimary.Label B N0)

theorem NavierStokes.ActualPrimaryBounds.outer_velocity_jets (B N0 : ℕ) (j : Fin 2) : PrimaryCopyBounds.NativeJets (NativeBandExtension.radialDomain CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared) (NativeBandExtension.velocityWeight CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared ⋯ j) fun (L : PrimaryGeometryAssembly.Index CorrectionInitialization.ActualPrimary.profile.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N) => CorrectionInitialization.ActualPrimary.outerRawVelocity j L

The outer slot localization is differentiated before periodization.

theorem NavierStokes.ActualPrimaryBounds.outer_pressure_jets (B N0 : ℕ) (j : Fin 2) : PrimaryCopyBounds.NativeJets (NativeBandExtension.radialDomain CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared) (NativeBandExtension.pressureWeight CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared ⋯ j) fun (L : PrimaryGeometryAssembly.Index CorrectionInitialization.ActualPrimary.profile.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N) => CorrectionInitialization.ActualPrimary.outerRawPressure j L

theorem NavierStokes.ActualPrimaryBounds.attached_velocity_jets (B N0 : ℕ) (j : Fin 2) : PrimaryCopyBounds.NativeJets (NativeBandExtension.radialDomain CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared) (NativeBandExtension.velocityWeight CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared ⋯ j) fun (L : PrimaryGeometryAssembly.Index CorrectionInitialization.ActualPrimary.profile.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N) => CorrectionInitialization.ActualPrimary.attachedRawVelocity j L

The annular attachment is equal to the native field on the entire open radial domain, including flat dyadic and transverse boundaries.

theorem NavierStokes.ActualPrimaryBounds.attached_pressure_jets (B N0 : ℕ) (j : Fin 2) : PrimaryCopyBounds.NativeJets (NativeBandExtension.radialDomain CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared) (NativeBandExtension.pressureWeight CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared ⋯ j) fun (L : PrimaryGeometryAssembly.Index CorrectionInitialization.ActualPrimary.profile.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N) => CorrectionInitialization.ActualPrimary.attachedRawPressure j L

theorem NavierStokes.ActualPrimaryBounds.attached_velocity_signed_jets (B N0 : ℕ) : PrimaryCopyBounds.NativeJets (PrimaryCopyBounds.signDomain (NativeBandExtension.radialDomain CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared)) (fun (l : Fin 2 × PrimaryGeometryAssembly.Index CorrectionInitialization.ActualPrimary.profile.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N) => NativeBandExtension.velocityWeight CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared ⋯ l.1 l.2) fun (l : Fin 2 × PrimaryGeometryAssembly.Index CorrectionInitialization.ActualPrimary.profile.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N) => CorrectionInitialization.ActualPrimary.attachedRawVelocity l.1 l.2

Both signs share the same finite-jet constants.

theorem NavierStokes.ActualPrimaryBounds.attached_pressure_signed_jets (B N0 : ℕ) : PrimaryCopyBounds.NativeJets (PrimaryCopyBounds.signDomain (NativeBandExtension.radialDomain CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared)) (fun (l : Fin 2 × PrimaryGeometryAssembly.Index CorrectionInitialization.ActualPrimary.profile.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N) => NativeBandExtension.pressureWeight CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared ⋯ l.1 l.2) fun (l : Fin 2 × PrimaryGeometryAssembly.Index CorrectionInitialization.ActualPrimary.profile.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N) => CorrectionInitialization.ActualPrimary.attachedRawPressure l.1 l.2

noncomputable def NavierStokes.ActualPrimaryBounds.spatialLabel {B N0 : ℕ} (l : SignedLabel B N0) : SlotColoring.Label

Spatial label, given by PartitionedCovariance.signedLabel (PrimaryGeometryAssembly.label ActualPrimary.nominal l.2) l.1.

Equations

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

theorem NavierStokes.ActualPrimaryBounds.label_large {B N0 : ℕ} (l : SignedLabel B N0) : 4 ≤ (spatialLabel l).1

noncomputable def NavierStokes.ActualPrimaryBounds.near {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) : Prop

Near, given by 1 ≤ n ∧ BaseChartJets.cellBand l.2 ∈ CommonWindow.levels n.

Equations

• NavierStokes.ActualPrimaryBounds.near l n = (1 ≤ n ∧ NavierStokes.BaseChartJets.cellBand l.2 ∈ NavierStokes.CorrectionInitialization.CommonWindow.levels n)

theorem NavierStokes.ActualPrimaryBounds.near_distance {B N0 : ℕ} {l : SignedLabel B N0} {n : ℕ} (hn : near l n) : n ≤ (spatialLabel l).1 + 4 ∧ (spatialLabel l).1 ≤ n + 4

theorem NavierStokes.ActualPrimaryBounds.geometry_eq {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) : CorrectionInitialization.ActualPrimary.chartGeometry n l.1 l.2 = ActualSignedGeometry.slotGeometry CorrectionInitialization.ActualPrimary.slots CorrectionInitialization.ActualPrimary.vectors_det (spatialLabel l) (ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) - CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)

theorem NavierStokes.ActualPrimaryBounds.clock_eq {B N0 : ℕ} (l : SignedLabel B N0) : CorrectionInitialization.ActualPrimary.clockWindow l.2 = ActualSignedGeometry.clockWindow CorrectionInitialization.ActualPrimary.slots (BaseChartJets.cellBand l.2)

noncomputable def NavierStokes.ActualPrimaryBounds.copyPoint {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : TorusInverse.Frequency) : Native → Native

Copy point, constructed using ActualSignedGeometry.copyPoint.

Equations

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

noncomputable def NavierStokes.ActualPrimaryBounds.copyLinear {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) : Native →L[ℝ] Native

Copy linear, constructed using ActualSignedGeometry.copyLinear.

Equations

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

theorem NavierStokes.ActualPrimaryBounds.copyPoint_affine {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : TorusInverse.Frequency) (x : Native) : copyPoint l n k x = (copyLinear l n) x + copyPoint l n k 0

theorem NavierStokes.ActualPrimaryBounds.copyPoint_smooth {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : TorusInverse.Frequency) : ContDiff ℝ (↑⊤) (copyPoint l n k)

noncomputable def NavierStokes.ActualPrimaryBounds.copyCost : ℝ

Copy cost, constructed using ActualSignedGeometry.slowChangeCost.

Equations

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

theorem NavierStokes.ActualPrimaryBounds.copyCost_one : 1 ≤ copyCost

theorem NavierStokes.ActualPrimaryBounds.copyLinear_bound {B N0 : ℕ} {l : SignedLabel B N0} {n : ℕ} (hn : near l n) : ‖copyLinear l n‖ ≤ copyCost * nativeStrip.slow n

noncomputable def NavierStokes.ActualPrimaryBounds.copyCells {B N0 : ℕ} (l : SignedLabel B N0) : PeriodizedWaveBounds.Cells Native TorusInverse.Frequency

Copy cells, constructed using PeriodizedWaveBounds.nativeCells.

Equations

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

noncomputable def NavierStokes.ActualPrimaryBounds.pulseEnvelope {B N0 : ℕ} (l : SignedLabel B N0) : ℝ → ℝ

Pulse envelope, constructed using PrimaryPulseBounds.referenceP.

Equations

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

noncomputable def NavierStokes.ActualPrimaryBounds.envelope {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (x : Native) : ℝ

Envelope, constructed using WaveEnvelopeTransport.copyEnvelope.

Equations

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

theorem NavierStokes.ActualPrimaryBounds.envelope_nonneg {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (x : Native) : 0 ≤ envelope l n x

theorem NavierStokes.ActualPrimaryBounds.envelope_copy {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : TorusInverse.Frequency) {x : Native} (hx : x ∈ (copyCells l).carrier n k) : envelope l n x = pulseEnvelope l (copyPoint l n k x).2.2

theorem NavierStokes.ActualPrimaryBounds.copyPoint_radial {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : TorusInverse.Frequency) {x : Native} (hx : x ∈ nativeStrip.domain) : copyPoint l n k x ∈ NativeBandExtension.radialInterior CorrectionInitialization.ActualPrimary.nominal

theorem NavierStokes.ActualPrimaryBounds.copyPoint_weight {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : TorusInverse.Frequency) {x : Native} (hx : x ∈ nativeStrip.domain) : PrimaryTargetBounds.movingWeight CorrectionInitialization.ActualPrimary.nominal (copyPoint l n k x).1 = nativeStrip.zeta x

theorem NavierStokes.ActualPrimaryBounds.copyPoint_growth {B N0 : ℕ} {l : SignedLabel B N0} {n : ℕ} (hn : near l n) (k : TorusInverse.Frequency) {x : Native} (hx : x ∈ nativeStrip.domain) : (NativeBandExtension.radialDomain CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared).growth l.2 (copyPoint l n k x) ≤ 25 * nativeStrip.growth n x

theorem NavierStokes.ActualPrimaryBounds.epsilon_power_window {n m : ℕ} (hnm : n ≤ m + 4) (hmn : m ≤ n + 4) (α : ℝ) : ChartScales.epsilon CorrectionInitialization.ActualPrimary.h m ^ α ≤ ActualSignedGeometry.powerBound (-(CorrectionInitialization.ActualPrimary.h * α)) * ChartScales.epsilon CorrectionInitialization.ActualPrimary.h n ^ α

noncomputable def NavierStokes.ActualPrimaryBounds.nativeWeight {B N0 : ℕ} (α : ℝ) (l : SignedLabel B N0) (x : Native) : ℝ

Native weight, constructed using ChartScales.epsilon.

Equations

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

noncomputable def NavierStokes.ActualPrimaryBounds.coefficientScale {B N0 : ℕ} (a : ℝ) (l : SignedLabel B N0) (n : ℕ) : ℝ

Coefficient scale, given by PhysicalParticularWave.ratioPower (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand l.2)) a.

Equations

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

theorem NavierStokes.ActualPrimaryBounds.coefficientScale_pos {B N0 : ℕ} (a : ℝ) (l : SignedLabel B N0) (n : ℕ) : 0 < coefficientScale a l n

noncomputable def NavierStokes.ActualPrimaryBounds.copied {B N0 : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℝ) (f : SignedLabel B N0 → Native → E) (l : SignedLabel B N0) (n : ℕ) (k : TorusInverse.Frequency) (x : Native) : E

Copied as an element of E.

Equations

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

theorem NavierStokes.ActualPrimaryBounds.copied_uniformLocalJets {B N0 : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a α : ℝ} {f : SignedLabel B N0 → Native → E} (hf : PrimaryCopyBounds.NativeJets (PrimaryCopyBounds.signDomain (NativeBandExtension.radialDomain CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared)) (nativeWeight α) f) : PeriodizedWaveBounds.UniformLocalJets nativeStrip (fun (l : SignedLabel B N0) (n : ℕ) (x : Native) => √(nativeStrip.zeta x) * envelope l n x) α (fun (l : SignedLabel B N0) => (copyCells l).carrier) (copied a f)

Active-window comparisons are required only where the copy is present. No comparison is imposed between remote band/label pairs.

theorem NavierStokes.ActualPrimaryBounds.velocityWeight_eq {B N0 : ℕ} (l : SignedLabel B N0) (x : Native) : NativeBandExtension.velocityWeight CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared ⋯ l.1 l.2 x = nativeWeight (1 / 2) l x

theorem NavierStokes.ActualPrimaryBounds.pressureWeight_eq {B N0 : ℕ} (l : SignedLabel B N0) (x : Native) : NativeBandExtension.pressureWeight CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared ⋯ l.1 l.2 x = nativeWeight 1 l x

theorem NavierStokes.ActualPrimaryBounds.complex_velocity_native_jets {B N0 : ℕ} : PrimaryCopyBounds.NativeJets (PrimaryCopyBounds.signDomain (NativeBandExtension.radialDomain CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared)) (nativeWeight (1 / 2)) fun (l : Fin 2 × PrimaryGeometryAssembly.Index CorrectionInitialization.ActualPrimary.profile.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N) (x : NativeBandExtension.Native) => CurlClassBounds.complexify (CorrectionInitialization.ActualPrimary.attachedRawVelocity l.1 l.2 x)

theorem NavierStokes.ActualPrimaryBounds.pressure_native_jets {B N0 : ℕ} : PrimaryCopyBounds.NativeJets (PrimaryCopyBounds.signDomain (NativeBandExtension.radialDomain CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared)) (nativeWeight 1) fun (l : Fin 2 × PrimaryGeometryAssembly.Index CorrectionInitialization.ActualPrimary.profile.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N) => CorrectionInitialization.ActualPrimary.attachedRawPressure l.1 l.2

noncomputable def NavierStokes.ActualPrimaryBounds.periodized {B N0 : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℝ) (f : SignedLabel B N0 → Native → E) (l : SignedLabel B N0) (n : ℕ) : Native → E

Periodized, given by PeriodizedWaveBounds.copySum (copied a f l n).

Equations

• NavierStokes.ActualPrimaryBounds.periodized a f l n = NavierStokes.PeriodizedWaveBounds.copySum (NavierStokes.ActualPrimaryBounds.copied a f l n)

theorem NavierStokes.ActualPrimaryBounds.periodized_uniform {B N0 : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a α : ℝ} {f : SignedLabel B N0 → Native → E} (hf : PrimaryCopyBounds.NativeJets (PrimaryCopyBounds.signDomain (NativeBandExtension.radialDomain CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared)) (nativeWeight α) f) (hs : ∀ (l : SignedLabel B N0) (x : Native), f l x ≠ 0 → x.2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.2).core) : LabelSumBounds.UniformWaveClass nativeStrip envelope α (periodized a f)

theorem NavierStokes.ActualPrimaryBounds.periodized_velocity_uniform {B N0 : ℕ} : LabelSumBounds.UniformWaveClass nativeStrip envelope (1 / 2) (periodized (CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) fun (l : SignedLabel B N0) (x : Native) => CurlClassBounds.complexify (CorrectionInitialization.ActualPrimary.attachedRawVelocity l.1 l.2 x))

theorem NavierStokes.ActualPrimaryBounds.periodized_pressure_uniform {B N0 : ℕ} : LabelSumBounds.UniformWaveClass nativeStrip envelope 1 (periodized (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) fun (l : SignedLabel B N0) => CorrectionInitialization.ActualPrimary.attachedRawPressure l.1 l.2)

theorem NavierStokes.ActualPrimaryBounds.near_of_closed_band {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) {p : PhaseCalculus.Slow} (hp : p ∈ BaseContextAssembly.slowCarrier CorrectionInitialization.ActualPrimary.nominal region) (hq : SimilarityHomogeneity.chartQ CorrectionInitialization.ActualPrimary.h ((ActualSignedGeometry.slowChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand l.2))) p) ∈ Set.Icc (1 / 2) 2) : near l n

A nonzero closed native dyadic band meets only the actual finite two-level window. The stronger four-level estimates therefore apply.

theorem NavierStokes.ActualPrimaryBounds.attached_zero_inactive {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) {p : PhaseCalculus.Slow} (hp : p ∈ BaseContextAssembly.slowCarrier CorrectionInitialization.ActualPrimary.nominal region) (hn : ¬near l n) (Y : TorusInverse.Plane) : CorrectionInitialization.ActualPrimary.attachedRawVelocity l.1 l.2 ((ActualSignedGeometry.slowChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand l.2))) p, Y) = 0 ∧ CorrectionInitialization.ActualPrimary.attachedRawPressure l.1 l.2 ((ActualSignedGeometry.slowChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand l.2))) p, Y) = 0

theorem NavierStokes.ActualPrimaryBounds.coefficientScale_eq {B N0 : ℕ} (a : ℝ) (l : SignedLabel B N0) (n : ℕ) : coefficientScale a l n = ChartScales.Q n ^ a * ChartScales.Q (BaseChartJets.cellBand l.2) ^ (-a)

theorem NavierStokes.ActualPrimaryBounds.periodized_velocity_eq {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) {x : Native} (hx : x ∈ nativeStrip.domain) (θ : ℝ) : periodized (CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) (fun (l : SignedLabel B N0) (y : Native) => CurlClassBounds.complexify (CorrectionInitialization.ActualPrimary.attachedRawVelocity l.1 l.2 y)) l n x = (CorrectionInitialization.ActualPrimary.chartCoefficients l.1 l.2).amplitude n (ActualSignedGeometry.meanEquiv x, θ)

theorem NavierStokes.ActualPrimaryBounds.periodized_pressure_eq {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) {x : Native} (hx : x ∈ nativeStrip.domain) (θ : ℝ) : periodized (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) (fun (l : SignedLabel B N0) => CorrectionInitialization.ActualPrimary.attachedRawPressure l.1 l.2) l n x = (CorrectionInitialization.ActualPrimary.chartCoefficients l.1 l.2).pressure n (ActualSignedGeometry.meanEquiv x, θ)

theorem NavierStokes.ActualPrimaryBounds.uniform_lift {D E ι : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ι → ℕ → D → ℝ} {α : ℝ} {f : ι → ℕ → D → E} (hf : LabelSumBounds.UniformClass s w α f) : LabelSumBounds.UniformClass (HarmonicWaveInteraction.productStrip s) (fun (l : ι) (n : ℕ) (x : D × ℝ) => w l n x.1) α fun (l : ι) (n : ℕ) (x : D × ℝ) => f l n x.1

noncomputable def NavierStokes.ActualPrimaryBounds.fullEnvelope {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (x : CorrectionInitialization.ActualPrimary.FullPoint) : ℝ

Full envelope, given by envelope l n (ActualSignedGeometry.meanEquiv.symm x.1).

Equations

• NavierStokes.ActualPrimaryBounds.fullEnvelope l n x = NavierStokes.ActualPrimaryBounds.envelope l n (NavierStokes.ActualSignedGeometry.meanEquiv.symm x.1)

theorem NavierStokes.ActualPrimaryBounds.chart_amplitude_uniform {B N0 : ℕ} : LabelSumBounds.UniformWaveClass (HarmonicWaveInteraction.productStrip strip) fullEnvelope (1 / 2) fun (l : SignedLabel B N0) => (CorrectionInitialization.ActualPrimary.chartCoefficients l.1 l.2).amplitude

theorem NavierStokes.ActualPrimaryBounds.chart_pressure_uniform {B N0 : ℕ} : LabelSumBounds.UniformWaveClass (HarmonicWaveInteraction.productStrip strip) fullEnvelope 1 fun (l : SignedLabel B N0) => (CorrectionInitialization.ActualPrimary.chartCoefficients l.1 l.2).pressure

noncomputable def NavierStokes.ActualPrimaryBounds.timeProjection {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) : Native →L[ℝ] ℝ

Time projection as an element of Native →L[ℝ] ℝ.

Equations

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

theorem NavierStokes.ActualPrimaryBounds.timeProjection_norm {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) : ‖timeProjection L‖ ≤ (CorrectionInitialization.ActualPrimary.choice B N0).prepared.M

theorem NavierStokes.ActualPrimaryBounds.gaussian_polynomial {B N0 : ℕ} : PhaseJetBounds.PolynomialJets (PrimaryCopyBounds.signDomain (NativeBandExtension.radialDomain CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared)).toDomain fun (l : SignedLabel B N0) => CorrectionInitialization.ActualPrimary.gaussian l.2

The fixed compact Gaussian profile has uniform jets after the actual slot rescaling, on the full radial domain.

noncomputable def NavierStokes.ActualPrimaryBounds.cutNativeVelocity {B N0 : ℕ} (l : SignedLabel B N0) (x : Native) : HarmonicCalculus.ComplexVector

Cut native velocity, given by ActualPrimary.gaussian l.2 x • CurlClassBounds.complexify (ActualPrimary.attachedRawVelocity l.1 l.2 x).

Equations

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

noncomputable def NavierStokes.ActualPrimaryBounds.cutNativePressure {B N0 : ℕ} (l : SignedLabel B N0) (x : Native) : ℂ

Cut native pressure, given by ActualPrimary.gaussian l.2 x • ActualPrimary.attachedRawPressure l.1 l.2 x.

Equations

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

theorem NavierStokes.ActualPrimaryBounds.cut_native_velocity_jets {B N0 : ℕ} : PrimaryCopyBounds.NativeJets (PrimaryCopyBounds.signDomain (NativeBandExtension.radialDomain CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared)) (nativeWeight (1 / 2)) cutNativeVelocity

theorem NavierStokes.ActualPrimaryBounds.cut_native_pressure_jets {B N0 : ℕ} : PrimaryCopyBounds.NativeJets (PrimaryCopyBounds.signDomain (NativeBandExtension.radialDomain CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared)) (nativeWeight 1) cutNativePressure

theorem NavierStokes.ActualPrimaryBounds.periodized_cut_velocity_uniform {B N0 : ℕ} : LabelSumBounds.UniformWaveClass nativeStrip envelope (1 / 2) (periodized (CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) cutNativeVelocity)

theorem NavierStokes.ActualPrimaryBounds.periodized_cut_pressure_uniform {B N0 : ℕ} : LabelSumBounds.UniformWaveClass nativeStrip envelope 1 (periodized (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) cutNativePressure)

theorem NavierStokes.ActualPrimaryBounds.gaussian_on_copy {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (hn : near l n) (k : TorusInverse.Frequency) (x : Native) (θ : ℝ) (hc : (copyPoint l n k x).2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.2).core) : CorrectionInitialization.ActualPrimary.chartCutoff l.1 l.2 n (ActualSignedGeometry.meanEquiv x, θ) = CorrectionInitialization.ActualPrimary.gaussian l.2 (copyPoint l n k x)

theorem NavierStokes.ActualPrimaryBounds.periodized_cut_eq {B N0 : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℝ) (f : SignedLabel B N0 → Native → E) (hs : ∀ (l : SignedLabel B N0) (x : Native), f l x ≠ 0 → x.2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.2).core) (l : SignedLabel B N0) (n : ℕ) (x : Native) (θ : ℝ) : periodized a (fun (l : SignedLabel B N0) (y : Native) => CorrectionInitialization.ActualPrimary.gaussian l.2 y • f l y) l n x = CorrectionInitialization.ActualPrimary.chartCutoff l.1 l.2 n (ActualSignedGeometry.meanEquiv x, θ) • periodized a f l n x

theorem NavierStokes.ActualPrimaryBounds.chart_cut_amplitude_uniform {B N0 : ℕ} : LabelSumBounds.UniformWaveClass (HarmonicWaveInteraction.productStrip strip) fullEnvelope (1 / 2) fun (l : SignedLabel B N0) => ((CorrectionInitialization.ActualPrimary.chartCoefficients l.1 l.2).withCutoff (CorrectionInitialization.ActualPrimary.chartCutoff l.1 l.2)).amplitude

theorem NavierStokes.ActualPrimaryBounds.chart_cut_pressure_uniform {B N0 : ℕ} : LabelSumBounds.UniformWaveClass (HarmonicWaveInteraction.productStrip strip) fullEnvelope 1 fun (l : SignedLabel B N0) => ((CorrectionInitialization.ActualPrimary.chartCoefficients l.1 l.2).withCutoff (CorrectionInitialization.ActualPrimary.chartCutoff l.1 l.2)).pressure

theorem NavierStokes.ActualPrimaryBounds.envelope_le_one {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (x : Native) : envelope l n x ≤ 1

theorem NavierStokes.ActualPrimaryBounds.fullEnvelope_nonneg {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (x : CorrectionInitialization.ActualPrimary.FullPoint) : 0 ≤ fullEnvelope l n x

theorem NavierStokes.ActualPrimaryBounds.fullEnvelope_le_one {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (x : CorrectionInitialization.ActualPrimary.FullPoint) : fullEnvelope l n x ≤ 1

noncomputable def NavierStokes.ActualPrimaryBounds.meanEnvelope {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (x : Point) : ℝ

Mean envelope, given by fullEnvelope l n (x, 0).

Equations

• NavierStokes.ActualPrimaryBounds.meanEnvelope l n x = NavierStokes.ActualPrimaryBounds.fullEnvelope l n (x, 0)

noncomputable def NavierStokes.ActualPrimaryBounds.angularFrequency {B N0 : ℕ} (l : SignedLabel B N0) (_n : ℕ) : ℤ

Angular frequency, constructed using PrimaryGeometryAssembly.angularMode.

Equations

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

noncomputable def NavierStokes.ActualPrimaryBounds.phase {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (x : Point) : ℝ

Phase, given by (ActualPrimary.chartCoefficients l.1 l.2).phase n (x, 0).

Equations

• NavierStokes.ActualPrimaryBounds.phase l n x = (NavierStokes.CorrectionInitialization.ActualPrimary.chartCoefficients l.1 l.2).phase n (x, 0)

theorem NavierStokes.ActualPrimaryBounds.tangent_block_uniform {B N0 : ℕ} : (∀ (i : Fin 3) (m : ℤ), LabelSumBounds.UniformWaveClass strip meanEnvelope (1 / 2) fun (l : SignedLabel B N0) (n : ℕ) (x : Point) => (((CorrectionInitialization.ActualPrimary.piece region l.1 l.2).tangentBlock (phase l) (angularFrequency l)).velocity n i).coeff m x) ∧ ∀ (m : ℤ), LabelSumBounds.UniformWaveClass strip meanEnvelope 1 fun (l : SignedLabel B N0) (n : ℕ) (x : Point) => (((CorrectionInitialization.ActualPrimary.piece region l.1 l.2).tangentBlock (phase l) (angularFrequency l)).pressure n).coeff m x

@[reducible, inline]

abbrev NavierStokes.ActualPrimaryBounds.CopyIndex (B N0 : ℕ) : Type

Copy index: an abbreviation for SignedLabel B N0 × TorusInverse.Frequency.

Equations

• NavierStokes.ActualPrimaryBounds.CopyIndex B N0 = (NavierStokes.ActualPrimaryBounds.SignedLabel B N0 × NavierStokes.TorusInverse.Frequency)

noncomputable def NavierStokes.ActualPrimaryBounds.fullCopy {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : TorusInverse.Frequency) (x : CorrectionInitialization.ActualPrimary.FullPoint) : Native

Full copy, given by copyPoint l n k (ActualSignedGeometry.meanEquiv.symm x.1).

Equations

• NavierStokes.ActualPrimaryBounds.fullCopy l n k x = NavierStokes.ActualPrimaryBounds.copyPoint l n k (NavierStokes.ActualSignedGeometry.meanEquiv.symm x.1)

noncomputable def NavierStokes.ActualPrimaryBounds.controlCell {B N0 : ℕ} (n : ℕ) (i : CopyIndex B N0) : Set CorrectionInitialization.ActualPrimary.FullPoint

Control cell as an element of Set ActualPrimary.FullPoint.

Equations

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

noncomputable def NavierStokes.ActualPrimaryBounds.fullStrip : WeightedClasses.StripData CorrectionInitialization.ActualPrimary.FullPoint

Full strip, given by HarmonicWaveInteraction.productStrip strip.

Equations

• NavierStokes.ActualPrimaryBounds.fullStrip = NavierStokes.HarmonicWaveInteraction.productStrip NavierStokes.ActualPrimaryBounds.strip

noncomputable def NavierStokes.ActualPrimaryBounds.nativeOfFull : CorrectionInitialization.ActualPrimary.FullPoint →L[ℝ] Native

Native of full, given by ActualSignedGeometry.meanEquiv.symm.toContinuousLinearEquiv.toContinuousLinearMap.comp (ContinuousLinearMap.fst ℝ Point ℝ).

Equations

• NavierStokes.ActualPrimaryBounds.nativeOfFull = ↑↑NavierStokes.ActualSignedGeometry.meanEquiv.symm ∘SL ContinuousLinearMap.fst ℝ NavierStokes.ActualPrimaryBounds.Point ℝ

theorem NavierStokes.ActualPrimaryBounds.nativeOfFull_norm : ‖nativeOfFull‖ ≤ 1

noncomputable def NavierStokes.ActualPrimaryBounds.slotOfNative : Native →L[ℝ] PhaseCalculus.Slow × ℝ

Slot of native as an element of Native →L[ℝ] (PhaseCalculus.Slow × ℝ).

Equations

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

theorem NavierStokes.ActualPrimaryBounds.slotOfNative_norm : ‖slotOfNative‖ ≤ 1

noncomputable def NavierStokes.ActualPrimaryBounds.slotLinear {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) : CorrectionInitialization.ActualPrimary.FullPoint →L[ℝ] PhaseCalculus.Slow × ℝ

Slot linear, given by slotOfNative.comp ((copyLinear l n).comp nativeOfFull).

Equations

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

theorem NavierStokes.ActualPrimaryBounds.slotLinear_bound {B N0 : ℕ} {l : SignedLabel B N0} {n : ℕ} (hn : near l n) : ‖slotLinear l n‖ ≤ copyCost * fullStrip.slow n

theorem NavierStokes.ActualPrimaryBounds.slotCopy_affine {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : TorusInverse.Frequency) (x : CorrectionInitialization.ActualPrimary.FullPoint) : ((fullCopy l n k x).1, (fullCopy l n k x).2.2) = (slotLinear l n) x + slotOfNative (copyPoint l n k 0)

theorem NavierStokes.ActualPrimaryBounds.control_maps {B N0 : ℕ} {i : CopyIndex B N0} {n : ℕ} {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ fullStrip.domain) (hc : x ∈ controlCell n i) : ((fullCopy i.1 n i.2 x).1, (fullCopy i.1 n i.2 x).2.2) ∈ (ActualPhaseDefect.reducedJetDomain ActualPhaseDefect.paddedRegion).carrier i.1

theorem NavierStokes.ActualPrimaryBounds.polynomial_on_control {B N0 : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : SignedLabel B N0 → PhaseCalculus.Slow × ℝ → E} (hf : PhaseJetBounds.PolynomialJets (ActualPhaseDefect.reducedJetDomain ActualPhaseDefect.paddedRegion) f) : LocalizedWaveBounds.LocalUnweighted fullStrip controlCell 0 fun (n : ℕ) (i : CopyIndex B N0) (x : CorrectionInitialization.ActualPrimary.FullPoint) => f i.1 ((fullCopy i.1 n i.2 x).1, (fullCopy i.1 n i.2 x).2.2)

Actual affine pullback of polynomial native jets, with constants uniform over the active label, chart, and lattice copy.

noncomputable def NavierStokes.ActualPrimaryBounds.jointPhase {B N0 : ℕ} : PhaseJetBounds.PhaseFamily (SignedLabel B N0)

Joint phase, bundling epsilon, p, pz, x0 and the required compatibility proofs.

Equations

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

theorem NavierStokes.ActualPrimaryBounds.native_normal_polynomial {B N0 : ℕ} : PhaseJetBounds.PolynomialJets (ActualPhaseDefect.reducedJetDomain ActualPhaseDefect.paddedRegion) jointPhase.normal

theorem NavierStokes.ActualPrimaryBounds.context_normal_swap (c : CorrectionState.Context Point) (s : WeightedClasses.StripData Point) (a : LinearWaveBounds.WaveCoefficients CorrectionInitialization.ActualPrimary.FullPoint) (n : ℕ) (G : PhysicalResidualBridge.ScaledGraph) (hG : PhysicalResidualTZ.MatchesAtTZ c.operators G n) (hepsilon : s.epsilon n = c.operators.epsilon n) (hradius : a.radius n = fun (x : CorrectionInitialization.ActualPrimary.FullPoint) => x.1.1) (Φ : PhysicalResidualBridge.Cylinder → ℝ) (hphase : a.phase n = fun (y : PhysicalResidualTZ.Cylinder) => Φ (PhysicalResidualTZ.swapCylinder y)) (x : CorrectionInitialization.ActualPrimary.FullPoint) : a.normal (HarmonicWaveInteraction.productStrip s) (PrimaryResidualClass.directions c) n x = HarmonicCalculus.phaseNormal PhysicalResidualBridge.ScaledGraph.radius G.radial PhysicalResidualBridge.ScaledGraph.angular G.axial Φ (PhysicalResidualTZ.swapCylinder x)

noncomputable def NavierStokes.ActualPrimaryBounds.normalScale {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) : ℝ

Normal scale, constructed using PhysicalParticularWave.normalWeight.

Equations

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

noncomputable def NavierStokes.ActualPrimaryBounds.chartNormal {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) : CorrectionInitialization.ActualPrimary.FullPoint → ProblemStatement.Space

Chart normal, given by (ActualPrimary.chartCoefficients l.1 l.2).normal fullStrip (PrimaryResidualClass.directions (ActualPrimary.commonContext B)) n.

Equations

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

theorem NavierStokes.ActualPrimaryBounds.fullCopy_slot {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : TorusInverse.Frequency) (x : CorrectionInitialization.ActualPrimary.FullPoint) : (fullCopy l n k x).2 = (ActualSignedGeometry.slotGeometry CorrectionInitialization.ActualPrimary.slots CorrectionInitialization.ActualPrimary.vectors_det (spatialLabel l) (ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (spatialLabel l).1 - CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).coordinates k (ActualSignedGeometry.meanEquiv.symm x.1).2

theorem NavierStokes.ActualPrimaryBounds.chart_normal_germ {B N0 : ℕ} {i : CopyIndex B N0} {n : ℕ} {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ fullStrip.domain) (hc : x ∈ controlCell n i) : chartNormal i.1 n =ᶠ[nhds x] fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => normalScale i.1 n • jointPhase.normal i.1 ((fullCopy i.1 n i.2 y).1, (fullCopy i.1 n i.2 y).2.2)

noncomputable def NavierStokes.ActualPrimaryBounds.normalLower : ℝ

Normal lower, given by (1 / 2 : ℝ) * (1 / ActualSignedGeometry.powerBound (ActualPrimary.h / 2 + 1 / 2)).

Equations

• NavierStokes.ActualPrimaryBounds.normalLower = 1 / 2 * (1 / NavierStokes.ActualSignedGeometry.powerBound (NavierStokes.CorrectionInitialization.ActualPrimary.h / 2 + 1 / 2))

noncomputable def NavierStokes.ActualPrimaryBounds.normalUpper : ℝ

Normal upper, given by 2 * ActualSignedGeometry.powerBound (ActualPrimary.h / 2 + 1 / 2).

Equations

• NavierStokes.ActualPrimaryBounds.normalUpper = 2 * NavierStokes.ActualSignedGeometry.powerBound (NavierStokes.CorrectionInitialization.ActualPrimary.h / 2 + 1 / 2)

theorem NavierStokes.ActualPrimaryBounds.normalLower_pos : 0 < normalLower

theorem NavierStokes.ActualPrimaryBounds.normalUpper_pos : 0 < normalUpper

theorem NavierStokes.ActualPrimaryBounds.normalScale_bounds {B N0 : ℕ} {l : SignedLabel B N0} {n : ℕ} (hn : near l n) : normalLower ≤ normalScale l n ∧ normalScale l n ≤ normalUpper

theorem NavierStokes.ActualPrimaryBounds.local_constant {s : WeightedClasses.StripData CorrectionInitialization.ActualPrimary.FullPoint} {I : Type u_1} {K : ℕ → I → Set CorrectionInitialization.ActualPrimary.FullPoint} {r : ℕ → I → ℝ} {C : ℝ} (hC : 0 ≤ C) (hr : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → |r n i| ≤ C) : LocalizedWaveBounds.LocalUnweighted s K 0 fun (n : ℕ) (i : I) (x : CorrectionInitialization.ActualPrimary.FullPoint) => r n i

A bound on an index-dependent constant is already a local all-jet bound, with the constant chosen before the index.

theorem NavierStokes.ActualPrimaryBounds.normalScale_local {B N0 : ℕ} : LocalizedWaveBounds.LocalUnweighted fullStrip controlCell 0 fun (n : ℕ) (i : CopyIndex B N0) (x : CorrectionInitialization.ActualPrimary.FullPoint) => normalScale i.1 n

theorem NavierStokes.ActualPrimaryBounds.chart_normal_local {B N0 : ℕ} : LocalizedWaveBounds.LocalUnweighted fullStrip controlCell 0 fun (n : ℕ) (i : CopyIndex B N0) => chartNormal i.1 n

noncomputable def NavierStokes.ActualPrimaryBounds.normalFloor (B N0 : ℕ) : ℝ

Normal floor, given by normalLower * min (ActualPrimary.phases B N0 0).b (ActualPrimary.phases B N0 1).b.

Equations

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

noncomputable def NavierStokes.ActualPrimaryBounds.normalCeiling (B N0 : ℕ) : ℝ

Normal ceiling, constructed using normalUpper.

Equations

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

theorem NavierStokes.ActualPrimaryBounds.normalFloor_pos (B N0 : ℕ) : 0 < normalFloor B N0

theorem NavierStokes.ActualPrimaryBounds.chart_normal_range {B N0 : ℕ} {i : CopyIndex B N0} {n : ℕ} {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ fullStrip.domain) (hc : x ∈ controlCell n i) : normalFloor B N0 ≤ ‖chartNormal i.1 n x‖ ∧ ‖chartNormal i.1 n x‖ ≤ normalCeiling B N0

theorem NavierStokes.ActualPrimaryBounds.chart_defect_local {B N0 : ℕ} : LocalizedWaveBounds.LocalUnweighted fullStrip controlCell 1 fun (n : ℕ) (i : CopyIndex B N0) => ActualPhaseDefect.defect i.1.1 i.1.2 n

noncomputable def NavierStokes.ActualPrimaryBounds.cutCoefficients {B N0 : ℕ} (l : SignedLabel B N0) : LinearWaveBounds.WaveCoefficients CorrectionInitialization.ActualPrimary.FullPoint

Cut coefficients, given by (ActualPrimary.chartCoefficients l.1 l.2).withCutoff (ActualPrimary.chartCutoff l.1 l.2).

Equations

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

noncomputable def NavierStokes.ActualPrimaryBounds.actualFamily {B N0 : ℕ} : LocalizedWaveBounds.WaveFamily CorrectionInitialization.ActualPrimary.FullPoint (CopyIndex B N0)

Actual family, given by LocalizedWaveBounds.WaveFamily.ofCoefficients (fun i => cutCoefficients i.1).

Equations

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

noncomputable def NavierStokes.ActualPrimaryBounds.directions (B : ℕ) : LinearWaveBounds.GraphDirections (LocalSignedRequest.Point × ℝ)

Directions, given by PrimaryResidualClass.directions (ActualPrimary.commonContext B).

Equations

• NavierStokes.ActualPrimaryBounds.directions B = NavierStokes.PrimaryResidualClass.directions (NavierStokes.CorrectionInitialization.ActualPrimary.commonContext B)

theorem NavierStokes.ActualPrimaryBounds.actualFamily_normal_eq {B N0 : ℕ} : actualFamily.normal fullStrip (directions B) = fun (n : ℕ) (i : CopyIndex B N0) => chartNormal i.1 n

theorem NavierStokes.ActualPrimaryBounds.actualFamily_defect_eq {B N0 : ℕ} : actualFamily.defect fullStrip (directions B) = fun (n : ℕ) (i : CopyIndex B N0) => ActualPhaseDefect.defect i.1.1 i.1.2 n

theorem NavierStokes.ActualPrimaryBounds.actualFamily_normal_range {B N0 : ℕ} {i : CopyIndex B N0} {n : ℕ} {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ fullStrip.domain) (hc : x ∈ controlCell n i) : normalFloor B N0 ≤ ‖actualFamily.normal fullStrip (directions B) n i x‖ ∧ ‖actualFamily.normal fullStrip (directions B) n i x‖ ≤ normalCeiling B N0

theorem NavierStokes.ActualPrimaryBounds.actualFamily_good_eq {B N0 : ℕ} : actualFamily.retainedGood fullStrip (directions B) = fun (n : ℕ) (i : CopyIndex B N0) => (CorrectionInitialization.ActualPrimary.piece region i.1.1 i.1.2).linearGood n

theorem NavierStokes.ActualPrimaryBounds.local_of_uniform {B N0 : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {w : SignedLabel B N0 → ℕ → CorrectionInitialization.ActualPrimary.FullPoint → ℝ} {α : ℝ} {f : SignedLabel B N0 → ℕ → CorrectionInitialization.ActualPrimary.FullPoint → E} (hf : LabelSumBounds.UniformClass fullStrip w α f) : LocalizedWaveBounds.LocalClass fullStrip controlCell (fun (n : ℕ) (i : CopyIndex B N0) => w i.1 n) α fun (n : ℕ) (i : CopyIndex B N0) => f i.1 n

theorem NavierStokes.ActualPrimaryBounds.carrier_band : WeightedClasses.BandBound fullStrip (-(1 / 2)) fun (n : ℕ) => ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)

theorem NavierStokes.ActualPrimaryBounds.inverse_carrier_band : WeightedClasses.BandBound fullStrip (1 / 2) fun (n : ℕ) => 1 / ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)

theorem NavierStokes.ActualPrimaryBounds.inverse_carrier_local {B N0 : ℕ} : LocalizedWaveBounds.LocalUnweighted fullStrip controlCell (1 / 2) fun (n : ℕ) (x : CopyIndex B N0) (x_1 : CorrectionInitialization.ActualPrimary.FullPoint) => 1 / ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)

theorem NavierStokes.ActualPrimaryBounds.radius_unweighted : WeightedClasses.UnweightedClass fullStrip 0 fun (x : ℕ) (x_1 : CorrectionInitialization.ActualPrimary.FullPoint) => x_1.1.1

theorem NavierStokes.ActualPrimaryBounds.slow_auxiliary (B : ℕ) : BaseContextAssembly.slowCoordinates (directions B).auxiliary.1 = 0

theorem NavierStokes.ActualPrimaryBounds.slow_field_auxiliary (B : ℕ) (f : PhaseCalculus.Slow → ℝ) (x : CorrectionInitialization.ActualPrimary.FullPoint) : (fderiv ℝ (fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => f (BaseContextAssembly.slowCoordinates y.1)) x) (directions B).auxiliary = 0

theorem NavierStokes.ActualPrimaryBounds.actual_local_inputs {B N0 : ℕ} : LocalizedWaveBounds.InputBounds fullStrip controlCell (fun (n : ℕ) (i : CopyIndex B N0) => fullEnvelope i.1 n) (1 / 2) ChartScales.kappa (directions B) actualFamily

theorem NavierStokes.ActualPrimaryBounds.actual_local_curl {B N0 : ℕ} : LocalizedWaveBounds.LocalWave fullStrip controlCell (fun (n : ℕ) (i : CopyIndex B N0) => fullEnvelope i.1 n) (1 - ChartScales.kappa) fun (n : ℕ) (i : CopyIndex B N0) => (cutCoefficients i.1).curlCorrection fullStrip (directions B) n

theorem NavierStokes.ActualPrimaryBounds.actual_local_good {B N0 : ℕ} : LocalizedWaveBounds.LocalWave fullStrip controlCell (fun (n : ℕ) (i : CopyIndex B N0) => fullEnvelope i.1 n) (1 - 3 * ChartScales.kappa) (actualFamily.retainedGood fullStrip (directions B))

theorem NavierStokes.ActualPrimaryBounds.cut_amplitude_eq {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ fullStrip.domain) : (cutCoefficients l).amplitude n x = periodized (CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) cutNativeVelocity l n (nativeOfFull x)

theorem NavierStokes.ActualPrimaryBounds.cut_pressure_eq {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ fullStrip.domain) : (cutCoefficients l).pressure n x = periodized (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) cutNativePressure l n (nativeOfFull x)

theorem NavierStokes.ActualPrimaryBounds.cut_amplitude_germ {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ fullStrip.domain) : (cutCoefficients l).amplitude n =ᶠ[nhds x] fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => periodized (CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) cutNativeVelocity l n (nativeOfFull y)

theorem NavierStokes.ActualPrimaryBounds.cut_pressure_germ {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ fullStrip.domain) : (cutCoefficients l).pressure n =ᶠ[nhds x] fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => periodized (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) cutNativePressure l n (nativeOfFull y)

theorem NavierStokes.ActualPrimaryBounds.copied_support {B N0 : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℝ) (f : SignedLabel B N0 → Native → E) (hs : ∀ (l : SignedLabel B N0) (x : Native), f l x ≠ 0 → x.2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.2).core) (l : SignedLabel B N0) (n : ℕ) (k : TorusInverse.Frequency) : Function.support (copied a f l n k) ⊆ (copyCells l).carrier n k

theorem NavierStokes.ActualPrimaryBounds.cut_native_velocity_support {B N0 : ℕ} (l : SignedLabel B N0) (x : Native) (hx : cutNativeVelocity l x ≠ 0) : x.2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.2).core

theorem NavierStokes.ActualPrimaryBounds.cut_native_pressure_support {B N0 : ℕ} (l : SignedLabel B N0) (x : Native) (hx : cutNativePressure l x ≠ 0) : x.2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.2).core

theorem NavierStokes.ActualPrimaryBounds.cut_native_zero_germs {B N0 : ℕ} (l : SignedLabel B N0) {x : Native} (hT : 0 < x.1.2.2) (hout : x.1 ∉ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier l.2 ∨ SimilarityHomogeneity.chartQ CorrectionInitialization.ActualPrimary.h x.1 ∉ Set.Icc (1 / 2) 2) : (cutNativeVelocity l =ᶠ[nhds x] fun (x : Native) => 0) ∧ cutNativePressure l =ᶠ[nhds x] fun (x : Native) => 0

theorem NavierStokes.ActualPrimaryBounds.actual_input_cover {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ fullStrip.domain) : (∃ (k : TorusInverse.Frequency), x ∈ controlCell n (l, k)) ∨ ((cutCoefficients l).amplitude n =ᶠ[nhds x] fun (x : CorrectionInitialization.ActualPrimary.FullPoint) => 0) ∧ (cutCoefficients l).pressure n =ᶠ[nhds x] fun (x : CorrectionInitialization.ActualPrimary.FullPoint) => 0

Every point has either an actual controlled native copy, or a neighborhood on which both literal input coefficients vanish.

theorem NavierStokes.ActualPrimaryBounds.chart_curl_uniform {B N0 : ℕ} : LabelSumBounds.UniformWaveClass fullStrip fullEnvelope (1 - ChartScales.kappa) fun (l : SignedLabel B N0) => (cutCoefficients l).curlCorrection fullStrip (directions B)

theorem NavierStokes.ActualPrimaryBounds.chart_exact_amplitude_uniform {B N0 : ℕ} : LabelSumBounds.UniformWaveClass fullStrip fullEnvelope (1 / 2) fun (l : SignedLabel B N0) => (CorrectionInitialization.ActualPrimary.piece region l.1 l.2).exactCoefficients.amplitude

theorem NavierStokes.ActualPrimaryBounds.chart_difference_uniform {B N0 : ℕ} : LabelSumBounds.UniformWaveClass fullStrip fullEnvelope (1 - ChartScales.kappa) fun (l : SignedLabel B N0) (n : ℕ) (x : CorrectionInitialization.ActualPrimary.FullPoint) => (CorrectionInitialization.ActualPrimary.piece region l.1 l.2).exactCoefficients.amplitude n x - (cutCoefficients l).amplitude n x

theorem NavierStokes.ActualPrimaryBounds.chart_exact_pressure_uniform {B N0 : ℕ} : LabelSumBounds.UniformWaveClass fullStrip fullEnvelope 1 fun (l : SignedLabel B N0) => (CorrectionInitialization.ActualPrimary.piece region l.1 l.2).exactCoefficients.pressure

theorem NavierStokes.ActualPrimaryBounds.chart_good_uniform {B N0 : ℕ} : LabelSumBounds.UniformWaveClass fullStrip fullEnvelope (1 - 3 * ChartScales.kappa) fun (l : SignedLabel B N0) => (CorrectionInitialization.ActualPrimary.piece region l.1 l.2).linearGood

theorem NavierStokes.ActualPrimaryBounds.exact_block_uniform {B N0 : ℕ} : (∀ (i : Fin 3) (m : ℤ), LabelSumBounds.UniformWaveClass strip meanEnvelope (1 / 2) fun (l : SignedLabel B N0) (n : ℕ) (x : Point) => (((CorrectionInitialization.ActualPrimary.piece region l.1 l.2).harmonicBlock (phase l) (angularFrequency l)).velocity n i).coeff m x) ∧ ∀ (m : ℤ), LabelSumBounds.UniformWaveClass strip meanEnvelope 1 fun (l : SignedLabel B N0) (n : ℕ) (x : Point) => (((CorrectionInitialization.ActualPrimary.piece region l.1 l.2).harmonicBlock (phase l) (angularFrequency l)).pressure n).coeff m x

theorem NavierStokes.ActualPrimaryBounds.difference_block_uniform {B N0 : ℕ} (i : Fin 3) (m : ℤ) : LabelSumBounds.UniformWaveClass strip meanEnvelope (1 - ChartScales.kappa) fun (l : SignedLabel B N0) (n : ℕ) (x : Point) => (((CorrectionInitialization.ActualPrimary.piece region l.1 l.2).differenceBlock (phase l) (angularFrequency l)).velocity n i).coeff m x