Uniform weighted coefficients and physical wave sums

The constants below are selected before the label and the band. The first step absorbs the actual two flat edges, including every inverse-edge power. Global smoothness and support then extend the estimate across the boundary. The final passage uses genuine common-coordinate compositions and the physical carrier estimates of PhysicalWaveSum.

structure NavierStokes.PhysicalClassBounds.FlatGeometry {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (cL cR L : ℝ) (ρ : D → ℝ) : Prop

Explicit fixed flat-edge geometry, pulled back through any radial coordinate. This is an equality of the weights, not a bound on them.

• left_pos : 0 < cL
• right_pos : 0 < cR
• position (x : D) : x ∈ s.domain → ρ x ∈ Set.Ioo 0 L
• delta_eq (x : D) : x ∈ s.domain → s.delta x = WeightedRadialPrimitive.delta L (ρ x)
• zeta_eq (x : D) : x ∈ s.domain → s.zeta x = WeightedRadialPrimitive.zeta cL cR L (ρ x)

theorem NavierStokes.PhysicalClassBounds.edge_rpow {x : ℝ} (hx : 0 < x) (a c : ℝ) : FlatCutoff.edge a x ^ c = FlatCutoff.edge (c * a) x

theorem NavierStokes.PhysicalClassBounds.zeta_rpow {L x : ℝ} (hx : x ∈ Set.Ioo 0 L) (cL cR c : ℝ) : WeightedRadialPrimitive.zeta cL cR L x ^ c = WeightedRadialPrimitive.zeta (c * cL) (c * cR) L x

theorem NavierStokes.PhysicalClassBounds.flat_edge_uniform {cL cR c : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (hc : 0 < c) (L : ℝ) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ x ∈ Set.Ioo 0 L, max 1 (WeightedRadialPrimitive.delta L x)⁻¹ ^ m * WeightedRadialPrimitive.zeta cL cR L x ^ c ≤ K

Exponential flatness absorbs any fixed inverse-edge power, uniformly at both endpoints and for every positive fractional power of the weight.

theorem NavierStokes.PhysicalClassBounds.FlatGeometry.uniform {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {cL cR L : ℝ} {ρ : D → ℝ} (hg : FlatGeometry s cL cR L ρ) {c : ℝ} (hc : 0 < c) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ x ∈ s.domain, max 1 (s.delta x)⁻¹ ^ m * s.zeta x ^ c ≤ K

theorem NavierStokes.PhysicalClassBounds.logStrip_flatGeometry {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a b cL cR : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) : FlatGeometry (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) cL cR (WeightedRadialPrimitive.logLength a b) fun (x : ℝ × V) => WeightedRadialPrimitive.logPosition a x.1

theorem NavierStokes.PhysicalClassBounds.movingStrip_flatGeometry {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) {a b cL cR : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) : FlatGeometry (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε S hε hεone hS) cL cR (WeightedRadialPrimitive.logLength a b) fun (x : LocalSignedRequest.Point) => WeightedRadialPrimitive.logPosition a (LocalSignedRequest.profileMap coord x).1

theorem NavierStokes.PhysicalClassBounds.UniformClass.edge_absorbed {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_2} {s : WeightedClasses.StripData D} {cL cR L : ℝ} {ρ : D → ℝ} (hg : FlatGeometry s cL cR L ρ) {c α : ℝ} (hc : 0 < c) {w : ι → ℕ → D → ℝ} {f : ι → ℕ → D → E} (hf : LabelSumBounds.UniformClass s w α f) (hw : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, w l n x ≤ s.zeta x ^ c) (m : ℕ) : ∃ (A : ℝ), 0 ≤ A ∧ ∃ (p : ℕ), ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, ∀ j ≤ m, ‖iteratedFDeriv ℝ j (f l n) x‖ ≤ A * s.epsilon n ^ α * s.slow n ^ p

Remove the edge growth from an actual uniform coefficient class. The input envelope may depend on the label and band; its domination is uniform.

theorem NavierStokes.PhysicalClassBounds.jets_bound_global_of_support {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : D → E} {U : Set D} {B : ℝ} (hf : ContDiff ℝ (↑⊤) f) (hB : 0 ≤ B) (hs : tsupport f ⊆ closure U) (m : ℕ) (hb : ∀ x ∈ U, ‖iteratedFDeriv ℝ m f x‖ ≤ B) (x : D) : ‖iteratedFDeriv ℝ m f x‖ ≤ B

The support boundary is included by continuity of the actual jets. Outside it all jets vanish, because there is an actual zero neighborhood.

theorem NavierStokes.PhysicalClassBounds.tsupport_subset_closure_of_zero {D : Type} [NormedAddCommGroup D] {E : Type u_1} [NormedAddCommGroup E] {f : D → E} {U : Set D} (hf : ∀ x ∉ closure U, f x = 0) : tsupport f ⊆ closure U

theorem NavierStokes.PhysicalClassBounds.UniformClass.edge_absorbed_global {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_2} {s : WeightedClasses.StripData D} {cL cR L : ℝ} {ρ : D → ℝ} (hg : FlatGeometry s cL cR L ρ) {c α : ℝ} (hc : 0 < c) {w : ι → ℕ → D → ℝ} {f : ι → ℕ → D → E} (hf : LabelSumBounds.UniformClass s w α f) (hw : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, w l n x ≤ s.zeta x ^ c) (hfc : ∀ (l : ι) (n : ℕ), ContDiff ℝ (↑⊤) (f l n)) (hs : ∀ (l : ι) (n : ℕ), tsupport (f l n) ⊆ closure s.domain) (m : ℕ) : ∃ (A : ℝ), 0 ≤ A ∧ ∃ (p : ℕ), ∀ (l : ι) (n : ℕ) (x : D), ∀ j ≤ m, ‖iteratedFDeriv ℝ j (f l n) x‖ ≤ A * s.epsilon n ^ α * s.slow n ^ p

theorem NavierStokes.PhysicalClassBounds.UniformClass.chart_bound {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_2} {s : WeightedClasses.StripData D} {cL cR L : ℝ} {ρ : D → ℝ} (hg : FlatGeometry s cL cR L ρ) {c α h K : ℝ} {q : ℕ} (hc : 0 < c) (hK : 1 ≤ K) (hε : ∀ (n : ℕ), s.epsilon n = ChartScales.epsilon h n) (hslow : ∀ (n : ℕ), 4 ≤ n → s.slow n ≤ K * ChartScales.S n ^ q) {w : ι → ℕ → D → ℝ} {f : ι → ℕ → D → E} (hf : LabelSumBounds.UniformClass s w α f) (hw : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, w l n x ≤ s.zeta x ^ c) (hfc : ∀ (l : ι) (n : ℕ), ContDiff ℝ (↑⊤) (f l n)) (hs : ∀ (l : ι) (n : ℕ), tsupport (f l n) ⊆ closure s.domain) (m : ℕ) : ∃ (A : ℝ), 0 ≤ A ∧ ∃ (p : ℕ), ∀ (l : ι) (n : ℕ), 4 ≤ n → ∀ (x : D), ∀ j ≤ m, ‖iteratedFDeriv ℝ j (f l n) x‖ ≤ A * ChartScales.Q n ^ (h * α) * ChartScales.S n ^ p

Conversion to physical band powers is exact; no exponent is lost when the two flat edges are removed.

theorem NavierStokes.PhysicalClassBounds.waveWeight_le {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_2} {s : WeightedClasses.StripData D} {P : ι → ℕ → D → ℝ} (hP : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, P l n x ≤ 1) (l : ι) (n : ℕ) (x : D) : x ∈ s.domain → √(s.zeta x) * P l n x ≤ s.zeta x ^ (1 / 2)

theorem NavierStokes.PhysicalClassBounds.UniformWaveClass.chart_bound {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_2} {s : WeightedClasses.StripData D} {cL cR L : ℝ} {ρ : D → ℝ} (hg : FlatGeometry s cL cR L ρ) {α h K : ℝ} {q : ℕ} (hK : 1 ≤ K) (hε : ∀ (n : ℕ), s.epsilon n = ChartScales.epsilon h n) (hslow : ∀ (n : ℕ), 4 ≤ n → s.slow n ≤ K * ChartScales.S n ^ q) {P : ι → ℕ → D → ℝ} {f : ι → ℕ → D → E} (hf : LabelSumBounds.UniformWaveClass s P α f) (hP : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, P l n x ≤ 1) (hfc : ∀ (l : ι) (n : ℕ), ContDiff ℝ (↑⊤) (f l n)) (hs : ∀ (l : ι) (n : ℕ), tsupport (f l n) ⊆ closure s.domain) (m : ℕ) : ∃ (A : ℝ), 0 ≤ A ∧ ∃ (p : ℕ), ∀ (l : ι) (n : ℕ), 4 ≤ n → ∀ (x : D), ∀ j ≤ m, ‖iteratedFDeriv ℝ j (f l n) x‖ ≤ A * ChartScales.Q n ^ (h * α) * ChartScales.S n ^ p

theorem NavierStokes.PhysicalClassBounds.UniformMeanClass.chart_bound {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_2} {s : WeightedClasses.StripData D} {cL cR L : ℝ} {ρ : D → ℝ} (hg : FlatGeometry s cL cR L ρ) {α h K : ℝ} {q : ℕ} (hK : 1 ≤ K) (hε : ∀ (n : ℕ), s.epsilon n = ChartScales.epsilon h n) (hslow : ∀ (n : ℕ), 4 ≤ n → s.slow n ≤ K * ChartScales.S n ^ q) {f : ι → ℕ → D → E} (hf : LabelSumBounds.UniformMeanClass s α f) (hfc : ∀ (l : ι) (n : ℕ), ContDiff ℝ (↑⊤) (f l n)) (hs : ∀ (l : ι) (n : ℕ), tsupport (f l n) ⊆ closure s.domain) (m : ℕ) : ∃ (A : ℝ), 0 ≤ A ∧ ∃ (p : ℕ), ∀ (l : ι) (n : ℕ), 4 ≤ n → ∀ (x : D), ∀ j ≤ m, ‖iteratedFDeriv ℝ j (f l n) x‖ ≤ A * ChartScales.Q n ^ (h * α) * ChartScales.S n ^ p

structure NavierStokes.PhysicalClassBounds.SourceBounds {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_2} (s : WeightedClasses.StripData D) (h α : ℝ) (w : ι → ℕ → D → ℝ) (f : ι → ℕ → D → E) : Prop

Primitive input for the physical bridge. In particular, uniform places its constants before the label, and support concerns the actual coefficient, not a prescribed bound for its derivatives.

• uniform : LabelSumBounds.UniformClass s w α f
• flat_geometry : ∃ (cL : ℝ) (cR : ℝ) (L : ℝ) (ρ : D → ℝ), FlatGeometry s cL cR L ρ
• weight_le : ∃ (c : ℝ), 0 < c ∧ ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, w l n x ≤ s.zeta x ^ c
• epsilon_eq (n : ℕ) : s.epsilon n = ChartScales.epsilon h n
• slow_le : ∃ (K : ℝ), 1 ≤ K ∧ ∃ (q : ℕ), ∀ (n : ℕ), 4 ≤ n → s.slow n ≤ K * ChartScales.S n ^ q
• smooth (l : ι) (n : ℕ) : ContDiff ℝ (↑⊤) (f l n)
• support (l : ι) (n : ℕ) : tsupport (f l n) ⊆ closure s.domain

theorem NavierStokes.PhysicalClassBounds.SourceBounds.chart_bound {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_2} {s : WeightedClasses.StripData D} {h α : ℝ} {w : ι → ℕ → D → ℝ} {f : ι → ℕ → D → E} (hf : SourceBounds s h α w f) (m : ℕ) : ∃ (A : ℝ), 0 ≤ A ∧ ∃ (p : ℕ), ∀ (l : ι) (n : ℕ), 4 ≤ n → ∀ (x : D), ∀ j ≤ m, ‖iteratedFDeriv ℝ j (f l n) x‖ ≤ A * ChartScales.Q n ^ (h * α) * ChartScales.S n ^ p

theorem NavierStokes.PhysicalClassBounds.SourceBounds.of_wave {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_2} {s : WeightedClasses.StripData D} {cL cR L : ℝ} {ρ : D → ℝ} (hg : FlatGeometry s cL cR L ρ) {h α K : ℝ} {q : ℕ} (hK : 1 ≤ K) (hε : ∀ (n : ℕ), s.epsilon n = ChartScales.epsilon h n) (hslow : ∀ (n : ℕ), 4 ≤ n → s.slow n ≤ K * ChartScales.S n ^ q) {P : ι → ℕ → D → ℝ} {f : ι → ℕ → D → E} (hf : LabelSumBounds.UniformWaveClass s P α f) (hP : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, P l n x ≤ 1) (hfc : ∀ (l : ι) (n : ℕ), ContDiff ℝ (↑⊤) (f l n)) (hs : ∀ (l : ι) (n : ℕ), tsupport (f l n) ⊆ closure s.domain) : SourceBounds s h α (fun (l : ι) (n : ℕ) (x : D) => √(s.zeta x) * P l n x) f

theorem NavierStokes.PhysicalClassBounds.SourceBounds.of_mean {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_2} {s : WeightedClasses.StripData D} {cL cR L : ℝ} {ρ : D → ℝ} (hg : FlatGeometry s cL cR L ρ) {h α K : ℝ} {q : ℕ} (hK : 1 ≤ K) (hε : ∀ (n : ℕ), s.epsilon n = ChartScales.epsilon h n) (hslow : ∀ (n : ℕ), 4 ≤ n → s.slow n ≤ K * ChartScales.S n ^ q) {f : ι → ℕ → D → E} (hf : LabelSumBounds.UniformMeanClass s α f) (hfc : ∀ (l : ι) (n : ℕ), ContDiff ℝ (↑⊤) (f l n)) (hs : ∀ (l : ι) (n : ℕ), tsupport (f l n) ⊆ closure s.domain) : SourceBounds s h α (fun (x : ι) (x_1 : ℕ) (x_2 : D) => s.zeta x_2) f

theorem NavierStokes.PhysicalClassBounds.SourceBounds.map {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] {s : WeightedClasses.StripData D} {h α : ℝ} {w : ι → ℕ → D → ℝ} {f : ι → ℕ → D → E} (hf : SourceBounds s h α w f) (T : E →L[ℝ] V) : SourceBounds s h α w fun (l : ι) (n : ℕ) (x : D) => T (f l n x)

theorem NavierStokes.PhysicalClassBounds.composition_jet_bound {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] {g : D → E} {φ : X → D} {U : Set X} (hg : ContDiff ℝ (↑⊤) g) (hU : IsOpen U) (hφ : ContDiffOn ℝ (↑⊤) φ U) {x : X} (hx : x ∈ U) (m : ℕ) {A B : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hgb : ∀ i ≤ m, ‖iteratedFDeriv ℝ i g (φ x)‖ ≤ A) (hφb : ∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDeriv ℝ i φ x‖ ≤ B) (j : ℕ) : j ≤ m → ‖iteratedFDeriv ℝ j (g ∘ φ) x‖ ≤ ↑m.factorial * A * B ^ m

A local form of the genuine higher chain-rule estimate. Only positive derivatives of the coordinate map are needed; the map's values may be unbounded.

structure NavierStokes.PhysicalClassBounds.CommonChart {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_2} {H : ℕ} (F : PhysicalWaveSum.WaveFamily H) (a b h r0 σ : ℝ) (f : ι → ℕ → D → ℂ) : Type u_2

The common-chart identity for actual amplitudes. This records only the source formula and the coordinate map's jets, before any physical graph or carrier has been differentiated.

• sourceIndex : PhysicalWaveSum.WaveIndex H → ι

  Source index of CommonChart, of type PhysicalWaveSum.WaveIndex H → ι.

• map : PhysicalWaveSum.WaveIndex H → PhysicalWaveSum.LiftPoint → D

  Map from a lifted point in each wave chart to the common physical domain.

• domain : PhysicalWaveSum.WaveIndex H → Set PhysicalWaveSum.LiftPoint

  Domain of CommonChart, of type PhysicalWaveSum.WaveIndex H → Set PhysicalWaveSum.LiftPoint.

• open_domain (I : PhysicalWaveSum.WaveIndex H) : IsOpen (self.domain I)
• smooth (I : PhysicalWaveSum.WaveIndex H) : ContDiffOn ℝ (↑⊤) (self.map I) (self.domain I)
• positive_jets (m : ℕ) : ∃ (B : ℝ), 1 ≤ B ∧ ∃ (q : ℕ), ∀ (I : PhysicalWaveSum.WaveIndex H), ∀ x ∈ self.domain I, ∀ (j : ℕ), 1 ≤ j → j ≤ m → ‖iteratedFDeriv ℝ j (self.map I) x‖ ≤ B * ChartScales.S (↑I.1).1 ^ q
• amplitude_eq (I : PhysicalWaveSum.WaveIndex H) : F.amplitude I = fun (x : PhysicalWaveSum.LiftPoint) => ChartScales.Q (↑I.1).1 ^ σ • f (self.sourceIndex I) (↑I.1).1 (self.map I x)
• contains (I : PhysicalWaveSum.WaveIndex H) (z : ProblemStatement.SpaceTime) : z ∈ PhysicalWaveSum.preterminal → PhysicalWaveSum.physicalParams h z ∈ PhysicalWaveSum.labelRegion (CoordinateAlgebra.D h) ↑I.1 → (PhysicalGraphBounds.scaledRadial (↑I.1).1) z ∈ PhysicalGraphBounds.annulus a b → PhysicalWaveSum.commonLift h (↑I.1).1 (F.gap I.1) z ∈ self.domain I

theorem NavierStokes.PhysicalClassBounds.CommonChart.amplitude_bound {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_2} {s : WeightedClasses.StripData D} {h α σ a b r0 : ℝ} {w : ι → ℕ → D → ℝ} {f : ι → ℕ → D → ℂ} (hf : SourceBounds s h α w f) {H : ℕ} {F : PhysicalWaveSum.WaveFamily H} (hc : CommonChart F a b h r0 σ f) (m : ℕ) : ∃ (A : ℝ), 0 ≤ A ∧ ∃ (p : ℕ), ∀ (I : PhysicalWaveSum.WaveIndex H), ∀ x ∈ hc.domain I, ∀ j ≤ m, ‖iteratedFDeriv ℝ j (F.amplitude I) x‖ ≤ A * ChartScales.Q (↑I.1).1 ^ (h * α + σ) * ChartScales.S (↑I.1).1 ^ p

Actual composition and the explicit band prefactor produce the stripped amplitude estimate. Its exponent is h*α+σ, and its constants are independent of the label.

noncomputable def NavierStokes.PhysicalClassBounds.bandDomain {V : Type} [NormedAddCommGroup V] (U : PhysicalWaveSum.BandLabel → Set V) (hU : ∀ (L : PhysicalWaveSum.BandLabel), IsOpen (U L)) : PhaseJetBounds.Domain PhysicalWaveSum.BandLabel V

The natural slow scale for a band label is at least one because the physical sum starts at band four.

Equations

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

structure NavierStokes.PhysicalClassBounds.CarrierBounds {H : ℕ} (F : PhysicalWaveSum.WaveFamily H) (a b h r0 : ℝ) : Type

Polynomial jets of the actual two base profiles entering the phase, on open slow-coordinate regions containing every relevant chart point.

• region : PhysicalWaveSum.BandLabel → Set PhysicalGraphBounds.Slow

  Region of CarrierBounds, of type PhysicalWaveSum.BandLabel → Set PhysicalGraphBounds.Slow.

• open_region (L : PhysicalWaveSum.BandLabel) : IsOpen (self.region L)
• jets : PhaseJetBounds.PolynomialJets (bandDomain self.region ⋯) fun (L : PhysicalWaveSum.BandLabel) (x : PhysicalGraphBounds.Slow) => ((F.carrier L).F x, (F.carrier L).G x)
• contains (I : PhysicalWaveSum.WaveIndex H) (z : ProblemStatement.SpaceTime) : z ∈ PhysicalWaveSum.preterminal → PhysicalWaveSum.physicalParams h z ∈ PhysicalWaveSum.labelRegion (CoordinateAlgebra.D h) ↑I.1 → (PhysicalGraphBounds.scaledRadial (↑I.1).1) z ∈ PhysicalGraphBounds.annulus a b → ∀ (chart : PolarCharts.Index), (PhysicalGraphBounds.scaledRadial (↑I.1).1) z ∈ PolarCharts.chartDomain a chart → (PhysicalGraphBounds.slotMap (PolarCharts.chart a chart) (ChartScales.timeCoefficient h (↑I.1).1) (F.carrier I.1).center r0 (PhysicalGraphBounds.physicalLift h (↑I.1).1 z)).1 ∈ self.region I.1

theorem NavierStokes.PhysicalClassBounds.CarrierBounds.profile_bound {H : ℕ} {F : PhysicalWaveSum.WaveFamily H} {a b h r0 : ℝ} (hb : CarrierBounds F a b h r0) (m : ℕ) : ∃ (B : ℝ), 1 ≤ B ∧ ∃ (p : ℕ), ∀ (L : PhysicalWaveSum.BandLabel), ∀ x ∈ hb.region L, ∀ j ≤ m, ‖iteratedFDeriv ℝ j (F.carrier L).F x‖ ≤ B * ChartScales.S (↑L).1 ^ p ∧ ‖iteratedFDeriv ℝ j (F.carrier L).G x‖ ≤ B * ChartScales.S (↑L).1 ^ p

theorem NavierStokes.PhysicalClassBounds.strippedClass {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_2} {s : WeightedClasses.StripData D} {h α σ a b r0 P : ℝ} {w : ι → ℕ → D → ℝ} {f : ι → ℕ → D → ℂ} (hf : SourceBounds s h α w f) {H : ℕ} {F : PhysicalWaveSum.WaveFamily H} (hc : CommonChart F a b h r0 σ f) (hb : CarrierBounds F a b h r0) (hp : ∀ (L : PhysicalWaveSum.BandLabel), |(F.carrier L).angular| ≤ P ∧ |(F.carrier L).axial| ≤ P ∧ |(F.carrier L).radial| ≤ P) (m : ℕ) : ∃ (A : ℝ), 0 ≤ A ∧ ∃ (B : ℝ), 1 ≤ B ∧ ∃ (p : ℕ) (q : ℕ), PhysicalWaveSum.StrippedClass F a b h r0 P A B (h * α + σ) (↑p) (↑q) m

The full StrippedClass is derived from the uniform weighted source, the primitive common-chart identity, and the actual base-profile jets.

noncomputable def NavierStokes.PhysicalClassBounds.physicalLoss (h σ : ℝ) (m : ℕ) : ℝ

The derivative loss includes the displayed physical field rescaling. It depends on the derivative order and fixed scaling parameters only.

Equations

• NavierStokes.PhysicalClassBounds.physicalLoss h σ m = NavierStokes.PhysicalGraphBounds.waveLoss h m - σ

theorem NavierStokes.PhysicalClassBounds.physical_sum_jet_bound {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_2} {s : WeightedClasses.StripData D} {h α σ a b r0 Z P : ℝ} {w : ι → ℕ → D → ℝ} {f : ι → ℕ → D → ℂ} (hf : SourceBounds s h α w f) {H Δ : ℕ} {F : PhysicalWaveSum.WaveFamily H} (hc : CommonChart F a b h r0 σ f) (hb : CarrierBounds F a b h r0) (hr : PhysicalWaveSum.RegularFamily F a b h r0 Z Δ) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hZ : 0 ≤ Z) (hr0 : 0 ≤ r0) (hP : 1 ≤ P) (hp : ∀ (L : PhysicalWaveSum.BandLabel), |(F.carrier L).angular| ≤ P ∧ |(F.carrier L).axial| ≤ P ∧ |(F.carrier L).radial| ≤ P) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ z ∈ PhysicalWaveSum.preterminal, |z.1| ≤ 1 → ‖iteratedFDeriv ℝ m (F.sum a h r0) z‖ ≤ C * PhysicalWaveSum.physicalQ h z ^ (h * α - physicalLoss h σ m)

Full physical jets of the actual locally finite wave sum. The derivative-loss function does not depend on the harmonic cutoff, cover gap, label, slow polynomial degrees, or correction stage.

theorem NavierStokes.PhysicalClassBounds.physical_vector_sum_jet_bound {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_2} {s : WeightedClasses.StripData D} {h α σ a b r0 Z P : ℝ} {w : ι → ℕ → D → ℝ} {f : ι → ℕ → D → ℂ} (hf : SourceBounds s h α w f) {H Δ : ℕ} {F : Fin 3 → PhysicalWaveSum.WaveFamily H} (hc : (i : Fin 3) → CommonChart (F i) a b h r0 σ f) (hb : (i : Fin 3) → CarrierBounds (F i) a b h r0) (hr : ∀ (i : Fin 3), PhysicalWaveSum.RegularFamily (F i) a b h r0 Z Δ) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hZ : 0 ≤ Z) (hr0 : 0 ≤ r0) (hP : 1 ≤ P) (hp : ∀ (i : Fin 3) (L : PhysicalWaveSum.BandLabel), |((F i).carrier L).angular| ≤ P ∧ |((F i).carrier L).axial| ≤ P ∧ |((F i).carrier L).radial| ≤ P) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ z ∈ PhysicalWaveSum.preterminal, |z.1| ≤ 1 → ‖iteratedFDeriv ℝ m (PhysicalWaveSum.vectorSum F a h r0) z‖ ≤ C * PhysicalWaveSum.physicalQ h z ^ (h * α - physicalLoss h σ m)

theorem NavierStokes.PhysicalClassBounds.physical_real_sum_jet_bound {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_2} {s : WeightedClasses.StripData D} {h α σ a b r0 Z P : ℝ} {w : ι → ℕ → D → ℝ} {f : ι → ℕ → D → ℂ} (hf : SourceBounds s h α w f) {H Δ : ℕ} {F : PhysicalWaveSum.WaveFamily H} (hc : CommonChart F a b h r0 σ f) (hb : CarrierBounds F a b h r0) (hr : PhysicalWaveSum.RegularFamily F a b h r0 Z Δ) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hZ : 0 ≤ Z) (hr0 : 0 ≤ r0) (hP : 1 ≤ P) (hp : ∀ (L : PhysicalWaveSum.BandLabel), |(F.carrier L).angular| ≤ P ∧ |(F.carrier L).axial| ≤ P ∧ |(F.carrier L).radial| ≤ P) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ z ∈ PhysicalWaveSum.preterminal, |z.1| ≤ 1 → ‖iteratedFDeriv ℝ m (fun (z : ProblemStatement.SpaceTime) => (F.sum a h r0 z).re) z‖ ≤ C * PhysicalWaveSum.physicalQ h z ^ (h * α - physicalLoss h σ m)

Taking the real part, as for the physical pressure, loses no constant.

noncomputable def NavierStokes.PhysicalClassBounds.spatialInclusion : ProblemStatement.Space →L[ℝ] ProblemStatement.SpaceTime

Inclusion of a spatial direction into a joint spacetime direction.

Equations

• NavierStokes.PhysicalClassBounds.spatialInclusion = ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ NavierStokes.ProblemStatement.Space)

noncomputable def NavierStokes.PhysicalClassBounds.jointCurl : (ProblemStatement.SpaceTime →L[ℝ] ProblemStatement.Space) →L[ℝ] ProblemStatement.Space

A fixed continuous linear map takes the spatial curl from a joint Jacobian. Its norm is independent of every band and correction stage.

Equations

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

theorem NavierStokes.PhysicalClassBounds.spatialCurl_eq_joint {A : ProblemStatement.VelocityField} {z : ProblemStatement.SpaceTime} (hA : DifferentiableAt ℝ A z) : SpatialCurl.spatialCurl A z = jointCurl (fderiv ℝ A z)

theorem NavierStokes.PhysicalClassBounds.spatialCurl_jet_bound {A : ProblemStatement.VelocityField} {U : Set ProblemStatement.SpaceTime} (hU : IsOpen U) (hA : ContDiffOn ℝ (↑⊤) A U) {z : ProblemStatement.SpaceTime} (hz : z ∈ U) (m : ℕ) : ‖iteratedFDeriv ℝ m (SpatialCurl.spatialCurl A) z‖ ≤ ‖jointCurl‖ * ‖iteratedFDeriv ℝ (m + 1) A z‖

Taking the actual spatial curl costs exactly one joint derivative and a fixed linear-operator norm.

theorem NavierStokes.PhysicalClassBounds.physical_vector_curl_jet_bound {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_2} {s : WeightedClasses.StripData D} {h α σ a b r0 Z P : ℝ} {w : ι → ℕ → D → ℝ} {f : ι → ℕ → D → ℂ} (hf : SourceBounds s h α w f) {H Δ : ℕ} {F : Fin 3 → PhysicalWaveSum.WaveFamily H} (hc : (i : Fin 3) → CommonChart (F i) a b h r0 σ f) (hb : (i : Fin 3) → CarrierBounds (F i) a b h r0) (hr : ∀ (i : Fin 3), PhysicalWaveSum.RegularFamily (F i) a b h r0 Z Δ) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hZ : 0 ≤ Z) (hr0 : 0 ≤ r0) (hP : 1 ≤ P) (hp : ∀ (i : Fin 3) (L : PhysicalWaveSum.BandLabel), |((F i).carrier L).angular| ≤ P ∧ |((F i).carrier L).axial| ≤ P ∧ |((F i).carrier L).radial| ≤ P) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ z ∈ PhysicalWaveSum.preterminal, |z.1| ≤ 1 → ‖iteratedFDeriv ℝ m (SpatialCurl.spatialCurl (PhysicalWaveSum.vectorSum F a h r0)) z‖ ≤ C * PhysicalWaveSum.physicalQ h z ^ (h * α - physicalLoss h σ (m + 1))

@[simp]

theorem NavierStokes.PhysicalClassBounds.physicalLoss_potential (h : ℝ) (m : ℕ) : physicalLoss h (-h) m = PhysicalGraphBounds.waveLoss h m + h

@[simp]

theorem NavierStokes.PhysicalClassBounds.physicalLoss_velocity (h : ℝ) (m : ℕ) : physicalLoss h (-CoordinateAlgebra.A h) m = PhysicalGraphBounds.waveLoss h m + CoordinateAlgebra.A h

@[simp]

theorem NavierStokes.PhysicalClassBounds.physicalLoss_pressure (h : ℝ) (m : ℕ) : physicalLoss h (-(2 * CoordinateAlgebra.A h)) m = PhysicalGraphBounds.waveLoss h m + 2 * CoordinateAlgebra.A h

The actual Cartesian-to-cylindrical coefficient map

@[reducible, inline]

abbrev NavierStokes.PhysicalClassBounds.CylindricalPoint : Type

Cylindrical point: an abbreviation for ℝ × ((ℝ × ℝ) × PhysicalGraphBounds.Plane).

Equations

• NavierStokes.PhysicalClassBounds.CylindricalPoint = (ℝ × (ℝ × ℝ) × NavierStokes.PhysicalGraphBounds.Plane)

noncomputable def NavierStokes.PhysicalClassBounds.cartesianRadius (y : PhysicalGraphBounds.Plane) : ℝ

Cartesian radius, given by Real.sqrt (y.1 ^ 2 + y.2 ^ 2).

Equations

• NavierStokes.PhysicalClassBounds.cartesianRadius y = √(y.1 ^ 2 + y.2 ^ 2)

theorem NavierStokes.PhysicalClassBounds.cartesianRadius_smooth : ContDiffOn ℝ (↑⊤) cartesianRadius {y : PhysicalGraphBounds.Plane | y ≠ 0}

noncomputable def NavierStokes.PhysicalClassBounds.slowFast : PhysicalWaveSum.LiftPoint →L[ℝ] (ℝ × ℝ) × PhysicalGraphBounds.Plane

Slow order (T,Z) and the actual common auxiliary coordinate.

Equations

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

@[simp]

theorem NavierStokes.PhysicalClassBounds.slowFast_apply (x : PhysicalWaveSum.LiftPoint) : slowFast x = ((x.1.1, x.1.2.2.2), x.2)

theorem NavierStokes.PhysicalClassBounds.norm_slowFast_le : ‖slowFast‖ ≤ 1

noncomputable def NavierStokes.PhysicalClassBounds.cylindricalMap (x : PhysicalWaveSum.LiftPoint) : CylindricalPoint

Cylindrical map, given by (cartesianRadius (PhysicalGraphBounds.liftXY x), slowFast x).

Equations

• NavierStokes.PhysicalClassBounds.cylindricalMap x = (NavierStokes.PhysicalClassBounds.cartesianRadius (NavierStokes.PhysicalGraphBounds.liftXY x), NavierStokes.PhysicalClassBounds.slowFast x)

noncomputable def NavierStokes.PhysicalClassBounds.cylindricalDomain (a b : ℝ) : Set PhysicalWaveSum.LiftPoint

Cylindrical domain, given by (fun x => ‖PhysicalGraphBounds.liftXY x‖) ⁻¹' Ioo (a / 2) (b + 1).

Equations

• NavierStokes.PhysicalClassBounds.cylindricalDomain a b = (fun (x : NavierStokes.PhysicalWaveSum.LiftPoint) => ‖NavierStokes.PhysicalGraphBounds.liftXY x‖) ⁻¹' Set.Ioo (a / 2) (b + 1)

theorem NavierStokes.PhysicalClassBounds.cylindricalDomain_open (a b : ℝ) : IsOpen (cylindricalDomain a b)

theorem NavierStokes.PhysicalClassBounds.cylindricalDomain_axisFree {a b : ℝ} (ha : 0 < a) {x : PhysicalWaveSum.LiftPoint} (hx : x ∈ cylindricalDomain a b) : PhysicalGraphBounds.liftXY x ≠ 0

theorem NavierStokes.PhysicalClassBounds.cylindricalMap_smooth {a b : ℝ} (ha : 0 < a) : ContDiffOn ℝ (↑⊤) cylindricalMap (cylindricalDomain a b)

theorem NavierStokes.PhysicalClassBounds.cylindricalMap_positiveJets {a b : ℝ} (ha : 0 < a) (m : ℕ) : ∃ (B : ℝ), 1 ≤ B ∧ ∀ x ∈ cylindricalDomain a b, ∀ (j : ℕ), 1 ≤ j → j ≤ m → ‖iteratedFDeriv ℝ j cylindricalMap x‖ ≤ B

All positive jets of the actual radius map are uniformly bounded on a fixed padded annulus, regardless of slow or auxiliary coordinates.

theorem NavierStokes.PhysicalClassBounds.liftXY_commonLift (h : ℝ) (n d : ℕ) (z : ProblemStatement.SpaceTime) : PhysicalGraphBounds.liftXY (PhysicalWaveSum.commonLift h n d z) = (PhysicalGraphBounds.scaledRadial n) z

theorem NavierStokes.PhysicalClassBounds.cylindricalMap_commonLift (h : ℝ) (n d : ℕ) (z : ProblemStatement.SpaceTime) : cylindricalMap (PhysicalWaveSum.commonLift h n d z) = (cartesianRadius ((PhysicalGraphBounds.scaledRadial n) z), ((1 - z.1) / ChartScales.Q n, ChartScales.Q n ^ (-CoordinateAlgebra.D h) * z.2.ofLp 2), (CommonCoverSolve.coverPower d).symm (PhysicalGraphBounds.nativeGraph h n z))

The actual common graph has the expected cylindrical radius, scaled slow variables, and inverse-covered auxiliary coordinate.

theorem NavierStokes.PhysicalClassBounds.commonLift_mem_cylindricalDomain {a b : ℝ} (ha : 0 < a) (h : ℝ) (n d : ℕ) (z : ProblemStatement.SpaceTime) (hz : (PhysicalGraphBounds.scaledRadial n) z ∈ PhysicalGraphBounds.annulus a b) : PhysicalWaveSum.commonLift h n d z ∈ cylindricalDomain a b

noncomputable def NavierStokes.PhysicalClassBounds.cylindricalCommonChart {ι : Type u_2} {H : ℕ} (F : PhysicalWaveSum.WaveFamily H) (a b h r0 σ : ℝ) (ha : 0 < a) (f : ι → ℕ → CylindricalPoint → ℂ) (index : PhysicalWaveSum.WaveIndex H → ι) (he : ∀ (I : PhysicalWaveSum.WaveIndex H), F.amplitude I = fun (x : PhysicalWaveSum.LiftPoint) => ChartScales.Q (↑I.1).1 ^ σ • f (index I) (↑I.1).1 (cylindricalMap x)) : CommonChart F a b h r0 σ f

Direct adapter for a genuine cylindrical coefficient. No coordinate derivative estimate is assumed: the preceding theorems prove it.

Equations

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