Physical jets of coherent mean fields

The graph below is the actual common-cover cylindrical graph, with slow order (T,Z). It is identified with VariableGaugeMean.physicalToChartTZ, and its derivative estimates are derived from the actual physical graph and radius map. The final restriction is a single coherent physical field, not a sum over bands.

@[reducible, inline]

abbrev NavierStokes.PhysicalMeanJetBounds.Point : Type

Point: an abbreviation for PressureStream.Lift PhysicalGraphBounds.Plane.

Equations

• NavierStokes.PhysicalMeanJetBounds.Point = NavierStokes.PressureStream.Lift NavierStokes.PhysicalGraphBounds.Plane

noncomputable def NavierStokes.PhysicalMeanJetBounds.physicalPoint (h : ℝ) (w : ProblemStatement.SpaceTime) : Point

The unscaled physical cylindrical point with the actual auxiliary graph.

Equations

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

noncomputable def NavierStokes.PhysicalMeanJetBounds.graph (h : ℝ) (n d : ℕ) : ProblemStatement.SpaceTime → Point

A bounded-gap common-cover graph, in the mean-field coordinate order.

Equations

• NavierStokes.PhysicalMeanJetBounds.graph h n d = NavierStokes.PhysicalClassBounds.cylindricalMap ∘ NavierStokes.PhysicalWaveSum.commonLift h n d

theorem NavierStokes.PhysicalMeanJetBounds.cartesianRadius_smul {c : ℝ} (hc : 0 ≤ c) (y : PhysicalGraphBounds.Plane) : PhysicalClassBounds.cartesianRadius (c • y) = c * PhysicalClassBounds.cartesianRadius y

theorem NavierStokes.PhysicalMeanJetBounds.physicalToChartTZ_apply (h : ℝ) (n i : ℕ) (p : Point) : (VariableGaugeMean.physicalToChartTZ h n i) p = (MeanChartCompatibility.chartScale n * p.1, (ChartScales.Q n ^ (-1) * p.2.1.1, ChartScales.Q n ^ (-CoordinateAlgebra.D h) * p.2.1.2), (TemporalMeanUpdate.coverMap i) p.2.2)

theorem NavierStokes.PhysicalMeanJetBounds.graph_eq_physicalToChartTZ (h : ℝ) (n d : ℕ) (hd : d ≤ ChartScales.nativeIndex h n) (w : ProblemStatement.SpaceTime) : graph h n d w = (VariableGaugeMean.physicalToChartTZ h n (ChartScales.nativeIndex h n - d)) (physicalPoint h w)

Exact identification with the variable-gauge mean chart. The cover index is the native index minus the actual common-cover gap.

theorem NavierStokes.PhysicalMeanJetBounds.graph_smoothAt {a b : ℝ} (ha : 0 < a) (h : ℝ) (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus a b) : ContDiffAt ℝ (↑⊤) (graph h n d) w

Selection of a comparable dyadic band

theorem NavierStokes.PhysicalMeanJetBounds.Q_eq_half_pow (n : ℕ) : ChartScales.Q n = (1 / 2) ^ n

theorem NavierStokes.PhysicalMeanJetBounds.Q_add (n k : ℕ) : ChartScales.Q (n + k) = ChartScales.Q n * ChartScales.Q k

theorem NavierStokes.PhysicalMeanJetBounds.exists_comparable_band (N : ℕ) {q : ℝ} (hq : 0 < q) (hsmall : q ≤ ChartScales.Q N) : ∃ (n : ℕ), N ≤ n ∧ q ≤ ChartScales.Q n ∧ ChartScales.Q n < 2 * q

Every sufficiently small positive physical scale has a comparable band above any prescribed cutoff. No summation over bands is introduced.

The local, nonoscillatory graph estimate

theorem NavierStokes.PhysicalMeanJetBounds.common_stripped_physical_bound_local {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 2) (ha : 0 < a) (Δ m : ℕ) (g e A : ℝ) (hA : 0 ≤ A) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), 4 ≤ n → ∀ d ≤ Δ, ∀ (w : ProblemStatement.SpaceTime), (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus a b → |w.1| ≤ 1 → ∀ (q : ℝ), 0 < q → q / 2 ≤ ChartScales.Q n → ChartScales.Q n ≤ 2 * q → ∀ (f : PhysicalWaveSum.LiftPoint → E), LocalPhysicalCopyBounds.SmoothNear f (PhysicalWaveSum.commonLift h n d w) → (∀ i ≤ m, ‖iteratedFDeriv ℝ i f (PhysicalWaveSum.commonLift h n d w)‖ ≤ A * ChartScales.Q n ^ g * ChartScales.S n ^ e) → ‖iteratedFDeriv ℝ m (f ∘ PhysicalWaveSum.commonLift h n d) w‖ ≤ C * q ^ (g - (PhysicalGraphBounds.graphLoss m + 1))

noncomputable def NavierStokes.PhysicalMeanJetBounds.bandField {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : ℝ) (n d : ℕ) (degree : ℝ) (f : Point → E) : ProblemStatement.SpaceTime → E

Band field, defined pointwise by (ChartScales.Q n ^ (-degree)) • f (graph h n d w).

Equations

• NavierStokes.PhysicalMeanJetBounds.bandField h n d degree f w = NavierStokes.ChartScales.Q n ^ (-degree) • f (NavierStokes.PhysicalMeanJetBounds.graph h n d w)

noncomputable def NavierStokes.PhysicalMeanJetBounds.loss (degree : ℝ) (m : ℕ) : ℝ

Loss, given by PhysicalGraphBounds.graphLoss m + 1 + degree.

Equations

• NavierStokes.PhysicalMeanJetBounds.loss degree m = NavierStokes.PhysicalGraphBounds.graphLoss m + 1 + degree

theorem NavierStokes.PhysicalMeanJetBounds.bandField_jet_bound {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 2) (ha : 0 < a) (Δ m : ℕ) (gain degree e A : ℝ) (hA : 0 ≤ A) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), 4 ≤ n → ∀ d ≤ Δ, ∀ (w : ProblemStatement.SpaceTime), (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus a b → |w.1| ≤ 1 → ∀ (q : ℝ), 0 < q → q / 2 ≤ ChartScales.Q n → ChartScales.Q n ≤ 2 * q → ∀ (f : Point → E), LocalPhysicalCopyBounds.SmoothNear f (graph h n d w) → (∀ i ≤ m, ‖iteratedFDeriv ℝ i f (graph h n d w)‖ ≤ A * ChartScales.Q n ^ gain * ChartScales.S n ^ e) → ‖iteratedFDeriv ℝ m (bandField h n d degree f) w‖ ≤ C * q ^ (gain - loss degree m)

Actual cylindrical mean-field restriction. Both graph stages are differentiated using their proved jet bounds. Raw input smoothness is local.

The actual normalized slow coordinate

theorem NavierStokes.PhysicalMeanJetBounds.physicalQ_eq (h : ℝ) (w : ProblemStatement.SpaceTime) : PhysicalWaveSum.physicalQ h w = SimilarityCoordinates.coordinateQ (2 * h) (1 - w.1, w.2.ofLp 2)

theorem NavierStokes.PhysicalMeanJetBounds.graph_slow (h : ℝ) (n d : ℕ) (w : ProblemStatement.SpaceTime) : (graph h n d w).2.1 = ((1 - w.1) / ChartScales.Q n, ChartScales.Q n ^ (-CoordinateAlgebra.D h) * w.2.ofLp 2)

theorem NavierStokes.PhysicalMeanJetBounds.graph_slow_continuous (h : ℝ) (n d : ℕ) : Continuous fun (w : ProblemStatement.SpaceTime) => (graph h n d w).2.1

theorem NavierStokes.PhysicalMeanJetBounds.graph_radius (h : ℝ) (n d : ℕ) (w : ProblemStatement.SpaceTime) : (graph h n d w).1 = PolarCharts.radius ((PhysicalGraphBounds.scaledRadial n) w)

theorem NavierStokes.PhysicalMeanJetBounds.graph_radius_continuous (h : ℝ) (n d : ℕ) : Continuous fun (w : ProblemStatement.SpaceTime) => (graph h n d w).1

theorem NavierStokes.PhysicalMeanJetBounds.graph_time_pos (h : ℝ) (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : 0 < (graph h n d w).2.1.1

theorem NavierStokes.PhysicalMeanJetBounds.graph_q_eq {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : SimilarityCoordinates.coordinateQ (2 * h) (graph h n d w).2.1 = PhysicalWaveSum.physicalQ h w / ChartScales.Q n

theorem NavierStokes.PhysicalMeanJetBounds.graph_slow_normalized {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hlo : PhysicalWaveSum.physicalQ h w / 2 ≤ ChartScales.Q n) (hhi : ChartScales.Q n ≤ 2 * PhysicalWaveSum.physicalQ h w) : (graph h n d w).2.1 ∈ PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 4) 4

theorem NavierStokes.PhysicalMeanJetBounds.graph_length_pos {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : 0 < VariableGaugeMean.qLength (2 * h) (graph h n d w).2.1

theorem NavierStokes.PhysicalMeanJetBounds.graph_length_continuousAt {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : ContinuousAt (fun (z : ProblemStatement.SpaceTime) => VariableGaugeMean.qLength (2 * h) (graph h n d z).2.1) w

theorem NavierStokes.PhysicalMeanJetBounds.graph_length_bounds {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hlo : PhysicalWaveSum.physicalQ h w / 2 ≤ ChartScales.Q n) (hhi : ChartScales.Q n ≤ 2 * PhysicalWaveSum.physicalQ h w) : 1 / 2 ≤ VariableGaugeMean.qLength (2 * h) (graph h n d w).2.1 ∧ VariableGaugeMean.qLength (2 * h) (graph h n d w).2.1 ≤ 2

One physical field represented in all valid bands

structure NavierStokes.PhysicalMeanJetBounds.CoherentFamily (h degree : ℝ) (N Δ : ℕ) (U : Set PhysicalGraphBounds.Plane) (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] : Type u_1

Exact chart coherence for the same physical lifted field. The data do not define a sum of band fields and contain no physical derivative estimate.

• native : ℕ → Point → E

  Native of CoherentFamily, of type ℕ → Point → E.

• physical : Point → E

  Physical of CoherentFamily, of type Point → E.

• gap : ℕ → ℕ

  Gap of CoherentFamily, of type ℕ → ℕ.

• gap_le (n : ℕ) : n ≥ N → self.gap n ≤ Δ
• gap_native (n : ℕ) : n ≥ N → self.gap n ≤ ChartScales.nativeIndex h n
• coherent (n : ℕ) : n ≥ N → ∀ (z : Point), 0 < z.2.1.1 → ((VariableGaugeMean.physicalToChartTZ h n (ChartScales.nativeIndex h n - self.gap n)) z).2.1 ∈ U → self.physical z = ChartScales.Q n ^ (-degree) • self.native n ((VariableGaugeMean.physicalToChartTZ h n (ChartScales.nativeIndex h n - self.gap n)) z)

noncomputable def NavierStokes.PhysicalMeanJetBounds.CoherentFamily.field {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {h degree : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : CoherentFamily h degree N Δ U E) : ProblemStatement.SpaceTime → E

Field, given by D.physical ∘ physicalPoint h.

Equations

• D.field = D.physical ∘ NavierStokes.PhysicalMeanJetBounds.physicalPoint h

theorem NavierStokes.PhysicalMeanJetBounds.CoherentFamily.field_eq {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {h degree : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : CoherentFamily h degree N Δ U E) (n : ℕ) (hn : N ≤ n) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hU : (graph h n (D.gap n) w).2.1 ∈ U) : D.field w = bandField h n (D.gap n) degree (D.native n) w

theorem NavierStokes.PhysicalMeanJetBounds.CoherentFamily.field_germ {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {h degree : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : CoherentFamily h degree N Δ U E) (hU : IsOpen U) (n : ℕ) (hn : N ≤ n) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hu : (graph h n (D.gap n) w).2.1 ∈ U) : D.field =ᶠ[nhds w] bandField h n (D.gap n) degree (D.native n)

def NavierStokes.PhysicalMeanJetBounds.NativeSupport {E : Type} [NormedAddCommGroup E] (h a b : ℝ) (N : ℕ) (U : Set PhysicalGraphBounds.Plane) (f : ℕ → Point → E) : Prop

Supported native coefficients, stated for an arbitrary normed target. For real-valued coefficients this is the actual SupportedGauge condition.

Equations

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

theorem NavierStokes.PhysicalMeanJetBounds.CoherentFamily.native_ratio_on_tsupport {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : CoherentFamily h degree N Δ U E) (hh : 0 < h) (hh1 : h < 1 / 2) (hU : IsOpen U) (hs : NativeSupport h a b N U D.native) (n : ℕ) (hn : N ≤ n) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hu : (graph h n (D.gap n) w).2.1 ∈ U) (hts : w ∈ tsupport D.field) : (graph h n (D.gap n) w).1 / VariableGaugeMean.qLength (2 * h) (graph h n (D.gap n) w).2.1 ∈ Set.Icc a b

theorem NavierStokes.PhysicalMeanJetBounds.CoherentFamily.annulus_on_tsupport {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : CoherentFamily h degree N Δ U E) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hU : IsOpen U) (hs : NativeSupport h a b N U D.native) (n : ℕ) (hn : N ≤ n) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hu : (graph h n (D.gap n) w).2.1 ∈ U) (hlo : PhysicalWaveSum.physicalQ h w / 2 ≤ ChartScales.Q n) (hhi : ChartScales.Q n ≤ 2 * PhysicalWaveSum.physicalQ h w) (hts : w ∈ tsupport D.field) : (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus (a / 4) (2 * b)

Native moving-annulus support gives a fixed Cartesian chart annulus at every supported physical point with a comparable band.

def NavierStokes.PhysicalMeanJetBounds.NativeJets {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (N : ℕ) (U : Set PhysicalGraphBounds.Plane) (gain : ℝ) (f : ℕ → Point → E) : Prop

Band-independent native jets after absorbing the actual flat weight.

Equations

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

theorem NavierStokes.PhysicalMeanJetBounds.CoherentFamily.field_jet_bound {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : 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 / 4) 4 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : NativeSupport h a b N U D.native) {gain : ℝ} (hj : 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 - loss degree m)

A uniform estimate for the same coherent physical field. A comparable band is selected at each point and used through an exact field germ.

theorem NavierStokes.PhysicalMeanJetBounds.CoherentFamily.field_smoothAt {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : 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 / 4) 4 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : 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

The local mean-class consumer

theorem NavierStokes.PhysicalMeanJetBounds.NativeJets.of_localBandJets {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {h α : ℝ} {N : ℕ} {U : Set PhysicalGraphBounds.Plane} {ε L : ℕ → ℝ} {f : ℕ → Point → E} (hj : PhysicalMeanDomain.LocalBandJets U ε L α f) (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) : NativeJets N U (h * α) f

theorem NavierStokes.PhysicalMeanJetBounds.CoherentFamily.field_jet_bound_of_localBandJets {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : 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 / 4) 4 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : 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 * α - loss degree m)

Incoming local band jets of any real class exponent give physical Cartesian jets of that same coherent field.

noncomputable def NavierStokes.PhysicalMeanJetBounds.physicalDomain (h : ℝ) (N : ℕ) : Set ProblemStatement.SpaceTime

The open physical region on which the local native hypotheses imply smoothness, including the zero neighborhood at the spatial axis.

Equations

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

theorem NavierStokes.PhysicalMeanJetBounds.physicalDomain_open {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (N : ℕ) : IsOpen (physicalDomain h N)

theorem NavierStokes.PhysicalMeanJetBounds.CoherentFamily.field_smooth {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : 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 / 4) 4 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : NativeSupport h a b N U D.native) : ContDiffOn ℝ (↑⊤) D.field (physicalDomain h N)

@[simp]

theorem NavierStokes.PhysicalMeanJetBounds.loss_velocity (h : ℝ) (m : ℕ) : loss (CoordinateAlgebra.A h) m = PhysicalGraphBounds.graphLoss m + 1 + CoordinateAlgebra.A h

theorem NavierStokes.PhysicalMeanJetBounds.loss_stream (h : ℝ) (m : ℕ) : loss (CoordinateAlgebra.A h - 1 / 2) m = PhysicalGraphBounds.graphLoss m + 1 + h

@[simp]

theorem NavierStokes.PhysicalMeanJetBounds.loss_pressure (h : ℝ) (m : ℕ) : loss (2 * CoordinateAlgebra.A h) m = PhysicalGraphBounds.graphLoss m + 1 + 2 * CoordinateAlgebra.A h

The actual Cartesian angular frame

noncomputable def NavierStokes.PhysicalMeanJetBounds.angularVector (y : PhysicalGraphBounds.Plane) : ProblemStatement.Space

The Cartesian unit angular direction, with the usual totalized value at the axis. Axis regularity below comes from the supported coefficient.

Equations

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

theorem NavierStokes.PhysicalMeanJetBounds.angularVector_smooth : ContDiffOn ℝ (↑⊤) angularVector {y : PhysicalGraphBounds.Plane | y ≠ 0}

theorem NavierStokes.PhysicalMeanJetBounds.angularVector_smul {c : ℝ} (hc : 0 < c) (y : PhysicalGraphBounds.Plane) : angularVector (c • y) = angularVector y

theorem NavierStokes.PhysicalMeanJetBounds.smul_jet_bound {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) {f : D → ℝ} {g : D → E} (hf : ContDiffOn ℝ (↑⊤) f U) (hg : ContDiffOn ℝ (↑⊤) g U) {z : D} (hz : z ∈ U) {m j : ℕ} (hj : j ≤ m) {A B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hfa : ∀ i ≤ m, ‖iteratedFDeriv ℝ i f z‖ ≤ A) (hgb : ∀ i ≤ m, ‖iteratedFDeriv ℝ i g z‖ ≤ B) : ‖iteratedFDeriv ℝ j (fun (x : D) => f x • g x) z‖ ≤ 2 ^ m * A * B

A local Leibniz estimate for scalar multiplication, including order zero. It uses actual Fréchet tensors on the supplied open set.

theorem NavierStokes.PhysicalMeanJetBounds.angularVector_lift_smooth {a b : ℝ} (ha : 0 < a) : ContDiffOn ℝ (↑⊤) (angularVector ∘ ⇑PhysicalGraphBounds.liftXY) (PhysicalClassBounds.cylindricalDomain a b)

theorem NavierStokes.PhysicalMeanJetBounds.angularVector_lift_jet_bound {a b : ℝ} (ha : 0 < a) (m : ℕ) : ∃ (B : ℝ), 1 ≤ B ∧ ∀ x ∈ PhysicalClassBounds.cylindricalDomain a b, ∀ j ≤ m, ‖iteratedFDeriv ℝ j (angularVector ∘ ⇑PhysicalGraphBounds.liftXY) x‖ ≤ B

The angular frame has uniform jets on the fixed padded annulus. No slow or auxiliary coordinate enters these constants.

theorem NavierStokes.PhysicalMeanJetBounds.angularVector_scaledRadial (n : ℕ) (w : ProblemStatement.SpaceTime) : angularVector ((PhysicalGraphBounds.scaledRadial n) w) = angularVector (PhysicalGraphBounds.radialProjection w)

noncomputable def NavierStokes.PhysicalMeanJetBounds.bandAngularField (h : ℝ) (n d : ℕ) (degree : ℝ) (f : Point → ℝ) : ProblemStatement.VelocityField

This is the direct angular vector when degree = A h, and the azimuthal stream potential when degree = A h - 1/2.

Equations

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

theorem NavierStokes.PhysicalMeanJetBounds.bandAngularField_jet_bound {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 2) (ha : 0 < a) (Δ m : ℕ) (gain degree e A : ℝ) (hA : 0 ≤ A) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), 4 ≤ n → ∀ d ≤ Δ, ∀ (w : ProblemStatement.SpaceTime), (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus a b → |w.1| ≤ 1 → ∀ (q : ℝ), 0 < q → q / 2 ≤ ChartScales.Q n → ChartScales.Q n ≤ 2 * q → ∀ (f : Point → ℝ), LocalPhysicalCopyBounds.SmoothNear f (graph h n d w) → (∀ i ≤ m, ‖iteratedFDeriv ℝ i f (graph h n d w)‖ ≤ A * ChartScales.Q n ^ gain * ChartScales.S n ^ e) → ‖iteratedFDeriv ℝ m (bandAngularField h n d degree f) w‖ ≤ C * q ^ (gain - loss degree m)

The actual angular direction is incorporated before estimating the physical graph. Thus it incurs no additional power loss.

noncomputable def NavierStokes.PhysicalMeanJetBounds.CoherentFamily.angularField {h degree : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : CoherentFamily h degree N Δ U ℝ) : ProblemStatement.VelocityField

The actual Cartesian vector associated with the coherent scalar field. The formula applies both to angular velocity and stream potential.

Equations

• D.angularField w = D.field w • NavierStokes.PhysicalMeanJetBounds.angularVector (NavierStokes.PhysicalGraphBounds.radialProjection w)

theorem NavierStokes.PhysicalMeanJetBounds.CoherentFamily.angularField_formula {h degree : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : CoherentFamily h degree N Δ U ℝ) (w : ProblemStatement.SpaceTime) : D.angularField w = (-w.2.ofLp 1 / PhysicalClassBounds.cartesianRadius (PhysicalGraphBounds.radialProjection w) * D.field w) • ProblemStatement.coordinateVector 0 + (w.2.ofLp 0 / PhysicalClassBounds.cartesianRadius (PhysicalGraphBounds.radialProjection w) * D.field w) • ProblemStatement.coordinateVector 1

theorem NavierStokes.PhysicalMeanJetBounds.CoherentFamily.angularField_germ {h degree : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : CoherentFamily h degree N Δ U ℝ) (hU : IsOpen U) (n : ℕ) (hn : N ≤ n) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hu : (graph h n (D.gap n) w).2.1 ∈ U) : D.angularField =ᶠ[nhds w] bandAngularField h n (D.gap n) degree (D.native n)

theorem NavierStokes.PhysicalMeanJetBounds.CoherentFamily.angularField_zero_germ {h degree : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : CoherentFamily h degree N Δ U ℝ) {w : ProblemStatement.SpaceTime} (hw : w ∉ tsupport D.field) : D.angularField =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.PhysicalMeanJetBounds.CoherentFamily.angularField_jet_bound {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : 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 / 4) 4 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : NativeSupport h a b N U D.native) {gain : ℝ} (hj : 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 - loss degree m)

theorem NavierStokes.PhysicalMeanJetBounds.CoherentFamily.angularField_smoothAt {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : 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 / 4) 4 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : 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.PhysicalMeanJetBounds.CoherentFamily.angularField_smooth {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : 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 / 4) 4 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : NativeSupport h a b N U D.native) : ContDiffOn ℝ (↑⊤) D.angularField (physicalDomain h N)

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

The actual spatial curl of the azimuthal stream potential. Its fixed physical loss uses one more derivative; no derivative is postulated.

theorem NavierStokes.PhysicalMeanJetBounds.CoherentFamily.curl_angularField_smooth {h degree a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : 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 / 4) 4 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : NativeSupport h a b N U D.native) : ContDiffOn ℝ (↑⊤) (SpatialCurl.spatialCurl D.angularField) (physicalDomain h N)

Genuine moving-weight mean classes

theorem NavierStokes.PhysicalMeanJetBounds.NativeJets.of_movingMeanClass {h α a b cL cR : ℝ} (R : LocalSignedRequest.SlowRegion (2 * h)) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {f : ℕ → Point → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain R.carrier)) (hs : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength (2 * h)) R.carrier (f n)) (hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData R a b cL cR ha hcL hcR ε L hε hεone hL) α f) (N : ℕ) (hεnative : ∀ n ≥ N, ε n = ChartScales.epsilon h n) {C : ℝ} {p : ℕ} (hC : 1 ≤ C) (hpoly : ∀ n ≥ N, L n ≤ C * ChartScales.S n ^ p) : NativeJets N R.carrier (h * α) f

The existing moving two-edge mean class supplies the native input jets. The only extra regularity is the genuine supported extension across the edges, on the valid slow region.

Coherence of the actual reconstructed pressure and stream

theorem NavierStokes.PhysicalMeanJetBounds.meanPressure_fiberLocal (d a b M : ℝ) (hab : a < b) (ell : PhysicalGraphBounds.Plane → ℝ) (v : PressureStream.Plane) : PhysicalMeanDomain.FiberLocal (VariableGaugeMean.meanPressure d a b M hab ell v)

theorem NavierStokes.PhysicalMeanJetBounds.streamPotential_fiberLocal (d a b M : ℝ) (ell : PhysicalGraphBounds.Plane → ℝ) (v : PressureStream.Plane) : PhysicalMeanDomain.FiberLocal (VariableGaugeMean.streamPotential d a b M ell v)

noncomputable def NavierStokes.PhysicalMeanJetBounds.CoherentFamily.reconstructPressure {h a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : CoherentFamily h (2 * CoordinateAlgebra.A h + 1 / 2) N Δ U ℝ) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) {d : ℝ} (hd : 0 < d) (M : ℝ) (hU : IsOpen U) (hf : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hp : ∀ n ≥ N, PhysicalMeanDomain.PeriodicOn U (D.native n)) (hs : NativeSupport h a b N U D.native) : CoherentFamily h (2 * CoordinateAlgebra.A h) N Δ U ℝ

Reconstruct the physical pressure from the coherent momentum source. The output coherence is proved from the actual integral operator; it is not an additional premise.

Equations

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

noncomputable def NavierStokes.PhysicalMeanJetBounds.CoherentFamily.reconstructStream {h a b : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : CoherentFamily h (CoordinateAlgebra.A h) N Δ U ℝ) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) {d : ℝ} (hd : 0 < d) (M : ℝ) (hU : IsOpen U) (hf : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : NativeSupport h a b N U D.native) : CoherentFamily h (CoordinateAlgebra.A h - 1 / 2) N Δ U ℝ

Reconstruct the azimuthal stream potential from a coherent axial source. Its physical degree is exactly A h - 1/2.

Equations

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