Ordinary jets of the selected primary phase

The angle and axial coordinate are affine in the actual phase. Their values need not be bounded, but their positive derivatives have a uniform bound. The remaining expression has polynomial slow jets on the same native phase cells used to construct the primary waves.

theorem NavierStokes.ActualPhaseJetBounds.norm_positive_jet_affine {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : E →L[ℝ] F) (c : F) (x : E) {j : ℕ} (hj : 1 ≤ j) : ‖iteratedFDeriv ℝ j (fun (y : E) => L y + c) x‖ ≤ ‖L‖

Affine values may be unbounded; every positive jet is bounded by the linear part alone.

@[reducible, inline]

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

Signed label: an abbreviation for ActualPrimaryBounds.SignedLabel B N0.

Equations

• NavierStokes.ActualPhaseJetBounds.SignedLabel B N0 = NavierStokes.ActualPrimaryBounds.SignedLabel B N0

noncomputable def NavierStokes.ActualPhaseJetBounds.slowDomain {B N0 : ℕ} : PhaseJetBounds.Domain (SignedLabel B N0) PhaseCalculus.Slow

Both signs share the actual, unmodified analytic phase cells.

Equations

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

noncomputable def NavierStokes.ActualPhaseJetBounds.jetDomain {B N0 : ℕ} : PhaseJetBounds.Domain (SignedLabel B N0) (PhaseCalculus.Slow × ℝ)

Jet domain, given by slowDomain.slot (fun l => (ActualPrimary.phases B N0 l.1).V l.2) (fun l => (ActualPrimary.phases B N0 l.1).openV l.2).

Equations

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

noncomputable def NavierStokes.ActualPhaseJetBounds.phaseSize (B N0 : ℕ) : ℝ

Phase size, given by (ActualPrimary.phases B N0 0).M + (ActualPrimary.phases B N0 1).M.

Equations

• NavierStokes.ActualPhaseJetBounds.phaseSize B N0 = (NavierStokes.CorrectionInitialization.ActualPrimary.phases B N0 0).M + (NavierStokes.CorrectionInitialization.ActualPrimary.phases B N0 1).M

theorem NavierStokes.ActualPhaseJetBounds.one_le_phaseSize {B N0 : ℕ} : 1 ≤ phaseSize B N0

theorem NavierStokes.ActualPhaseJetBounds.signSize_le {B N0 : ℕ} (j : Fin 2) : (CorrectionInitialization.ActualPrimary.phases B N0 j).M ≤ phaseSize B N0

theorem NavierStokes.ActualPhaseJetBounds.phase_constants_bound {B N0 : ℕ} (l : SignedLabel B N0) : |(CorrectionInitialization.ActualPrimary.phases B N0 l.1).phase.p l.2| ≤ phaseSize B N0 ∧ |(CorrectionInitialization.ActualPrimary.phases B N0 l.1).phase.pz l.2| ≤ phaseSize B N0 ∧ |(CorrectionInitialization.ActualPrimary.phases B N0 l.1).phase.x0 l.2| ≤ phaseSize B N0

noncomputable def NavierStokes.ActualPhaseJetBounds.nativeRemainder {B N0 : ℕ} (l : SignedLabel B N0) (z : PhaseCalculus.Slow × ℝ) : ℝ

The nonaffine part of the literal native phase.

Equations

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

theorem NavierStokes.ActualPhaseJetBounds.nativeRemainder_polynomial {B N0 : ℕ} : PhaseJetBounds.PolynomialJets jetDomain nativeRemainder

All orders follow from the actual constructed F/G jets and bounded native constants; this contains no phase-jet hypothesis.

Ordinary pullback jets on the actual native copy

@[reducible, inline]

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

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

Equations

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

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

Only the genuine analytic cell and clock core are required. In particular, this also allows the larger geometric source window.

Equations

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

theorem NavierStokes.ActualPhaseJetBounds.controlCell_subset_phaseCell {B N0 : ℕ} (n : ℕ) (i : CopyIndex B N0) : ActualPrimaryBounds.controlCell n i ⊆ phaseCell n i

theorem NavierStokes.ActualPhaseJetBounds.phaseCell_maps {B N0 n : ℕ} {i : CopyIndex B N0} {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ phaseCell n i) : ((ActualPrimaryBounds.fullCopy i.1 n i.2 x).1, (ActualPrimaryBounds.fullCopy i.1 n i.2 x).2.2) ∈ jetDomain.carrier i.1

theorem NavierStokes.ActualPhaseJetBounds.slow_eq_S {n : ℕ} (hn : 1 ≤ n) : ActualPrimaryBounds.fullStrip.slow n = ChartScales.S n

theorem NavierStokes.ActualPhaseJetBounds.polynomial_copy_smooth {B N0 : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : SignedLabel B N0 → PhaseCalculus.Slow × ℝ → E} (hf : PhaseJetBounds.PolynomialJets jetDomain f) {n : ℕ} {i : CopyIndex B N0} {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ phaseCell n i) : ContDiffAt ℝ (↑⊤) (fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => f i.1 ((ActualPrimaryBounds.fullCopy i.1 n i.2 y).1, (ActualPrimaryBounds.fullCopy i.1 n i.2 y).2.2)) x

theorem NavierStokes.ActualPhaseJetBounds.polynomial_copy_bound {B N0 : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : SignedLabel B N0 → PhaseCalculus.Slow × ℝ → E} (hf : PhaseJetBounds.PolynomialJets jetDomain f) (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∃ (p : ℕ), ∀ (n : ℕ) (i : CopyIndex B N0), ∀ x ∈ phaseCell n i, ∀ j ≤ m, ‖iteratedFDeriv ℝ j (fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => f i.1 ((ActualPrimaryBounds.fullCopy i.1 n i.2 y).1, (ActualPrimaryBounds.fullCopy i.1 n i.2 y).2.2)) x‖ ≤ C * ChartScales.S n ^ p

The estimate uses only the slow scale S, with no inverse distance to the boundary hidden in the bound.

noncomputable def NavierStokes.ActualPhaseJetBounds.nativeZ : PhaseCalculus.Slow × ℝ →L[ℝ] ℝ

The axial coordinate on the native slow/clock product.

Equations

• NavierStokes.ActualPhaseJetBounds.nativeZ = ContinuousLinearMap.fst ℝ ℝ ℝ ∘SL ContinuousLinearMap.snd ℝ ℝ (ℝ × ℝ) ∘SL ContinuousLinearMap.fst ℝ NavierStokes.PhaseCalculus.Slow ℝ

theorem NavierStokes.ActualPhaseJetBounds.nativeZ_norm : ‖nativeZ‖ ≤ 1

noncomputable def NavierStokes.ActualPhaseJetBounds.phaseLinear {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) : CorrectionInitialization.ActualPrimary.FullPoint →L[ℝ] ℝ

Phase linear as an element of ActualPrimary.FullPoint →L[ℝ] ℝ.

Equations

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

noncomputable def NavierStokes.ActualPhaseJetBounds.phaseOffset {B N0 : ℕ} (n : ℕ) (i : CopyIndex B N0) : ℝ

Phase offset as an element of ℝ.

Equations

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

noncomputable def NavierStokes.ActualPhaseJetBounds.localPhase {B N0 : ℕ} (n : ℕ) (i : CopyIndex B N0) (x : CorrectionInitialization.ActualPrimary.FullPoint) : ℝ

Local phase, constructed using PhaseCalculus.phase.

Equations

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

theorem NavierStokes.ActualPhaseJetBounds.localPhase_decomposition {B N0 : ℕ} (n : ℕ) (i : CopyIndex B N0) (x : CorrectionInitialization.ActualPrimary.FullPoint) : localPhase n i x = (phaseLinear i.1 n) x + phaseOffset n i + nativeRemainder i.1 ((ActualPrimaryBounds.fullCopy i.1 n i.2 x).1, (ActualPrimaryBounds.fullCopy i.1 n i.2 x).2.2)

theorem NavierStokes.ActualPhaseJetBounds.localPhase_smooth {B N0 n : ℕ} {i : CopyIndex B N0} {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ phaseCell n i) : ContDiffAt ℝ (↑⊤) (localPhase n i) x

theorem NavierStokes.ActualPhaseJetBounds.one_le_inverse_epsilon (n : ℕ) : 1 ≤ (ChartScales.epsilon CorrectionInitialization.ActualPrimary.h n)⁻¹

theorem NavierStokes.ActualPhaseJetBounds.carrier_le_inverse_epsilon (n : ℕ) : ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n) ≤ 2 * (ChartScales.epsilon CorrectionInitialization.ActualPrimary.h n)⁻¹

theorem NavierStokes.ActualPhaseJetBounds.phaseLinear_bound {B N0 : ℕ} {l : SignedLabel B N0} {n : ℕ} (hn : ActualPrimaryBounds.near l n) : ‖phaseLinear l n‖ ≤ 2 * phaseSize B N0 * ActualPrimaryBounds.copyCost * ChartScales.S n * (ChartScales.epsilon CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2))⁻¹

theorem NavierStokes.ActualPhaseJetBounds.localPhase_positive_jets {B N0 : ℕ} (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∃ (p : ℕ), ∀ (n : ℕ) (i : CopyIndex B N0), ∀ x ∈ phaseCell n i, ∀ (j : ℕ), 1 ≤ j → j ≤ m → ‖iteratedFDeriv ℝ j (localPhase n i) x‖ ≤ C * ChartScales.S n ^ p * (ChartScales.epsilon CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand i.1.2))⁻¹

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

The full frequency-weighted phase, with the literal chosen carrier.

Equations

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

theorem NavierStokes.ActualPhaseJetBounds.weightedPhase_germ {B N0 n : ℕ} {i : CopyIndex B N0} {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ phaseCell n i) : weightedPhase i.1 n =ᶠ[nhds x] fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand i.1.2)) * localPhase n i y

theorem NavierStokes.ActualPhaseJetBounds.weightedPhase_smooth {B N0 n : ℕ} {i : CopyIndex B N0} {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ phaseCell n i) : ContDiffAt ℝ (↑⊤) (weightedPhase i.1 n) x

theorem NavierStokes.ActualPhaseJetBounds.inverse_sq_eq_rpow (n : ℕ) : (ChartScales.epsilon CorrectionInitialization.ActualPrimary.h n)⁻¹ ^ 2 = ChartScales.epsilon CorrectionInitialization.ActualPrimary.h n ^ (-2)

theorem NavierStokes.ActualPhaseJetBounds.inverse_epsilon_sq (n : ℕ) : (ChartScales.epsilon CorrectionInitialization.ActualPrimary.h n)⁻¹ ^ 2 = ChartScales.Q n ^ (-(2 * CorrectionInitialization.ActualPrimary.h))

theorem NavierStokes.ActualPhaseJetBounds.inverse_epsilon_sq_window {B N0 : ℕ} {l : SignedLabel B N0} {n : ℕ} (hn : ActualPrimaryBounds.near l n) : (ChartScales.epsilon CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2))⁻¹ ^ 2 ≤ ActualSignedGeometry.powerBound (2 * CorrectionInitialization.ActualPrimary.h) * (ChartScales.epsilon CorrectionInitialization.ActualPrimary.h n)⁻¹ ^ 2

theorem NavierStokes.ActualPhaseJetBounds.weightedPhase_positive_jets {B N0 : ℕ} (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∃ (p : ℕ), ∀ (n : ℕ) (i : CopyIndex B N0), ∀ x ∈ phaseCell n i, ∀ (j : ℕ), 1 ≤ j → j ≤ m → ‖iteratedFDeriv ℝ j (weightedPhase i.1 n) x‖ ≤ C * ChartScales.S n ^ p * ChartScales.Q n ^ (-(2 * CorrectionInitialization.ActualPrimary.h))

One fixed loss Q^(-2h) controls every positive ordinary phase derivative. Only the constant and the slow power depend on its order.

theorem NavierStokes.ActualPhaseJetBounds.weightedPhase_contDiffOn {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) (weightedPhase l n) ActualPrimaryBounds.fullStrip.domain

theorem NavierStokes.ActualPhaseJetBounds.weightedPhase_eq_section {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (x : CorrectionInitialization.ActualPrimary.FullPoint) : weightedPhase l n x = (CorrectionInitialization.ActualPrimary.chartCoefficients l.1 l.2).frequency n * ActualPrimaryBounds.phase l n x.1 + ↑(ActualPrimaryBounds.angularFrequency l n) * x.2

The full phase is exactly the zero-angle section plus the fixed integer angular frequency.

theorem NavierStokes.ActualPhaseJetBounds.phaseCell_of_cut_tsupport {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ ActualPrimaryBounds.fullStrip.domain) (hs : x ∈ tsupport ((ActualPrimaryBounds.cutCoefficients l).amplitude n)) : ∃ (k : TorusInverse.Frequency), x ∈ phaseCell n (l, k)

theorem NavierStokes.ActualPhaseJetBounds.weightedPhase_positive_jets_cut {B N0 : ℕ} (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∃ (p : ℕ), ∀ (l : SignedLabel B N0) (n : ℕ), ∀ x ∈ ActualPrimaryBounds.fullStrip.domain, x ∈ tsupport ((ActualPrimaryBounds.cutCoefficients l).amplitude n) → ∀ (j : ℕ), 1 ≤ j → j ≤ m → ‖iteratedFDeriv ℝ j (weightedPhase l n) x‖ ≤ C * ChartScales.S n ^ p * ChartScales.Q n ^ (-(2 * CorrectionInitialization.ActualPrimary.h))

theorem NavierStokes.ActualPhaseJetBounds.carrier_eq_character {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) : HarmonicCalculus.carrier ((CorrectionInitialization.ActualPrimary.chartCoefficients l.1 l.2).frequency n) ((CorrectionInitialization.ActualPrimary.chartCoefficients l.1 l.2).phase n) = PhysicalGraphBounds.character 1 ∘ weightedPhase l n

theorem NavierStokes.ActualPhaseJetBounds.inverse_power_eq_rpow (n m : ℕ) : (ChartScales.epsilon CorrectionInitialization.ActualPrimary.h n)⁻¹ ^ (2 * m) = ChartScales.epsilon CorrectionInitialization.ActualPrimary.h n ^ (-(2 * ↑m))

theorem NavierStokes.ActualPhaseJetBounds.carrier_jets_phaseCell {B N0 : ℕ} (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∃ (p : ℕ), ∀ (n : ℕ) (i : CopyIndex B N0), ∀ x ∈ ActualPrimaryBounds.fullStrip.domain, x ∈ phaseCell n i → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (HarmonicCalculus.carrier ((CorrectionInitialization.ActualPrimary.chartCoefficients i.1.1 i.1.2).frequency n) ((CorrectionInitialization.ActualPrimary.chartCoefficients i.1.1 i.1.2).phase n)) x‖ ≤ WeightedClasses.majorant ActualPrimaryBounds.fullStrip (fun (x : ℕ) (x_1 : CorrectionInitialization.ActualPrimary.FullPoint) => 1) (-(2 * ↑m)) C p n x

Restoring the unit-modulus exponential uses only positive inner phase jets. Its finite-prefix loss is explicit, including order zero.

theorem NavierStokes.ActualPhaseJetBounds.carrier_jets_cut {B N0 : ℕ} (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ) (r : ℝ), ∀ (l : SignedLabel B N0) (n : ℕ), ∀ x ∈ ActualPrimaryBounds.fullStrip.domain, x ∈ tsupport ((ActualPrimaryBounds.cutCoefficients l).amplitude n) → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (HarmonicCalculus.carrier ((CorrectionInitialization.ActualPrimary.chartCoefficients l.1 l.2).frequency n) ((CorrectionInitialization.ActualPrimary.chartCoefficients l.1 l.2).phase n)) x‖ ≤ WeightedClasses.majorant ActualPrimaryBounds.fullStrip (fun (x : ℕ) (x_1 : CorrectionInitialization.ActualPrimary.FullPoint) => 1) r C p n x

The actual cut amplitude's support supplies the needed native copy; no independent carrier-jet estimate is assumed.

theorem NavierStokes.ActualPhaseJetBounds.phase_jet_le_weighted {B N0 n : ℕ} {i : CopyIndex B N0} {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ phaseCell n i) (j : ℕ) : ‖iteratedFDeriv ℝ j ((CorrectionInitialization.ActualPrimary.chartCoefficients i.1.1 i.1.2).phase n) x‖ ≤ ‖iteratedFDeriv ℝ j (weightedPhase i.1 n) x‖

theorem NavierStokes.ActualPhaseJetBounds.phase_positive_jets {B N0 : ℕ} (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∃ (p : ℕ), ∀ (n : ℕ) (i : CopyIndex B N0), ∀ x ∈ phaseCell n i, ∀ (j : ℕ), 1 ≤ j → j ≤ m → ‖iteratedFDeriv ℝ j ((CorrectionInitialization.ActualPrimary.chartCoefficients i.1.1 i.1.2).phase n) x‖ ≤ C * ChartScales.S n ^ p * ChartScales.Q n ^ (-(2 * CorrectionInitialization.ActualPrimary.h))

The literal normalized phase satisfies the same fixed-loss bound.

theorem NavierStokes.ActualPhaseJetBounds.harmonicPhase_positive_jets {B N0 : ℕ} (H : ℝ) (hH : 1 ≤ H) (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∃ (p : ℕ), ∀ (a : ℝ), |a| ≤ H → ∀ (n : ℕ) (i : CopyIndex B N0), ∀ x ∈ phaseCell n i, ∀ (j : ℕ), 1 ≤ j → j ≤ m → ‖iteratedFDeriv ℝ j (fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => a * weightedPhase i.1 n y) x‖ ≤ C * ChartScales.S n ^ p * ChartScales.Q n ^ (-(2 * CorrectionInitialization.ActualPrimary.h))

A bounded set of harmonic multiples changes only the constant. The power of Q is independent of both harmonic and derivative order.