Physical waves on common covers and locally finite label sums

Cover changes are the actual powers of J_g. Bounds use actual Fréchet derivatives and the constructed dyadic and spatial masks.

@[reducible, inline]

abbrev NavierStokes.PhysicalWaveSum.Plane : Type

Plane: an abbreviation for PhysicalGraphBounds.Plane.

Equations

• NavierStokes.PhysicalWaveSum.Plane = NavierStokes.PhysicalGraphBounds.Plane

@[reducible, inline]

abbrev NavierStokes.PhysicalWaveSum.LiftPoint : Type

Lift point: an abbreviation for PhysicalGraphBounds.LiftPoint.

Equations

• NavierStokes.PhysicalWaveSum.LiftPoint = NavierStokes.PhysicalGraphBounds.LiftPoint

@[reducible, inline]

abbrev NavierStokes.PhysicalWaveSum.Label : Type

Label: an abbreviation for SlotColoring.Label.

Equations

• NavierStokes.PhysicalWaveSum.Label = NavierStokes.SlotColoring.Label

@[reducible, inline]

abbrev NavierStokes.PhysicalWaveSum.Position : Type

Position: an abbreviation for SlotColoring.Position.

Equations

• NavierStokes.PhysicalWaveSum.Position = NavierStokes.SlotColoring.Position

noncomputable def NavierStokes.PhysicalWaveSum.downLift (d : ℕ) : LiftPoint →L[ℝ] LiftPoint

Change only the auxiliary coordinate from native to common level.

Equations

• NavierStokes.PhysicalWaveSum.downLift d = (ContinuousLinearMap.id ℝ NavierStokes.PhysicalGraphBounds.ChartPoint).prodMap ↑(NavierStokes.CommonCoverSolve.coverPower d).symm

noncomputable def NavierStokes.PhysicalWaveSum.upLift (d : ℕ) : LiftPoint →L[ℝ] LiftPoint

Up lift, given by (ContinuousLinearMap.id ℝ PhysicalGraphBounds.ChartPoint).prodMap (CommonCoverSolve.coverPower d : Plane →L[ℝ] Plane).

Equations

• NavierStokes.PhysicalWaveSum.upLift d = (ContinuousLinearMap.id ℝ NavierStokes.PhysicalGraphBounds.ChartPoint).prodMap ↑(NavierStokes.CommonCoverSolve.coverPower d)

@[simp]

theorem NavierStokes.PhysicalWaveSum.downLift_apply (d : ℕ) (y : LiftPoint) : (downLift d) y = (y.1, (CommonCoverSolve.coverPower d).symm y.2)

@[simp]

theorem NavierStokes.PhysicalWaveSum.upLift_apply (d : ℕ) (y : LiftPoint) : (upLift d) y = (y.1, (CommonCoverSolve.coverPower d) y.2)

theorem NavierStokes.PhysicalWaveSum.up_down (d : ℕ) (y : LiftPoint) : (upLift d) ((downLift d) y) = y

theorem NavierStokes.PhysicalWaveSum.down_up (d : ℕ) (y : LiftPoint) : (downLift d) ((upLift d) y) = y

noncomputable def NavierStokes.PhysicalWaveSum.coverBound (Δ : ℕ) : ℝ

Cover bound, given by 1 + CommonCoverSolve.coveringBound Δ.

Equations

• NavierStokes.PhysicalWaveSum.coverBound Δ = 1 + NavierStokes.CommonCoverSolve.coveringBound Δ

theorem NavierStokes.PhysicalWaveSum.coverBound_ge_one (Δ : ℕ) : 1 ≤ coverBound Δ

theorem NavierStokes.PhysicalWaveSum.norm_downLift_le {d Δ : ℕ} (hd : d ≤ Δ) : ‖downLift d‖ ≤ coverBound Δ

theorem NavierStokes.PhysicalWaveSum.norm_upLift_le {d Δ : ℕ} (hd : d ≤ Δ) : ‖upLift d‖ ≤ coverBound Δ

noncomputable def NavierStokes.PhysicalWaveSum.commonLift (h : ℝ) (n d : ℕ) : ProblemStatement.SpaceTime → LiftPoint

Common lift, given by downLift d ∘ PhysicalGraphBounds.physicalLift h n.

Equations

• NavierStokes.PhysicalWaveSum.commonLift h n d = ⇑(NavierStokes.PhysicalWaveSum.downLift d) ∘ NavierStokes.PhysicalGraphBounds.physicalLift h n

theorem NavierStokes.PhysicalWaveSum.commonLift_formula (h : ℝ) (n d : ℕ) (hd : d ≤ ChartScales.nativeIndex h n) (w : ProblemStatement.SpaceTime) : commonLift h n d w = (PhysicalGraphBounds.physicalChart h n w, (SlotGeometry.cover ^ (ChartScales.nativeIndex h n - d)) (PhysicalGraphBounds.radialProfile (ChartScales.radialExponent h) (PhysicalGraphBounds.radialProjection w) + w.1 • PhysicalGraphBounds.timeDirection))

The changed coordinate is exactly J_g^(i(n)-d) Y, when the gap does not exceed the native index. No periodicity of the source is assumed.

theorem NavierStokes.PhysicalWaveSum.commonLift_smoothAt (h : ℝ) (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : PhysicalGraphBounds.radialProjection w ≠ 0) : ContDiffAt ℝ (↑⊤) (commonLift h n d) w

theorem NavierStokes.PhysicalWaveSum.downLift_jet_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : LiftPoint → E} (hf : ContDiff ℝ (↑⊤) f) {d Δ m : ℕ} (hd : d ≤ Δ) (y : LiftPoint) {B : ℝ} (hB : 0 ≤ B) (hb : ∀ i ≤ m, ‖iteratedFDeriv ℝ i f ((downLift d) y)‖ ≤ B) (i : ℕ) : i ≤ m → ‖iteratedFDeriv ℝ i (f ∘ ⇑(downLift d)) y‖ ≤ B * coverBound Δ ^ m

theorem NavierStokes.PhysicalWaveSum.common_stripped_physical_bound {E : Type u_1} [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 : LiftPoint → E), ContDiff ℝ (↑⊤) f → (∀ i ≤ m, ‖iteratedFDeriv ℝ i f (commonLift h n d w)‖ ≤ A * ChartScales.Q n ^ g * ChartScales.S n ^ e) → ‖iteratedFDeriv ℝ m (f ∘ commonLift h n d) w‖ ≤ C * q ^ (g - (PhysicalGraphBounds.graphLoss m + 1))

Common-cover descent changes the constant, preserving the native graph loss and arbitrary input gain. The source may live only on the coarsest covering torus.

structure NavierStokes.PhysicalWaveSum.CarrierData : Type

Native phase data remain distinct from a source on a common cover.

• chart : PolarCharts.Index

  Chart of CarrierData, of type PolarCharts.Index.

• center : Plane

  Center of CarrierData, of type Plane.

• angular : ℝ

  Angular of CarrierData, of type ℝ.

• axial : ℝ

  Axial of CarrierData, of type ℝ.

• radial : ℝ

  Radial of CarrierData, of type ℝ.

• F : PhysicalGraphBounds.Slow → ℝ

  F of CarrierData, of type PhysicalGraphBounds.Slow → ℝ.

• G : PhysicalGraphBounds.Slow → ℝ

  Geometric data of CarrierData, of type PhysicalGraphBounds.Slow → ℝ.

noncomputable def NavierStokes.PhysicalWaveSum.CarrierData.phase (c : CarrierData) (a h : ℝ) (n : ℕ) (r0 : ℝ) : LiftPoint → ℝ

Phase, given by PhysicalGraphBounds.liftedPhase (PolarCharts.chart a c.chart) h n c.center r0 c.angular c.axial c.radial c.F c.G.

Equations

• c.phase a h n r0 = NavierStokes.PhysicalGraphBounds.liftedPhase (NavierStokes.PolarCharts.chart a c.chart) h n c.center r0 c.angular c.axial c.radial c.F c.G

noncomputable def NavierStokes.PhysicalWaveSum.commonWave (a h : ℝ) (n d : ℕ) (r0 : ℝ) (c : CarrierData) (amp : LiftPoint → ℂ) (j : ℤ) (w : ProblemStatement.SpaceTime) : ℂ

Common wave, constructed using amp.

Equations

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

theorem NavierStokes.PhysicalWaveSum.commonWave_smoothAt {a : ℝ} (ha : 0 < a) (h : ℝ) (n d : ℕ) (r0 : ℝ) (c : CarrierData) {amp : LiftPoint → ℂ} (hamp : ContDiff ℝ (↑⊤) amp) (hF : ContDiff ℝ (↑⊤) c.F) (hG : ContDiff ℝ (↑⊤) c.G) (j : ℤ) {w : ProblemStatement.SpaceTime} (hw : PhysicalGraphBounds.radialProjection w ≠ 0) : ContDiffAt ℝ (↑⊤) (commonWave a h n d r0 c amp j) w

theorem NavierStokes.PhysicalWaveSum.common_carrier_physical_bound {h a b Z r0 P B eBase : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 2) (ha : 0 < a) (hZ : 0 ≤ Z) (hr0 : 0 ≤ r0) (hP : 1 ≤ P) (hB : 1 ≤ B) (heBase : 0 ≤ eBase) (Δ m : ℕ) (g eAmp A H : ℝ) (hA : 0 ≤ A) (hH : 0 ≤ H) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), 4 ≤ n → ∀ d ≤ Δ, ∀ (w : ProblemStatement.SpaceTime), (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus a b → |w.1| ≤ 1 → ‖PhysicalGraphBounds.liftZT (PhysicalGraphBounds.physicalLift h n w)‖ ≤ Z → ∀ (q : ℝ), 0 < q → q / 2 ≤ ChartScales.Q n → ChartScales.Q n ≤ 2 * q → ∀ (c : CarrierData) (amp : LiftPoint → ℂ) (j : ℤ), |c.angular| ≤ P → |c.axial| ≤ P → |c.radial| ≤ P → |PhysicalGraphBounds.etaCoordinate (PhysicalGraphBounds.nativeGraph h n w - c.center)| ≤ r0 → ContDiff ℝ (↑⊤) amp → ContDiff ℝ (↑⊤) c.F → ContDiff ℝ (↑⊤) c.G → |↑j| ≤ H → (∀ i ≤ m, ‖iteratedFDeriv ℝ i amp (commonLift h n d w)‖ ≤ A * ChartScales.Q n ^ g * ChartScales.S n ^ eAmp) → (∀ i ≤ m, ‖iteratedFDeriv ℝ i c.F (PhysicalGraphBounds.slotMap (PolarCharts.chart a c.chart) (ChartScales.timeCoefficient h n) c.center r0 (PhysicalGraphBounds.physicalLift h n w)).1‖ ≤ B * ChartScales.S n ^ eBase) → (∀ i ≤ m, ‖iteratedFDeriv ℝ i c.G (PhysicalGraphBounds.slotMap (PolarCharts.chart a c.chart) (ChartScales.timeCoefficient h n) c.center r0 (PhysicalGraphBounds.physicalLift h n w)).1‖ ≤ B * ChartScales.S n ^ eBase) → ‖iteratedFDeriv ℝ m (commonWave a h n d r0 c amp j) w‖ ≤ C * q ^ (g - PhysicalGraphBounds.waveLoss h m)

The literal native phase may multiply an arbitrary common-cover amplitude. Bounded inverse-cover changes add only the factor coverBound^m to the stripped constant.

noncomputable def NavierStokes.PhysicalWaveSum.labelRegion (D : ℝ) (L : Label) : Set (ℝ × Position)

Closed supports of the actual dyadic and slow masks.

Equations

• NavierStokes.PhysicalWaveSum.labelRegion D L = tsupport (NavierStokes.SquaredPartition.dyadicMask ↑L.1) ×ˢ tsupport (NavierStokes.SquaredPartition.physicalSlowMask D L.1 L.2.1)

theorem NavierStokes.PhysicalWaveSum.labelRegion_closed (D : ℝ) (L : Label) : IsClosed (labelRegion D L)

noncomputable def NavierStokes.PhysicalWaveSum.physicalMask (D : ℝ) (L : Label) (z : ℝ × Position) : ℝ

Physical mask, given by SquaredPartition.dyadicMask (L.1 : ℤ) z.1 * SquaredPartition.physicalSlowMask D L.1 L.2.1 z.2.

Equations

• NavierStokes.PhysicalWaveSum.physicalMask D L z = NavierStokes.SquaredPartition.dyadicMask (↑L.1) z.1 * NavierStokes.SquaredPartition.physicalSlowMask D L.1 L.2.1 z.2

theorem NavierStokes.PhysicalWaveSum.physicalMask_support_subset (D : ℝ) (L : Label) : Function.support (physicalMask D L) ⊆ labelRegion D L

theorem NavierStokes.PhysicalWaveSum.physicalMask_tsupport_subset (D : ℝ) (L : Label) : tsupport (physicalMask D L) ⊆ labelRegion D L

theorem NavierStokes.PhysicalWaveSum.labelRegion_band {D : ℝ} {L : Label} {z : ℝ × Position} (hz : z ∈ labelRegion D L) : ChartScales.Q L.1 / 2 ≤ z.1 ∧ z.1 ≤ 2 * ChartScales.Q L.1

theorem NavierStokes.PhysicalWaveSum.labelRegion_active_relation {D : ℝ} {L : Label} {z : ℝ × Position} (hz : z ∈ labelRegion D L) : z.1 / 2 ≤ ChartScales.Q L.1 ∧ ChartScales.Q L.1 ≤ 2 * z.1

theorem NavierStokes.PhysicalWaveSum.logCoordinate_in_band {q : ℝ} (hq : 0 < q) {n : ℕ} (hlo : ChartScales.Q n / 2 ≤ q) (hhi : q ≤ 2 * ChartScales.Q n) : SquaredPartition.logCoordinate q ∈ Set.Icc (↑n - 1) (↑n + 1)

theorem NavierStokes.PhysicalWaveSum.labelRegion_adjacency {D : ℝ} {L M : Label} {z : ℝ × Position} (hq : 0 < z.1) (hL : 1 ≤ L.1) (hM : 1 ≤ M.1) (hne : L ≠ M) (hzL : z ∈ labelRegion D L) (hzM : z ∈ labelRegion D M) : SlotColoring.Adj D L M

theorem NavierStokes.PhysicalWaveSum.labelRegion_color_injective {D : ℝ} {z : ℝ × Position} (hq : 0 < z.1) : Set.InjOn SlotColoring.colorData {L : Label | 1 ≤ L.1 ∧ z ∈ labelRegion D L}

theorem NavierStokes.PhysicalWaveSum.labelRegion_card_le {D : ℝ} {z : ℝ × Position} (hq : 0 < z.1) (s : Finset Label) (hs : ∀ L ∈ s, 1 ≤ L.1 ∧ z ∈ labelRegion D L) : s.card ≤ 2250

The constructed coloring bounds overlap even on closed derivative supports. In particular no generic bounded-overlap hypothesis is used.

@[reducible, inline]

abbrev NavierStokes.PhysicalWaveSum.PositiveParam : Type

Positive param: an abbreviation for Ioi (0 : ℝ) × Position.

Equations

• NavierStokes.PhysicalWaveSum.PositiveParam = (↑(Set.Ioi 0) × NavierStokes.PhysicalWaveSum.Position)

theorem NavierStokes.PhysicalWaveSum.dyadic_closed_locallyFinite : LocallyFinite fun (n : ℕ) => {q : ↑(Set.Ioi 0) | ↑q ∈ tsupport (SquaredPartition.dyadicMask ↑n)}

theorem NavierStokes.PhysicalWaveSum.labelRegion_locallyFinite (D : ℝ) : LocallyFinite fun (L : Label) => {z : PositiveParam | (↑z.1, z.2) ∈ labelRegion D L}

@[reducible, inline]

abbrev NavierStokes.PhysicalWaveSum.BandLabel : Type

Band label: an abbreviation for {L : Label // 4 ≤ L.1}.

Equations

• NavierStokes.PhysicalWaveSum.BandLabel = { L : NavierStokes.PhysicalWaveSum.Label // 4 ≤ L.1 }

@[reducible, inline]

abbrev NavierStokes.PhysicalWaveSum.Harmonic (H : ℕ) : Type

Harmonic: an abbreviation for ↥(Finset.Icc (-(H : ℤ)) (H : ℤ)).

Equations

• NavierStokes.PhysicalWaveSum.Harmonic H = ↥(Finset.Icc (-↑H) ↑H)

@[reducible, inline]

abbrev NavierStokes.PhysicalWaveSum.WaveIndex (H : ℕ) : Type

Wave index: an abbreviation for BandLabel × Harmonic H.

Equations

• NavierStokes.PhysicalWaveSum.WaveIndex H = (NavierStokes.PhysicalWaveSum.BandLabel × NavierStokes.PhysicalWaveSum.Harmonic H)

theorem NavierStokes.PhysicalWaveSum.harmonic_bound {H : ℕ} (j : Harmonic H) : |↑↑j| ≤ ↑H

theorem NavierStokes.PhysicalWaveSum.harmonic_card (H : ℕ) : Fintype.card (Harmonic H) = 2 * H + 1

noncomputable def NavierStokes.PhysicalWaveSum.waveColor {H : ℕ} (I : WaveIndex H) : SlotColoring.Palette × Harmonic H

Wave color, given by (SlotColoring.colorData I.1.val, I.2).

Equations

• NavierStokes.PhysicalWaveSum.waveColor I = (NavierStokes.SlotColoring.colorData ↑I.1, I.2)

theorem NavierStokes.PhysicalWaveSum.waveRegion_card_le {D : ℝ} {H : ℕ} {z : ℝ × Position} (hq : 0 < z.1) (s : Finset (WaveIndex H)) (hs : ∀ I ∈ s, z ∈ labelRegion D ↑I.1) : s.card ≤ 2250 * (2 * H + 1)

theorem NavierStokes.PhysicalWaveSum.waveRegion_locallyFinite (D : ℝ) (H : ℕ) : LocallyFinite fun (I : WaveIndex H) => {z : PositiveParam | (↑z.1, z.2) ∈ labelRegion D ↑I.1}

noncomputable def NavierStokes.PhysicalWaveSum.preterminal : Set ProblemStatement.SpaceTime

Preterminal, given by {w | w.1 < 1}.

Equations

• NavierStokes.PhysicalWaveSum.preterminal = {w : NavierStokes.ProblemStatement.SpaceTime | w.1 < 1}

theorem NavierStokes.PhysicalWaveSum.preterminal_open : IsOpen preterminal

noncomputable def NavierStokes.PhysicalWaveSum.physicalQ (h : ℝ) (w : ProblemStatement.SpaceTime) : ℝ

The actual similarity coordinate at a Cartesian spacetime point.

Equations

• NavierStokes.PhysicalWaveSum.physicalQ h w = NavierStokes.SimilarityProfile.q h (NavierStokes.AxisymmetricFields.profilePoint w.1 w.2)

theorem NavierStokes.PhysicalWaveSum.physicalQ_pos {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {w : ProblemStatement.SpaceTime} (hw : w ∈ preterminal) : 0 < physicalQ h w

theorem NavierStokes.PhysicalWaveSum.physicalQ_smoothAt {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {w : ProblemStatement.SpaceTime} (hw : w ∈ preterminal) : ContDiffAt ℝ (↑⊤) (physicalQ h) w

noncomputable def NavierStokes.PhysicalWaveSum.physicalPosition (w : ProblemStatement.SpaceTime) : Position

The three physical variables whose rescalings enter the slow masks.

Equations

• NavierStokes.PhysicalWaveSum.physicalPosition w = ![NavierStokes.PolarCharts.radius (NavierStokes.PhysicalGraphBounds.radialProjection w), w.2.ofLp 2, 1 - w.1]

theorem NavierStokes.PhysicalWaveSum.physicalPosition_continuous : Continuous physicalPosition

noncomputable def NavierStokes.PhysicalWaveSum.physicalParams (h : ℝ) (w : ProblemStatement.SpaceTime) : ℝ × Position

Physical params, given by (physicalQ h w, physicalPosition w).

Equations

• NavierStokes.PhysicalWaveSum.physicalParams h w = (NavierStokes.PhysicalWaveSum.physicalQ h w, NavierStokes.PhysicalWaveSum.physicalPosition w)

theorem NavierStokes.PhysicalWaveSum.physicalParams_continuousAt {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {w : ProblemStatement.SpaceTime} (hw : w ∈ preterminal) : ContinuousAt (physicalParams h) w

noncomputable def NavierStokes.PhysicalWaveSum.positiveParams {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (w : ↑preterminal) : PositiveParam

Positive params, given by (⟨physicalQ h w, physicalQ_pos hh hh1 w.property⟩, physicalPosition w).

Equations

• NavierStokes.PhysicalWaveSum.positiveParams hh hh1 w = (⟨NavierStokes.PhysicalWaveSum.physicalQ h ↑w, ⋯⟩, NavierStokes.PhysicalWaveSum.physicalPosition ↑w)

theorem NavierStokes.PhysicalWaveSum.positiveParams_continuous {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) : Continuous (positiveParams hh hh1)

theorem NavierStokes.PhysicalWaveSum.waveRegion_closed (D : ℝ) {H : ℕ} (I : WaveIndex H) : IsClosed {z : PositiveParam | (↑z.1, z.2) ∈ labelRegion D ↑I.1}

theorem NavierStokes.PhysicalWaveSum.active_neighborhood {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {V : ι → Set X} (hV : LocallyFinite V) (hc : ∀ (i : ι), IsClosed (V i)) (x : X) : ∃ (s : Finset ι), (∀ (i : ι), i ∈ s ↔ x ∈ V i) ∧ ∀ᶠ (y : X) in nhds x, ∀ (i : ι), y ∈ V i → i ∈ s

A locally finite closed family has a neighborhood with no new indices beyond the finite family active at the point.

theorem NavierStokes.PhysicalWaveSum.physical_active_neighborhood {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (H : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ preterminal) : ∃ (s : Finset (WaveIndex H)), (∀ (I : WaveIndex H), I ∈ s ↔ physicalParams h w ∈ labelRegion (CoordinateAlgebra.D h) ↑I.1) ∧ ∀ᶠ (y : ProblemStatement.SpaceTime) in nhds w, y ∈ preterminal ∧ ∀ (I : WaveIndex H), physicalParams h y ∈ labelRegion (CoordinateAlgebra.D h) ↑I.1 → I ∈ s

Local finiteness is used only on the actual positive-q domain.

theorem NavierStokes.PhysicalWaveSum.iteratedFDeriv_eq_of_eventuallyEq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f g : E → F} {x : E} (he : f =ᶠ[nhds x] g) (m : ℕ) : iteratedFDeriv ℝ m f x = iteratedFDeriv ℝ m g x

theorem NavierStokes.PhysicalWaveSum.iteratedFDeriv_finset_sum_at {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (s : Finset ι) {f : ι → E → F} {x : E} {m : ℕ} (hf : ∀ i ∈ s, ContDiffAt ℝ (↑m) (f i) x) : iteratedFDeriv ℝ m (fun (y : E) => ∑ i ∈ s, f i y) x = ∑ i ∈ s, iteratedFDeriv ℝ m (f i) x

theorem NavierStokes.PhysicalWaveSum.masked_finsum_eventually {E : Type u_1} [AddCommMonoid E] {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {H : ℕ} (f : WaveIndex H → ProblemStatement.SpaceTime → E) (hsupp : ∀ (I : WaveIndex H), ∀ y ∈ preterminal, f I y ≠ 0 → physicalParams h y ∈ labelRegion (CoordinateAlgebra.D h) ↑I.1) {w : ProblemStatement.SpaceTime} (hw : w ∈ preterminal) : ∃ (s : Finset (WaveIndex H)), (∀ (I : WaveIndex H), I ∈ s ↔ physicalParams h w ∈ labelRegion (CoordinateAlgebra.D h) ↑I.1) ∧ (fun (y : ProblemStatement.SpaceTime) => ∑ᶠ (I : WaveIndex H), f I y) =ᶠ[nhds w] fun (y : ProblemStatement.SpaceTime) => ∑ I ∈ s, f I y

A mask support hypothesis produces an actual local finite-sum identity. The summands need not have any native-torus periodicity.

theorem NavierStokes.PhysicalWaveSum.masked_finsum_smooth {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {H : ℕ} (f : WaveIndex H → ProblemStatement.SpaceTime → E) (hf : ∀ (I : WaveIndex H), ∀ w ∈ preterminal, ContDiffAt ℝ (↑⊤) (f I) w) (hsupp : ∀ (I : WaveIndex H), ∀ y ∈ preterminal, f I y ≠ 0 → physicalParams h y ∈ labelRegion (CoordinateAlgebra.D h) ↑I.1) : ContDiffOn ℝ (↑⊤) (fun (y : ProblemStatement.SpaceTime) => ∑ᶠ (I : WaveIndex H), f I y) preterminal

theorem NavierStokes.PhysicalWaveSum.masked_finsum_jet_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {H : ℕ} (f : WaveIndex H → ProblemStatement.SpaceTime → E) (hf : ∀ (I : WaveIndex H), ∀ w ∈ preterminal, ContDiffAt ℝ (↑⊤) (f I) w) (hsupp : ∀ (I : WaveIndex H), ∀ y ∈ preterminal, f I y ≠ 0 → physicalParams h y ∈ labelRegion (CoordinateAlgebra.D h) ↑I.1) {w : ProblemStatement.SpaceTime} (hw : w ∈ preterminal) (m : ℕ) {B : ℝ} (hB : 0 ≤ B) (hb : ∀ (I : WaveIndex H), physicalParams h w ∈ labelRegion (CoordinateAlgebra.D h) ↑I.1 → ‖iteratedFDeriv ℝ m (f I) w‖ ≤ B) : ‖iteratedFDeriv ℝ m (fun (y : ProblemStatement.SpaceTime) => ∑ᶠ (I : WaveIndex H), f I y) w‖ ≤ ↑(2250 * (2 * H + 1)) * B

theorem NavierStokes.PhysicalWaveSum.closed_property_on_tsupport {E : Type u_1} {X : Type u_2} {Y : Type u_3} [Zero E] [TopologicalSpace X] [TopologicalSpace Y] {f : X → E} {g : X → Y} {U : Set X} (hU : IsOpen U) {x : X} (hx : x ∈ U) (hg : ContinuousAt g x) {S : Set Y} (hS : IsClosed S) (hs : ∀ y ∈ U, f y ≠ 0 → g y ∈ S) (ht : x ∈ tsupport f) : g x ∈ S

A closed input support condition remains true on the topological support of a physical field. Only continuity at the point is needed.

theorem NavierStokes.PhysicalWaveSum.jet_zero_off_tsupport {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (m : ℕ) {x : E} (hx : x ∉ tsupport f) : iteratedFDeriv ℝ m f x = 0

noncomputable def NavierStokes.PhysicalWaveSum.CarrierData.withChart (c : CarrierData) (i : PolarCharts.Index) : CarrierData

With chart, given by {c with chart := i}.

Equations

• c.withChart i = { chart := i, center := c.center, angular := c.angular, axial := c.axial, radial := c.radial, F := c.F, G := c.G }

noncomputable def NavierStokes.PhysicalWaveSum.chooseChart (a : ℝ) (x : Plane) : PolarCharts.Index

Choose chart, choosing the witness provided by hi.

Equations

• NavierStokes.PhysicalWaveSum.chooseChart a x = if hi : ∃ (i : NavierStokes.PolarCharts.Index), x ∈ NavierStokes.PolarCharts.chartDomain a i then Classical.choose hi else 0

theorem NavierStokes.PhysicalWaveSum.chooseChart_valid {a b : ℝ} (ha : 0 < a) {x : Plane} (hx : x ∈ PhysicalGraphBounds.annulus a b) : x ∈ PolarCharts.chartDomain a (chooseChart a x)

noncomputable def NavierStokes.PhysicalWaveSum.polarCarrier (c : CarrierData) (k : ℝ) (j : ℤ) (ε : ℝ) (zt : ℝ × ℝ) (v : ℝ) (rθ : Plane) : ℂ

Polar carrier, given by PhaseCalculus.harmonic k j ε c.angular c.axial c.radial c.F c.G ((rθ.1, zt), (rθ.2, v)).

Equations

• NavierStokes.PhysicalWaveSum.polarCarrier c k j ε zt v rθ = NavierStokes.PhaseCalculus.harmonic k j ε c.angular c.axial c.radial c.F c.G ((rθ.1, zt), rθ.2, v)

@[simp]

theorem NavierStokes.PhysicalWaveSum.withChart_chart (c : CarrierData) (i : PolarCharts.Index) : (c.withChart i).chart = i

@[simp]

theorem NavierStokes.PhysicalWaveSum.withChart_center (c : CarrierData) (i : PolarCharts.Index) : (c.withChart i).center = c.center

@[simp]

theorem NavierStokes.PhysicalWaveSum.polarCarrier_withChart (c : CarrierData) (i : PolarCharts.Index) (k : ℝ) (j : ℤ) (ε : ℝ) (zt : ℝ × ℝ) (v : ℝ) : polarCarrier (c.withChart i) k j ε zt v = polarCarrier c k j ε zt v

theorem NavierStokes.PhysicalWaveSum.polarCarrier_periodic (c : CarrierData) (k : ℝ) (j : ℤ) (ε : ℝ) (zt : ℝ × ℝ) (v : ℝ) (m : ℤ) (hkp : k * c.angular = ↑m) (r : ℝ) : Function.Periodic (fun (θ : ℝ) => polarCarrier c k j ε zt v (r, θ)) (2 * Real.pi)

theorem NavierStokes.PhysicalWaveSum.commonWave_polar (a h : ℝ) (n d : ℕ) (r0 : ℝ) (c : CarrierData) (amp : LiftPoint → ℂ) (j : ℤ) (w : ProblemStatement.SpaceTime) : commonWave a h n d r0 c amp j w = amp (commonLift h n d w) * polarCarrier c (↑(ChartScales.carrier h n)) j (ChartScales.epsilon h n) (PhysicalGraphBounds.liftZT (PhysicalGraphBounds.physicalLift h n w)) (PhysicalGraphBounds.slotTime h n c.center r0 w) (PolarCharts.chart a c.chart ((PhysicalGraphBounds.scaledRadial n) w))

theorem NavierStokes.PhysicalWaveSum.commonWave_charts_agree {a : ℝ} (ha : 0 < a) (h : ℝ) (n d : ℕ) (r0 : ℝ) (c : CarrierData) (amp : LiftPoint → ℂ) (j : ℤ) (w : ProblemStatement.SpaceTime) (m : ℤ) (hkp : ↑(ChartScales.carrier h n) * c.angular = ↑m) (i k : PolarCharts.Index) (hi : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a i) (hk : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a k) : commonWave a h n d r0 (c.withChart i) amp j w = commonWave a h n d r0 (c.withChart k) amp j w

noncomputable def NavierStokes.PhysicalWaveSum.globalWave (a h : ℝ) (n d : ℕ) (r0 : ℝ) (c : CarrierData) (amp : LiftPoint → ℂ) (j : ℤ) (w : ProblemStatement.SpaceTime) : ℂ

A genuine angular carrier: valid polar charts are selected pointwise; the integer angular mode will prove that the selection is smooth.

Equations

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

theorem NavierStokes.PhysicalWaveSum.globalWave_eq_zero {a h r0 : ℝ} {n d : ℕ} {c : CarrierData} {amp : LiftPoint → ℂ} {j : ℤ} {w : ProblemStatement.SpaceTime} (hz : amp (commonLift h n d w) = 0) : globalWave a h n d r0 c amp j w = 0

theorem NavierStokes.PhysicalWaveSum.globalWave_eventually_common {a b h r0 : ℝ} (ha : 0 < a) (n d : ℕ) (c : CarrierData) (amp : LiftPoint → ℂ) (j m : ℤ) (hkp : ↑(ChartScales.carrier h n) * c.angular = ↑m) (hs : ∀ (y : ProblemStatement.SpaceTime), amp (commonLift h n d y) ≠ 0 → (PhysicalGraphBounds.scaledRadial n) y ∈ PhysicalGraphBounds.annulus a b) {w : ProblemStatement.SpaceTime} (i : PolarCharts.Index) (hi : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a i) : globalWave a h n d r0 c amp j =ᶠ[nhds w] commonWave a h n d r0 (c.withChart i) amp j

theorem NavierStokes.PhysicalWaveSum.globalWave_eventually_zero_off_annulus {a b h r0 : ℝ} {n d : ℕ} (c : CarrierData) (amp : LiftPoint → ℂ) (j : ℤ) (hs : ∀ (y : ProblemStatement.SpaceTime), amp (commonLift h n d y) ≠ 0 → (PhysicalGraphBounds.scaledRadial n) y ∈ PhysicalGraphBounds.annulus a b) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∉ PhysicalGraphBounds.annulus a b) : globalWave a h n d r0 c amp j =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.PhysicalWaveSum.globalWave_smooth {a b h r0 : ℝ} (ha : 0 < a) (n d : ℕ) (c : CarrierData) (amp : LiftPoint → ℂ) (j m : ℤ) (hkp : ↑(ChartScales.carrier h n) * c.angular = ↑m) (hamp : ContDiff ℝ (↑⊤) amp) (hF : ContDiff ℝ (↑⊤) c.F) (hG : ContDiff ℝ (↑⊤) c.G) (hs : ∀ (y : ProblemStatement.SpaceTime), amp (commonLift h n d y) ≠ 0 → (PhysicalGraphBounds.scaledRadial n) y ∈ PhysicalGraphBounds.annulus a b) : ContDiff ℝ (↑⊤) (globalWave a h n d r0 c amp j)

theorem NavierStokes.PhysicalWaveSum.globalWave_ne_zero_amp {a h r0 : ℝ} {n d : ℕ} {c : CarrierData} {amp : LiftPoint → ℂ} {j : ℤ} {w : ProblemStatement.SpaceTime} (hw : globalWave a h n d r0 c amp j w ≠ 0) : amp (commonLift h n d w) ≠ 0

theorem NavierStokes.PhysicalWaveSum.physicalSlowPair_eq (h : ℝ) (n : ℕ) (w : ProblemStatement.SpaceTime) : PhysicalGraphBounds.liftZT (PhysicalGraphBounds.physicalLift h n w) = (ChartScales.Q n ^ (-CoordinateAlgebra.D h) * w.2.ofLp 2, (1 - w.1) / ChartScales.Q n)

theorem NavierStokes.PhysicalWaveSum.physicalSlowPair_continuous (h : ℝ) (n : ℕ) : Continuous fun (w : ProblemStatement.SpaceTime) => PhysicalGraphBounds.liftZT (PhysicalGraphBounds.physicalLift h n w)

theorem NavierStokes.PhysicalWaveSum.nativeSlotCoordinate_eq (h : ℝ) (n : ℕ) (center : Plane) (w : ProblemStatement.SpaceTime) : PhysicalGraphBounds.etaCoordinate (PhysicalGraphBounds.nativeGraph h n w - center) = ChartScales.Tg ^ ChartScales.nativeIndex h n * w.1 - PhysicalGraphBounds.etaCoordinate center

theorem NavierStokes.PhysicalWaveSum.nativeSlotCoordinate_continuous (h : ℝ) (n : ℕ) (center : Plane) : Continuous fun (w : ProblemStatement.SpaceTime) => PhysicalGraphBounds.etaCoordinate (PhysicalGraphBounds.nativeGraph h n w - center)

theorem NavierStokes.PhysicalWaveSum.globalWave_tsupport_geometry {a b h r0 Z : ℝ} {n d : ℕ} (c : CarrierData) (amp : LiftPoint → ℂ) (j : ℤ) (hs : ∀ (y : ProblemStatement.SpaceTime), amp (commonLift h n d y) ≠ 0 → (PhysicalGraphBounds.scaledRadial n) y ∈ PhysicalGraphBounds.annulus a b ∧ ‖PhysicalGraphBounds.liftZT (PhysicalGraphBounds.physicalLift h n y)‖ ≤ Z ∧ |PhysicalGraphBounds.etaCoordinate (PhysicalGraphBounds.nativeGraph h n y - c.center)| ≤ r0) {w : ProblemStatement.SpaceTime} (hw : w ∈ tsupport (globalWave a h n d r0 c amp j)) : (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus a b ∧ ‖PhysicalGraphBounds.liftZT (PhysicalGraphBounds.physicalLift h n w)‖ ≤ Z ∧ |PhysicalGraphBounds.etaCoordinate (PhysicalGraphBounds.nativeGraph h n w - c.center)| ≤ r0

structure NavierStokes.PhysicalWaveSum.WaveFamily (H : ℕ) : Type

Wave family data, collecting gap, carrier, amplitude.

• gap : BandLabel → ℕ

  Gap of WaveFamily, of type BandLabel → ℕ.

• carrier : BandLabel → CarrierData

  Carrier of WaveFamily, of type BandLabel → CarrierData.

• amplitude : WaveIndex H → LiftPoint → ℂ

  Amplitude of WaveFamily, of type WaveIndex H → LiftPoint → ℂ.

noncomputable def NavierStokes.PhysicalWaveSum.WaveFamily.term {H : ℕ} (f : WaveFamily H) (a h r0 : ℝ) (I : WaveIndex H) : ProblemStatement.SpaceTime → ℂ

Term, given by globalWave a h I.1.val.1 (f.gap I.1) r0 (f.carrier I.1) (f.amplitude I) I.2.val.

Equations

• f.term a h r0 I = NavierStokes.PhysicalWaveSum.globalWave a h (↑I.1).1 (f.gap I.1) r0 (f.carrier I.1) (f.amplitude I) ↑I.2

noncomputable def NavierStokes.PhysicalWaveSum.WaveFamily.sum {H : ℕ} (f : WaveFamily H) (a h r0 : ℝ) (w : ProblemStatement.SpaceTime) : ℂ

Sum, given by ∑ᶠ I : WaveIndex H, f.term a h r0 I w.

Equations

• f.sum a h r0 w = ∑ᶠ (I : NavierStokes.PhysicalWaveSum.WaveIndex H), f.term a h r0 I w

structure NavierStokes.PhysicalWaveSum.RegularFamily {H : ℕ} (f : WaveFamily H) (a b h r0 Z : ℝ) (Δ : ℕ) : Prop

Smooth coefficients, the genuine angular integrality condition, and input amplitude supports. No output derivative estimate is assumed.

• gap_le (L : BandLabel) : f.gap L ≤ Δ
• gap_native (L : BandLabel) : f.gap L ≤ ChartScales.nativeIndex h (↑L).1
• amplitude_smooth (I : WaveIndex H) : ContDiff ℝ (↑⊤) (f.amplitude I)
• F_smooth (L : BandLabel) : ContDiff ℝ (↑⊤) (f.carrier L).F
• G_smooth (L : BandLabel) : ContDiff ℝ (↑⊤) (f.carrier L).G
• angular_integer (L : BandLabel) : ∃ (m : ℤ), ↑(ChartScales.carrier h (↑L).1) * (f.carrier L).angular = ↑m
• geometry_support (I : WaveIndex H) (y : ProblemStatement.SpaceTime) : f.amplitude I (commonLift h (↑I.1).1 (f.gap I.1) y) ≠ 0 → (PhysicalGraphBounds.scaledRadial (↑I.1).1) y ∈ PhysicalGraphBounds.annulus a b ∧ ‖PhysicalGraphBounds.liftZT (PhysicalGraphBounds.physicalLift h (↑I.1).1 y)‖ ≤ Z ∧ |PhysicalGraphBounds.etaCoordinate (PhysicalGraphBounds.nativeGraph h (↑I.1).1 y - (f.carrier I.1).center)| ≤ r0
• mask_support (I : WaveIndex H) (y : ProblemStatement.SpaceTime) : y ∈ preterminal → f.amplitude I (commonLift h (↑I.1).1 (f.gap I.1) y) ≠ 0 → physicalMask (CoordinateAlgebra.D h) (↑I.1) (physicalParams h y) ≠ 0

theorem NavierStokes.PhysicalWaveSum.RegularFamily.commonLift_formula {H : ℕ} {f : WaveFamily H} {a b h r0 Z : ℝ} {Δ : ℕ} (hf : RegularFamily f a b h r0 Z Δ) (L : BandLabel) (w : ProblemStatement.SpaceTime) : commonLift h (↑L).1 (f.gap L) w = (PhysicalGraphBounds.physicalChart h (↑L).1 w, (SlotGeometry.cover ^ (ChartScales.nativeIndex h (↑L).1 - f.gap L)) (PhysicalGraphBounds.radialProfile (ChartScales.radialExponent h) (PhysicalGraphBounds.radialProjection w) + w.1 • PhysicalGraphBounds.timeDirection))

theorem NavierStokes.PhysicalWaveSum.RegularFamily.term_smooth {H : ℕ} {f : WaveFamily H} {a b h r0 Z : ℝ} {Δ : ℕ} (hf : RegularFamily f a b h r0 Z Δ) (ha : 0 < a) (I : WaveIndex H) : ContDiff ℝ (↑⊤) (f.term a h r0 I)

theorem NavierStokes.PhysicalWaveSum.RegularFamily.term_support {H : ℕ} {f : WaveFamily H} {a b h r0 Z : ℝ} {Δ : ℕ} (hf : RegularFamily f a b h r0 Z Δ) (I : WaveIndex H) (w : ProblemStatement.SpaceTime) (hw : w ∈ preterminal) (hn : f.term a h r0 I w ≠ 0) : physicalParams h w ∈ labelRegion (CoordinateAlgebra.D h) ↑I.1

theorem NavierStokes.PhysicalWaveSum.RegularFamily.sum_smooth {H : ℕ} {f : WaveFamily H} {a b h r0 Z : ℝ} {Δ : ℕ} (hf : RegularFamily f a b h r0 Z Δ) (ha : 0 < a) (hh : 0 < h) (hh1 : h < 1 / 2) : ContDiffOn ℝ (↑⊤) (f.sum a h r0) preterminal

structure NavierStokes.PhysicalWaveSum.StrippedClass {H : ℕ} (f : WaveFamily H) (a b h r0 P A B g eAmp eBase : ℝ) (m : ℕ) : Prop

Bounds on genuine input coefficient jets in common coordinates, and on the genuine base profiles entering the native phase.

• parameters (L : BandLabel) : |(f.carrier L).angular| ≤ P ∧ |(f.carrier L).axial| ≤ P ∧ |(f.carrier L).radial| ≤ P
• amplitude (I : WaveIndex H) (w : ProblemStatement.SpaceTime) : w ∈ preterminal → physicalParams h w ∈ labelRegion (CoordinateAlgebra.D h) ↑I.1 → (PhysicalGraphBounds.scaledRadial (↑I.1).1) w ∈ PhysicalGraphBounds.annulus a b → ∀ i ≤ m, ‖iteratedFDeriv ℝ i (f.amplitude I) (commonLift h (↑I.1).1 (f.gap I.1) w)‖ ≤ A * ChartScales.Q (↑I.1).1 ^ g * ChartScales.S (↑I.1).1 ^ eAmp
• base_F (I : WaveIndex H) (w : ProblemStatement.SpaceTime) : w ∈ preterminal → physicalParams h w ∈ labelRegion (CoordinateAlgebra.D h) ↑I.1 → (PhysicalGraphBounds.scaledRadial (↑I.1).1) w ∈ PhysicalGraphBounds.annulus a b → ∀ (chart : PolarCharts.Index), (PhysicalGraphBounds.scaledRadial (↑I.1).1) w ∈ PolarCharts.chartDomain a chart → ∀ i ≤ m, ‖iteratedFDeriv ℝ i (f.carrier I.1).F (PhysicalGraphBounds.slotMap (PolarCharts.chart a chart) (ChartScales.timeCoefficient h (↑I.1).1) (f.carrier I.1).center r0 (PhysicalGraphBounds.physicalLift h (↑I.1).1 w)).1‖ ≤ B * ChartScales.S (↑I.1).1 ^ eBase
• base_G (I : WaveIndex H) (w : ProblemStatement.SpaceTime) : w ∈ preterminal → physicalParams h w ∈ labelRegion (CoordinateAlgebra.D h) ↑I.1 → (PhysicalGraphBounds.scaledRadial (↑I.1).1) w ∈ PhysicalGraphBounds.annulus a b → ∀ (chart : PolarCharts.Index), (PhysicalGraphBounds.scaledRadial (↑I.1).1) w ∈ PolarCharts.chartDomain a chart → ∀ i ≤ m, ‖iteratedFDeriv ℝ i (f.carrier I.1).G (PhysicalGraphBounds.slotMap (PolarCharts.chart a chart) (ChartScales.timeCoefficient h (↑I.1).1) (f.carrier I.1).center r0 (PhysicalGraphBounds.physicalLift h (↑I.1).1 w)).1‖ ≤ B * ChartScales.S (↑I.1).1 ^ eBase

theorem NavierStokes.PhysicalWaveSum.physical_sum_jet_bound {h a b Z r0 P B eBase : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hZ : 0 ≤ Z) (hr0 : 0 ≤ r0) (hP : 1 ≤ P) (hB : 1 ≤ B) (heBase : 0 ≤ eBase) (H Δ m : ℕ) (g eAmp A : ℝ) (hA : 0 ≤ A) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (f : WaveFamily H), RegularFamily f a b h r0 Z Δ → StrippedClass f a b h r0 P A B g eAmp eBase m → ∀ w ∈ preterminal, |w.1| ≤ 1 → ‖iteratedFDeriv ℝ m (f.sum a h r0) w‖ ≤ C * physicalQ h w ^ (g - PhysicalGraphBounds.waveLoss h m)

The full physical sum has exactly the same power loss as one native carrier. The number of harmonics, bounded cover gap, overlap count, and stripped-class degrees affect its constant only.

noncomputable def NavierStokes.PhysicalWaveSum.coverChange (d e : ℕ) : LiftPoint →L[ℝ] LiftPoint

Cover change, given by (downLift e).comp (upLift d).

Equations

• NavierStokes.PhysicalWaveSum.coverChange d e = NavierStokes.PhysicalWaveSum.downLift e ∘SL NavierStokes.PhysicalWaveSum.upLift d

theorem NavierStokes.PhysicalWaveSum.coverChange_common (h : ℝ) (n d e : ℕ) (w : ProblemStatement.SpaceTime) : (coverChange d e) (commonLift h n d w) = commonLift h n e w

theorem NavierStokes.PhysicalWaveSum.norm_coverChange_le {d e Δ : ℕ} (hd : d ≤ Δ) (he : e ≤ Δ) : ‖coverChange d e‖ ≤ coverBound Δ ^ 2

theorem NavierStokes.PhysicalWaveSum.commonWave_reexpress (a h : ℝ) (n d e : ℕ) (r0 : ℝ) (c : CarrierData) (amp : LiftPoint → ℂ) (j : ℤ) (w : ProblemStatement.SpaceTime) : commonWave a h n d r0 c (amp ∘ ⇑(coverChange d e)) j w = commonWave a h n e r0 c amp j w

Re-expressing a source by the true linear cover change preserves its physical wave exactly. This does not require finer native periodicity.

theorem NavierStokes.PhysicalWaveSum.globalWave_reexpress (a h : ℝ) (n d e : ℕ) (r0 : ℝ) (c : CarrierData) (amp : LiftPoint → ℂ) (j : ℤ) (w : ProblemStatement.SpaceTime) : globalWave a h n d r0 c (amp ∘ ⇑(coverChange d e)) j w = globalWave a h n e r0 c amp j w

theorem NavierStokes.PhysicalWaveSum.RegularFamily.sum_locally_finite {H : ℕ} {f : WaveFamily H} {a b h r0 Z : ℝ} {Δ : ℕ} (hf : RegularFamily f a b h r0 Z Δ) (hh : 0 < h) (hh1 : h < 1 / 2) {w : ProblemStatement.SpaceTime} (hw : w ∈ preterminal) : ∃ (s : Finset (WaveIndex H)), s.card ≤ 2250 * (2 * H + 1) ∧ f.sum a h r0 =ᶠ[nhds w] fun (y : ProblemStatement.SpaceTime) => ∑ I ∈ s, f.term a h r0 I y

theorem NavierStokes.PhysicalWaveSum.mask_support_of_factorization {D h : ℝ} {L : Label} {n d : ℕ} {amp : LiftPoint → ℂ} {rest : ProblemStatement.SpaceTime → ℂ} (he : ∀ (w : ProblemStatement.SpaceTime), amp (commonLift h n d w) = ↑(physicalMask D L (physicalParams h w)) * rest w) (w : ProblemStatement.SpaceTime) (hw : amp (commonLift h n d w) ≠ 0) : physicalMask D L (physicalParams h w) ≠ 0

Factoring in the actual constructed mask proves the support input used by RegularFamily; no separate support assertion about the sum is needed.

noncomputable def NavierStokes.PhysicalWaveSum.realCoordinate (i : Fin 3) : ℂ →L[ℝ] ProblemStatement.Space

Real coordinate, given by Complex.reCLM.smulRight (coordinateVector i).

Equations

• NavierStokes.PhysicalWaveSum.realCoordinate i = Complex.reCLM.smulRight (NavierStokes.ProblemStatement.coordinateVector i)

@[simp]

theorem NavierStokes.PhysicalWaveSum.realCoordinate_apply (i : Fin 3) (z : ℂ) : (realCoordinate i) z = z.re • ProblemStatement.coordinateVector i

theorem NavierStokes.PhysicalWaveSum.norm_realCoordinate_le (i : Fin 3) : ‖realCoordinate i‖ ≤ 1

noncomputable def NavierStokes.PhysicalWaveSum.vectorSum {H : ℕ} (f : Fin 3 → WaveFamily H) (a h r0 : ℝ) (w : ProblemStatement.SpaceTime) : ProblemStatement.Space

Real Euclidean vector assembled from the three scalar carrier sums.

Equations

• NavierStokes.PhysicalWaveSum.vectorSum f a h r0 w = ∑ i : Fin 3, (NavierStokes.PhysicalWaveSum.realCoordinate i) ((f i).sum a h r0 w)

theorem NavierStokes.PhysicalWaveSum.vectorSum_smooth {H : ℕ} {f : Fin 3 → WaveFamily H} {a b h r0 Z : ℝ} {Δ : ℕ} (hf : ∀ (i : Fin 3), RegularFamily (f i) a b h r0 Z Δ) (ha : 0 < a) (hh : 0 < h) (hh1 : h < 1 / 2) : ContDiffOn ℝ (↑⊤) (vectorSum f a h r0) preterminal

theorem NavierStokes.PhysicalWaveSum.norm_jet_linear_comp_at {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : E → F} {w : E} {m : ℕ} (hf : ContDiffAt ℝ (↑m) f w) (L : F →L[ℝ] G) : ‖iteratedFDeriv ℝ m (⇑L ∘ f) w‖ ≤ ‖L‖ * ‖iteratedFDeriv ℝ m f w‖

theorem NavierStokes.PhysicalWaveSum.vectorSum_jet_bound {H : ℕ} {f : Fin 3 → WaveFamily H} {a b h r0 Z : ℝ} {Δ : ℕ} (hf : ∀ (i : Fin 3), RegularFamily (f i) a b h r0 Z Δ) (ha : 0 < a) (hh : 0 < h) (hh1 : h < 1 / 2) {w : ProblemStatement.SpaceTime} (hw : w ∈ preterminal) (m : ℕ) {B : ℝ} (hb : ∀ (i : Fin 3), ‖iteratedFDeriv ℝ m ((f i).sum a h r0) w‖ ≤ B) : ‖iteratedFDeriv ℝ m (vectorSum f a h r0) w‖ ≤ 3 * B

theorem NavierStokes.PhysicalWaveSum.physical_vector_sum_jet_bound {h a b Z r0 P B eBase : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hZ : 0 ≤ Z) (hr0 : 0 ≤ r0) (hP : 1 ≤ P) (hB : 1 ≤ B) (heBase : 0 ≤ eBase) (H Δ m : ℕ) (g eAmp A : ℝ) (hA : 0 ≤ A) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (f : Fin 3 → WaveFamily H), (∀ (i : Fin 3), RegularFamily (f i) a b h r0 Z Δ) → (∀ (i : Fin 3), StrippedClass (f i) a b h r0 P A B g eAmp eBase m) → ∀ w ∈ preterminal, |w.1| ≤ 1 → ‖iteratedFDeriv ℝ m (vectorSum f a h r0) w‖ ≤ C * physicalQ h w ^ (g - PhysicalGraphBounds.waveLoss h m)

The same stage-independent loss for an actual real Cartesian vector field. Passing from scalar components costs only a factor of three.