Physical mean estimates on the actual normalized slow region

The comparable band satisfies q ≤ Q_n < 2q. Its normalized slow scale therefore lies strictly in (1/2, 2). The estimates below use that actual open region and a genuine local equality with the selected band field. The field itself is the existing coherent physical field, not a band sum.

theorem NavierStokes.LocalMeanPhysicalBounds.exists_field_germ {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {h degree : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U E) (hh : 0 < h) (hh1 : h < 1 / 2) (hU : IsOpen U) (hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hsmall : PhysicalWaveSum.physicalQ h w ≤ ChartScales.Q N) : ∃ (n : ℕ), N ≤ n ∧ PhysicalWaveSum.physicalQ h w ≤ ChartScales.Q n ∧ ChartScales.Q n < 2 * PhysicalWaveSum.physicalQ h w ∧ (PhysicalMeanJetBounds.graph h n (D.gap n) w).2.1 ∈ U ∧ D.field =ᶠ[nhds w] PhysicalMeanJetBounds.bandField h n (D.gap n) degree (D.native n)

Band selection gives an actual field germ on the original native region, even when the physical point lies on a band-selection boundary.

theorem NavierStokes.LocalMeanPhysicalBounds.exists_angularField_germ {h degree : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U ℝ) (hh : 0 < h) (hh1 : h < 1 / 2) (hU : IsOpen U) (hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hsmall : PhysicalWaveSum.physicalQ h w ≤ ChartScales.Q N) : ∃ (n : ℕ), N ≤ n ∧ PhysicalWaveSum.physicalQ h w ≤ ChartScales.Q n ∧ ChartScales.Q n < 2 * PhysicalWaveSum.physicalQ h w ∧ (PhysicalMeanJetBounds.graph h n (D.gap n) w).2.1 ∈ U ∧ D.angularField =ᶠ[nhds w] PhysicalMeanJetBounds.bandAngularField h n (D.gap n) degree (D.native n)

theorem NavierStokes.LocalMeanPhysicalBounds.field_jet_bound {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U E) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hN : 4 ≤ N) (hU : IsOpen U) (hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanJetBounds.NativeSupport h a b N U D.native) {gain : ℝ} (hj : PhysicalMeanJetBounds.NativeJets N U gain D.native) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ PhysicalWaveSum.preterminal, |w.1| ≤ 1 → PhysicalWaveSum.physicalQ h w ≤ ChartScales.Q N → ‖iteratedFDeriv ℝ m D.field w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (gain - PhysicalMeanJetBounds.loss degree m)

The original physical loss holds on the smaller, actual native region.

theorem NavierStokes.LocalMeanPhysicalBounds.field_smoothAt {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U E) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hU : IsOpen U) (hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanJetBounds.NativeSupport h a b N U D.native) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hsmall : PhysicalWaveSum.physicalQ h w ≤ ChartScales.Q N) : ContDiffAt ℝ (↑⊤) D.field w

theorem NavierStokes.LocalMeanPhysicalBounds.field_smooth {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U E) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hU : IsOpen U) (hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanJetBounds.NativeSupport h a b N U D.native) : ContDiffOn ℝ (↑⊤) D.field (PhysicalMeanJetBounds.physicalDomain h N)

theorem NavierStokes.LocalMeanPhysicalBounds.angularField_jet_bound {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U ℝ) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hN : 4 ≤ N) (hU : IsOpen U) (hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanJetBounds.NativeSupport h a b N U D.native) {gain : ℝ} (hj : PhysicalMeanJetBounds.NativeJets N U gain D.native) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ PhysicalWaveSum.preterminal, |w.1| ≤ 1 → PhysicalWaveSum.physicalQ h w ≤ ChartScales.Q N → ‖iteratedFDeriv ℝ m D.angularField w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (gain - PhysicalMeanJetBounds.loss degree m)

theorem NavierStokes.LocalMeanPhysicalBounds.angularField_smoothAt {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U ℝ) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hU : IsOpen U) (hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanJetBounds.NativeSupport h a b N U D.native) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hsmall : PhysicalWaveSum.physicalQ h w ≤ ChartScales.Q N) : ContDiffAt ℝ (↑⊤) D.angularField w

theorem NavierStokes.LocalMeanPhysicalBounds.angularField_smooth {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U ℝ) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hU : IsOpen U) (hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanJetBounds.NativeSupport h a b N U D.native) : ContDiffOn ℝ (↑⊤) D.angularField (PhysicalMeanJetBounds.physicalDomain h N)

theorem NavierStokes.LocalMeanPhysicalBounds.curl_angularField_jet_bound {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U ℝ) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hN : 4 ≤ N) (hU : IsOpen U) (hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanJetBounds.NativeSupport h a b N U D.native) {gain : ℝ} (hj : PhysicalMeanJetBounds.NativeJets N U gain D.native) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ PhysicalMeanJetBounds.physicalDomain h N, |w.1| ≤ 1 → ‖iteratedFDeriv ℝ m (SpatialCurl.spatialCurl D.angularField) w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (gain - PhysicalMeanJetBounds.loss degree (m + 1))

Curl costs one actual derivative, with the same fixed PMJB loss.

theorem NavierStokes.LocalMeanPhysicalBounds.curl_angularField_smooth {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U ℝ) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hU : IsOpen U) (hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanJetBounds.NativeSupport h a b N U D.native) : ContDiffOn ℝ (↑⊤) (SpatialCurl.spatialCurl D.angularField) (PhysicalMeanJetBounds.physicalDomain h N)

Native class inputs on the same region

theorem NavierStokes.LocalMeanPhysicalBounds.field_jet_bound_of_localBandJets {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U E) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hN : 4 ≤ N) (hU : IsOpen U) (hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanJetBounds.NativeSupport h a b N U D.native) {α : ℝ} {ε L : ℕ → ℝ} (hj : PhysicalMeanDomain.LocalBandJets U ε L α D.native) (hε : ∀ n ≥ N, ε n = ChartScales.epsilon h n) (hL0 : ∀ n ≥ N, 0 ≤ L n) {C : ℝ} {p : ℕ} (hC : 1 ≤ C) (hL : ∀ n ≥ N, L n ≤ C * ChartScales.S n ^ p) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ w ∈ PhysicalWaveSum.preterminal, |w.1| ≤ 1 → PhysicalWaveSum.physicalQ h w ≤ ChartScales.Q N → ‖iteratedFDeriv ℝ m D.field w‖ ≤ K * PhysicalWaveSum.physicalQ h w ^ (h * α - PhysicalMeanJetBounds.loss degree m)

theorem NavierStokes.LocalMeanPhysicalBounds.angularField_jet_bound_of_localBandJets {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U ℝ) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hN : 4 ≤ N) (hU : IsOpen U) (hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanJetBounds.NativeSupport h a b N U D.native) {α : ℝ} {ε L : ℕ → ℝ} (hj : PhysicalMeanDomain.LocalBandJets U ε L α D.native) (hε : ∀ n ≥ N, ε n = ChartScales.epsilon h n) (hL0 : ∀ n ≥ N, 0 ≤ L n) {C : ℝ} {p : ℕ} (hC : 1 ≤ C) (hL : ∀ n ≥ N, L n ≤ C * ChartScales.S n ^ p) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ w ∈ PhysicalWaveSum.preterminal, |w.1| ≤ 1 → PhysicalWaveSum.physicalQ h w ≤ ChartScales.Q N → ‖iteratedFDeriv ℝ m D.angularField w‖ ≤ K * PhysicalWaveSum.physicalQ h w ^ (h * α - PhysicalMeanJetBounds.loss degree m)

theorem NavierStokes.LocalMeanPhysicalBounds.curl_angularField_jet_bound_of_localBandJets {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U ℝ) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hN : 4 ≤ N) (hU : IsOpen U) (hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanJetBounds.NativeSupport h a b N U D.native) {α : ℝ} {ε L : ℕ → ℝ} (hj : PhysicalMeanDomain.LocalBandJets U ε L α D.native) (hε : ∀ n ≥ N, ε n = ChartScales.epsilon h n) (hL0 : ∀ n ≥ N, 0 ≤ L n) {C : ℝ} {p : ℕ} (hC : 1 ≤ C) (hL : ∀ n ≥ N, L n ≤ C * ChartScales.S n ^ p) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ w ∈ PhysicalMeanJetBounds.physicalDomain h N, |w.1| ≤ 1 → ‖iteratedFDeriv ℝ m (SpatialCurl.spatialCurl D.angularField) w‖ ≤ K * PhysicalWaveSum.physicalQ h w ^ (h * α - PhysicalMeanJetBounds.loss degree (m + 1))

Open physical sublevel interfaces

theorem NavierStokes.LocalMeanPhysicalBounds.field_sublevel_smooth {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U E) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hU : IsOpen U) (hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanJetBounds.NativeSupport h a b N U D.native) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) : ContDiffOn ℝ (↑⊤) D.field (CutStageEstimates.physicalSublevel h qbig)

theorem NavierStokes.LocalMeanPhysicalBounds.angularField_sublevel_smooth {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U ℝ) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hU : IsOpen U) (hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanJetBounds.NativeSupport h a b N U D.native) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) : ContDiffOn ℝ (↑⊤) D.angularField (CutStageEstimates.physicalSublevel h qbig)

theorem NavierStokes.LocalMeanPhysicalBounds.curl_angularField_sublevel_smooth {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U ℝ) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hU : IsOpen U) (hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanJetBounds.NativeSupport h a b N U D.native) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) : ContDiffOn ℝ (↑⊤) (SpatialCurl.spatialCurl D.angularField) (CutStageEstimates.physicalSublevel h qbig)

theorem NavierStokes.LocalMeanPhysicalBounds.field_sublevel_bound {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U E) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hN : 4 ≤ N) (hU : IsOpen U) (hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanJetBounds.NativeSupport h a b N U D.native) {gain : ℝ} (hj : PhysicalMeanJetBounds.NativeJets N U gain D.native) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m D.field w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (gain - PhysicalMeanJetBounds.loss degree m)

theorem NavierStokes.LocalMeanPhysicalBounds.angularField_sublevel_bound {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U ℝ) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hN : 4 ≤ N) (hU : IsOpen U) (hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanJetBounds.NativeSupport h a b N U D.native) {gain : ℝ} (hj : PhysicalMeanJetBounds.NativeJets N U gain D.native) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m D.angularField w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (gain - PhysicalMeanJetBounds.loss degree m)

theorem NavierStokes.LocalMeanPhysicalBounds.curl_angularField_sublevel_bound {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U ℝ) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hN : 4 ≤ N) (hU : IsOpen U) (hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanJetBounds.NativeSupport h a b N U D.native) {gain : ℝ} (hj : PhysicalMeanJetBounds.NativeJets N U gain D.native) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m (SpatialCurl.spatialCurl D.angularField) w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (gain - PhysicalMeanJetBounds.loss degree (m + 1))