A common shrinking support for actual physical increments #
Native outer radii, bounded by one fixed patch radius, give one physical outer-support constant for every stage. Coherent means are represented in a comparable native band; no physical support property is an input. The zeroth support assertion concerns the finite initialization increment.
theorem
NavierStokes.PhysicalStageSupport.support_mono
{V : Type u_1}
[NormedAddCommGroup V]
{h C D qbig : ℝ}
{f : ProblemStatement.SpaceTime → V}
(hf : MixedDiagonalExtensions.SublevelShrinkingSupport h C qbig f)
(hCD : C ≤ D)
:
theorem
NavierStokes.PhysicalStageSupport.support_congr
{V : Type u_1}
[NormedAddCommGroup V]
{h C qbig : ℝ}
{f g : ProblemStatement.SpaceTime → V}
(hf : MixedDiagonalExtensions.SublevelShrinkingSupport h C qbig f)
(he : Set.EqOn f g (CutStageEstimates.physicalSublevel h qbig))
:
theorem
NavierStokes.PhysicalStageSupport.support_map_zero
{V : Type u_1}
[NormedAddCommGroup V]
{E : Type u_2}
[NormedAddCommGroup E]
{h C qbig : ℝ}
{f : ProblemStatement.SpaceTime → V}
(hf : MixedDiagonalExtensions.SublevelShrinkingSupport h C qbig f)
(T : ProblemStatement.SpaceTime → V → E)
(hT : ∀ (w : ProblemStatement.SpaceTime), T w 0 = 0)
:
MixedDiagonalExtensions.SublevelShrinkingSupport h C qbig fun (w : ProblemStatement.SpaceTime) => T w (f w)
theorem
NavierStokes.PhysicalStageSupport.support_add
{V : Type u_1}
[NormedAddCommGroup V]
{h C qbig : ℝ}
{f g : ProblemStatement.SpaceTime → V}
(hf : MixedDiagonalExtensions.SublevelShrinkingSupport h C qbig f)
(hg : MixedDiagonalExtensions.SublevelShrinkingSupport h C qbig g)
:
MixedDiagonalExtensions.SublevelShrinkingSupport h C qbig fun (w : ProblemStatement.SpaceTime) => f w + g w
theorem
NavierStokes.PhysicalStageSupport.support_finset_sum
{V : Type u_1}
[NormedAddCommGroup V]
{ι : Type u_2}
{h C qbig : ℝ}
{f : ι → ProblemStatement.SpaceTime → V}
(s : Finset ι)
(hf : ∀ i ∈ s, MixedDiagonalExtensions.SublevelShrinkingSupport h C qbig (f i))
:
MixedDiagonalExtensions.SublevelShrinkingSupport h C qbig fun (w : ProblemStatement.SpaceTime) => ∑ i ∈ s, f i w
This constant is shared by the entire stage sequence.
Equations
Instances For
theorem
NavierStokes.PhysicalStageSupport.wave_scalar_support
{h : ℝ}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{I : Type u_1}
{K : Type u_2}
{J : Type u_3}
(W : PhysicalStageBounds.WaveData h D I K J)
(i : J)
{qbig R : ℝ}
(hR : W.upperRadius ≤ 2 * R)
:
MixedDiagonalExtensions.SublevelShrinkingSupport h (outerConstant R) qbig (W.scalar i)
theorem
NavierStokes.PhysicalStageSupport.wave_vector_support
{h : ℝ}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{I : Type u_1}
{K : Type u_2}
(W : PhysicalStageBounds.WaveData h D I K (Fin 3))
{qbig R : ℝ}
(hR : W.upperRadius ≤ 2 * R)
:
theorem
NavierStokes.PhysicalStageSupport.wave_pressure_support
{h : ℝ}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{I : Type u_1}
{K : Type u_2}
(W : PhysicalStageBounds.WaveData h D I K Unit)
{qbig R : ℝ}
(hR : W.upperRadius ≤ 2 * R)
:
theorem
NavierStokes.PhysicalStageSupport.mean_field_support
{h degree : ℝ}
(M : PhysicalStageBounds.MeanData h degree)
(hh : 0 < h)
(hh1 : h < 1 / 2)
{qbig R : ℝ}
(hq : qbig ≤ ChartScales.Q M.firstBand)
(hR : M.upperRadius ≤ R)
:
Exact coherence and the native moving annulus supply the physical support for the same scalar field on the common valid sublevel.
theorem
NavierStokes.PhysicalStageSupport.mean_angular_support
{h degree : ℝ}
(M : PhysicalStageBounds.MeanData h degree)
(hh : 0 < h)
(hh1 : h < 1 / 2)
{qbig R : ℝ}
(hq : qbig ≤ ChartScales.Q M.firstBand)
(hR : M.upperRadius ≤ R)
:
The Cartesian angular reconstruction is pointwise zero-preserving.
theorem
NavierStokes.PhysicalStageSupport.comparable_graph_mem
{h : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
(n d : ℕ)
{w : ProblemStatement.SpaceTime}
(ht : w.1 < 1)
(hlo : PhysicalWaveSum.physicalQ h w ≤ ChartScales.Q n)
(hhi : ChartScales.Q n < 2 * PhysicalWaveSum.physicalQ h w)
:
(PhysicalMeanJetBounds.graph h n d w).2.1 ∈ PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2
The selected comparable band lies in the actual open normalized
window (1/2,2). No enlargement of the native mean domain is required.
theorem
NavierStokes.PhysicalStageSupport.coherent_field_support
{h degree : ℝ}
{N gap : ℕ}
{U : Set PhysicalGraphBounds.Plane}
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(D : PhysicalMeanJetBounds.CoherentFamily h degree N gap U E)
(hh : 0 < h)
(hh1 : h < 1 / 2)
{a b qbig R : ℝ}
(ha : 0 < a)
(hab : a < b)
(hU : IsOpen U)
(hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U)
(hs : PhysicalMeanJetBounds.NativeSupport h a b N U D.native)
(hq : qbig ≤ ChartScales.Q N)
(hR : b ≤ R)
:
theorem
NavierStokes.PhysicalStageSupport.coherent_angular_support
{h degree : ℝ}
{N gap : ℕ}
{U : Set PhysicalGraphBounds.Plane}
(D : PhysicalMeanJetBounds.CoherentFamily h degree N gap U ℝ)
(hh : 0 < h)
(hh1 : h < 1 / 2)
{a b qbig R : ℝ}
(ha : 0 < a)
(hab : a < b)
(hU : IsOpen U)
(hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U)
(hs : PhysicalMeanJetBounds.NativeSupport h a b N U D.native)
(hq : qbig ≤ ChartScales.Q N)
(hR : b ≤ R)
:
theorem
NavierStokes.PhysicalStageSupport.potentialIncrement_support
{h : ℝ}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{I : Type u_1}
{K : Type u_2}
(W : PhysicalStageBounds.WaveData h D I K (Fin 3))
(M : PhysicalStageBounds.MeanData h (CoordinateAlgebra.A h - 1 / 2))
(hh : 0 < h)
(hh1 : h < 1 / 2)
{qbig R : ℝ}
(hq : qbig ≤ ChartScales.Q M.firstBand)
(hW : W.upperRadius ≤ 2 * R)
(hM : M.upperRadius ≤ R)
:
theorem
NavierStokes.PhysicalStageSupport.pressureIncrement_support
{h : ℝ}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{I : Type u_1}
{K : Type u_2}
(W : PhysicalStageBounds.WaveData h D I K Unit)
(M : PhysicalStageBounds.MeanData h (2 * CoordinateAlgebra.A h))
(hh : 0 < h)
(hh1 : h < 1 / 2)
{qbig R : ℝ}
(hq : qbig ≤ ChartScales.Q M.firstBand)
(hW : W.upperRadius ≤ 2 * R)
(hM : M.upperRadius ≤ R)
:
structure
NavierStokes.PhysicalStageSupport.NativeOuterBounds
{h : ℝ}
{DA DP : Type}
[NormedAddCommGroup DA]
[NormedSpace ℝ DA]
[NormedAddCommGroup DP]
[NormedSpace ℝ DP]
{IA : Type u_1}
{KA : Type u_2}
{IP : Type u_3}
{KP : Type u_4}
(R : ℝ)
(WA : ℕ → PhysicalStageBounds.WaveData h DA IA KA (Fin 3))
(MA : ℕ → PhysicalStageBounds.MeanData h (CoordinateAlgebra.A h - 1 / 2))
(MB : ℕ → PhysicalStageBounds.MeanData h (CoordinateAlgebra.A h))
(WP : ℕ → PhysicalStageBounds.WaveData h DP IP KP Unit)
(MP : ℕ → PhysicalStageBounds.MeanData h (2 * CoordinateAlgebra.A h))
:
Numeric bounds on the native radial endpoints. The same R occurs
at every stage, including stage zero.
Instances For
theorem
NavierStokes.PhysicalStageSupport.NativeOuterBounds.radius_pos
{h : ℝ}
{DA DP : Type}
[NormedAddCommGroup DA]
[NormedSpace ℝ DA]
[NormedAddCommGroup DP]
[NormedSpace ℝ DP]
{IA : Type u_1}
{KA : Type u_2}
{IP : Type u_3}
{KP : Type u_4}
(WA : ℕ → PhysicalStageBounds.WaveData h DA IA KA (Fin 3))
(MA : ℕ → PhysicalStageBounds.MeanData h (CoordinateAlgebra.A h - 1 / 2))
(MB : ℕ → PhysicalStageBounds.MeanData h (CoordinateAlgebra.A h))
(WP : ℕ → PhysicalStageBounds.WaveData h DP IP KP Unit)
(MP : ℕ → PhysicalStageBounds.MeanData h (2 * CoordinateAlgebra.A h))
{R : ℝ}
(H : NativeOuterBounds R WA MA MB WP MP)
:
theorem
NavierStokes.PhysicalStageSupport.all_increment_support
{h : ℝ}
{DA DP : Type}
[NormedAddCommGroup DA]
[NormedSpace ℝ DA]
[NormedAddCommGroup DP]
[NormedSpace ℝ DP]
{IA : Type u_1}
{KA : Type u_2}
{IP : Type u_3}
{KP : Type u_4}
(WA : ℕ → PhysicalStageBounds.WaveData h DA IA KA (Fin 3))
(MA : ℕ → PhysicalStageBounds.MeanData h (CoordinateAlgebra.A h - 1 / 2))
(MB : ℕ → PhysicalStageBounds.MeanData h (CoordinateAlgebra.A h))
(WP : ℕ → PhysicalStageBounds.WaveData h DP IP KP Unit)
(MP : ℕ → PhysicalStageBounds.MeanData h (2 * CoordinateAlgebra.A h))
(hh : 0 < h)
(hh1 : h < 1 / 2)
{qbig R : ℝ}
(hqA : ∀ (j : ℕ), qbig ≤ ChartScales.Q (MA j).firstBand)
(hqB : ∀ (j : ℕ), qbig ≤ ChartScales.Q (MB j).firstBand)
(hqP : ∀ (j : ℕ), qbig ≤ ChartScales.Q (MP j).firstBand)
(H : NativeOuterBounds R WA MA MB WP MP)
:
(∀ (j : ℕ),
MixedDiagonalExtensions.SublevelShrinkingSupport h (outerConstant R) qbig
(PhysicalStageBounds.potentialIncrement (WA j) (MA j))) ∧ (∀ (j : ℕ),
MixedDiagonalExtensions.SublevelShrinkingSupport h (outerConstant R) qbig
(PhysicalStageBounds.directStages MB j)) ∧ ∀ (j : ℕ),
MixedDiagonalExtensions.SublevelShrinkingSupport h (outerConstant R) qbig
(PhysicalStageBounds.pressureIncrement (WP j) (MP j))
All three increment families share this explicit constant, independently of stage-dependent harmonics, native bands, cover gaps, and jet constants.
theorem
NavierStokes.PhysicalStageSupport.exists_common_support
{h : ℝ}
{DA DP : Type}
[NormedAddCommGroup DA]
[NormedSpace ℝ DA]
[NormedAddCommGroup DP]
[NormedSpace ℝ DP]
{IA : Type u_1}
{KA : Type u_2}
{IP : Type u_3}
{KP : Type u_4}
(WA : ℕ → PhysicalStageBounds.WaveData h DA IA KA (Fin 3))
(MA : ℕ → PhysicalStageBounds.MeanData h (CoordinateAlgebra.A h - 1 / 2))
(MB : ℕ → PhysicalStageBounds.MeanData h (CoordinateAlgebra.A h))
(WP : ℕ → PhysicalStageBounds.WaveData h DP IP KP Unit)
(MP : ℕ → PhysicalStageBounds.MeanData h (2 * CoordinateAlgebra.A h))
(hh : 0 < h)
(hh1 : h < 1 / 2)
{qbig R : ℝ}
(hqA : ∀ (j : ℕ), qbig ≤ ChartScales.Q (MA j).firstBand)
(hqB : ∀ (j : ℕ), qbig ≤ ChartScales.Q (MB j).firstBand)
(hqP : ∀ (j : ℕ), qbig ≤ ChartScales.Q (MP j).firstBand)
(H : NativeOuterBounds R WA MA MB WP MP)
:
∃ (C : ℝ),
0 < C ∧ (∀ (j : ℕ),
MixedDiagonalExtensions.SublevelShrinkingSupport h C qbig
(PhysicalStageBounds.potentialIncrement (WA j) (MA j))) ∧ (∀ (j : ℕ), MixedDiagonalExtensions.SublevelShrinkingSupport h C qbig (PhysicalStageBounds.directStages MB j)) ∧ ∀ (j : ℕ),
MixedDiagonalExtensions.SublevelShrinkingSupport h C qbig
(PhysicalStageBounds.pressureIncrement (WP j) (MP j))
theorem
NavierStokes.PhysicalStageSupport.candidate_support_inputs
{h : ℝ}
{DA DP : Type}
[NormedAddCommGroup DA]
[NormedSpace ℝ DA]
[NormedAddCommGroup DP]
[NormedSpace ℝ DP]
{IA : Type u_1}
{KA : Type u_2}
{IP : Type u_3}
{KP : Type u_4}
(WA : ℕ → PhysicalStageBounds.WaveData h DA IA KA (Fin 3))
(MA : ℕ → PhysicalStageBounds.MeanData h (CoordinateAlgebra.A h - 1 / 2))
(MB : ℕ → PhysicalStageBounds.MeanData h (CoordinateAlgebra.A h))
(WP : ℕ → PhysicalStageBounds.WaveData h DP IP KP Unit)
(MP : ℕ → PhysicalStageBounds.MeanData h (2 * CoordinateAlgebra.A h))
(hh : 0 < h)
(hh1 : h < 1 / 2)
{qbig R : ℝ}
(hqA : ∀ (j : ℕ), qbig ≤ ChartScales.Q (MA j).firstBand)
(hqB : ∀ (j : ℕ), qbig ≤ ChartScales.Q (MB j).firstBand)
(hqP : ∀ (j : ℕ), qbig ≤ ChartScales.Q (MP j).firstBand)
(H : NativeOuterBounds R WA MA MB WP MP)
(initial : MixedAxisPreservation.PotentialStage h (MixedAxisPreservation.localDomain h qbig))
(stages : ℕ → MixedAxisPreservation.PotentialStage h (MixedAxisPreservation.localDomain h qbig))
(D : ℕ → DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain h qbig))
(pInitial : ProblemStatement.PressureField)
(pStages : ℕ → ProblemStatement.PressureField)
(hInitial :
Set.EqOn initial.field (PhysicalStageBounds.potentialIncrement (WA 0) (MA 0))
(CutStageEstimates.physicalSublevel h qbig))
(hStages :
∀ (j : ℕ),
Set.EqOn (stages j).field (PhysicalStageBounds.potentialIncrement (WA (j + 1)) (MA (j + 1)))
(CutStageEstimates.physicalSublevel h qbig))
(hDirect :
∀ (j : ℕ),
Set.EqOn (LocalAngularDiagonal.rawSeries D j) (PhysicalStageBounds.directStages MB j)
(CutStageEstimates.physicalSublevel h qbig))
(hpInitial :
Set.EqOn pInitial (PhysicalStageBounds.pressureIncrement (WP 0) (MP 0)) (CutStageEstimates.physicalSublevel h qbig))
(hpStages :
∀ (j : ℕ),
Set.EqOn (pStages j) (PhysicalStageBounds.pressureIncrement (WP (j + 1)) (MP (j + 1)))
(CutStageEstimates.physicalSublevel h qbig))
:
MixedDiagonalExtensions.SublevelShrinkingSupport h (outerConstant R) qbig initial.field ∧ (∀ (j : ℕ), MixedDiagonalExtensions.SublevelShrinkingSupport h (outerConstant R) qbig (stages j).field) ∧ (∀ (j : ℕ),
MixedDiagonalExtensions.SublevelShrinkingSupport h (outerConstant R) qbig
(LocalAngularDiagonal.rawSeries D j)) ∧ MixedDiagonalExtensions.SublevelShrinkingSupport h (outerConstant R) qbig pInitial ∧ ∀ (j : ℕ), MixedDiagonalExtensions.SublevelShrinkingSupport h (outerConstant R) qbig (pStages j)
The common-radius conclusion is preserved by literal representations
of the five families supplied to MixedCandidateAssembly.
The initial field is the finite change, without the base potential.
theorem
NavierStokes.PhysicalStageSupport.potentialStages_positive_support
{h : ℝ}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{I : Type u_1}
{K : Type u_2}
(base : ProblemStatement.VelocityField)
(W : ℕ → PhysicalStageBounds.WaveData h D I K (Fin 3))
(M : ℕ → PhysicalStageBounds.MeanData h (CoordinateAlgebra.A h - 1 / 2))
(hh : 0 < h)
(hh1 : h < 1 / 2)
{qbig R : ℝ}
(hq : ∀ (j : ℕ), qbig ≤ ChartScales.Q (M j).firstBand)
(hW : ∀ (j : ℕ), (W j).upperRadius ≤ 2 * R)
(hM : ∀ (j : ℕ), (M j).upperRadius ≤ R)
(j : ℕ)
(hj : j ≠ 0)
:
MixedDiagonalExtensions.SublevelShrinkingSupport h (outerConstant R) qbig
(PhysicalStageBounds.potentialStages base W M j)
theorem
NavierStokes.PhysicalStageSupport.pressureStages_positive_support
{h : ℝ}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{I : Type u_1}
{K : Type u_2}
(base : ProblemStatement.PressureField)
(W : ℕ → PhysicalStageBounds.WaveData h D I K Unit)
(M : ℕ → PhysicalStageBounds.MeanData h (2 * CoordinateAlgebra.A h))
(hh : 0 < h)
(hh1 : h < 1 / 2)
{qbig R : ℝ}
(hq : ∀ (j : ℕ), qbig ≤ ChartScales.Q (M j).firstBand)
(hW : ∀ (j : ℕ), (W j).upperRadius ≤ 2 * R)
(hM : ∀ (j : ℕ), (M j).upperRadius ≤ R)
(j : ℕ)
(hj : j ≠ 0)
:
MixedDiagonalExtensions.SublevelShrinkingSupport h (outerConstant R) qbig
(PhysicalStageBounds.pressureStages base W M j)
theorem
NavierStokes.PhysicalStageSupport.potentialStages_initial_support
{h : ℝ}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{I : Type u_1}
{K : Type u_2}
(base : ProblemStatement.VelocityField)
(W : ℕ → PhysicalStageBounds.WaveData h D I K (Fin 3))
(M : ℕ → PhysicalStageBounds.MeanData h (CoordinateAlgebra.A h - 1 / 2))
(hh : 0 < h)
(hh1 : h < 1 / 2)
{qbig R : ℝ}
(hq : qbig ≤ ChartScales.Q (M 0).firstBand)
(hW : (W 0).upperRadius ≤ 2 * R)
(hM : (M 0).upperRadius ≤ R)
:
MixedDiagonalExtensions.SublevelShrinkingSupport h (outerConstant R) qbig fun (w : ProblemStatement.SpaceTime) =>
PhysicalStageBounds.potentialStages base W M 0 w - base w
Subtracting the base from initialized stage zero leaves exactly its finite supported potential increment.
theorem
NavierStokes.PhysicalStageSupport.pressureStages_initial_support
{h : ℝ}
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{I : Type u_1}
{K : Type u_2}
(base : ProblemStatement.PressureField)
(W : ℕ → PhysicalStageBounds.WaveData h D I K Unit)
(M : ℕ → PhysicalStageBounds.MeanData h (2 * CoordinateAlgebra.A h))
(hh : 0 < h)
(hh1 : h < 1 / 2)
{qbig R : ℝ}
(hq : qbig ≤ ChartScales.Q (M 0).firstBand)
(hW : (W 0).upperRadius ≤ 2 * R)
(hM : (M 0).upperRadius ≤ R)
:
MixedDiagonalExtensions.SublevelShrinkingSupport h (outerConstant R) qbig fun (w : ProblemStatement.SpaceTime) =>
PhysicalStageBounds.pressureStages base W M 0 w - base w
noncomputable def
NavierStokes.PhysicalStageSupport.geometryOuterConstant
(G : SignedMeanGain.Geometry)
:
Geometry outer constant, given by outerConstant G.patch.b.
Equations
Instances For
The concrete common constant for the manuscript's fixed actual patch.
Equations
Instances For
theorem
NavierStokes.PhysicalStageSupport.actual_coherent_support
{degree : ℝ}
{N gap : ℕ}
(D :
PhysicalMeanJetBounds.CoherentFamily CorrectionInitialization.ActualPrimary.h degree N gap
CorrectionInitialization.ActualPrimary.standardRegion.carrier ℝ)
(hs :
PhysicalMeanJetBounds.NativeSupport CorrectionInitialization.ActualPrimary.h ActualInitialization.geometry.patch.a
ActualInitialization.geometry.patch.b N CorrectionInitialization.ActualPrimary.standardRegion.carrier D.native)
{qbig : ℝ}
(hq : qbig ≤ ChartScales.Q N)
:
A literal coherent family on the fixed actual mean domain has the same outer constant as the wave increments.
theorem
NavierStokes.PhysicalStageSupport.actual_patch_support
{DA DP : Type}
[NormedAddCommGroup DA]
[NormedSpace ℝ DA]
[NormedAddCommGroup DP]
[NormedSpace ℝ DP]
{IA : Type u_1}
{KA : Type u_2}
{IP : Type u_3}
{KP : Type u_4}
(WA : ℕ → PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DA IA KA (Fin 3))
(MA :
ℕ →
PhysicalStageBounds.MeanData CorrectionInitialization.ActualPrimary.h
(CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h - 1 / 2))
(MB :
ℕ →
PhysicalStageBounds.MeanData CorrectionInitialization.ActualPrimary.h
(CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h))
(WP : ℕ → PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DP IP KP Unit)
(MP :
ℕ →
PhysicalStageBounds.MeanData CorrectionInitialization.ActualPrimary.h
(2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h))
{qbig : ℝ}
(hqA : ∀ (j : ℕ), qbig ≤ ChartScales.Q (MA j).firstBand)
(hqB : ∀ (j : ℕ), qbig ≤ ChartScales.Q (MB j).firstBand)
(hqP : ∀ (j : ℕ), qbig ≤ ChartScales.Q (MP j).firstBand)
(H : NativeOuterBounds ActualInitialization.geometry.patch.b WA MA MB WP MP)
:
(∀ (j : ℕ),
MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h actualOuterConstant qbig
(PhysicalStageBounds.potentialIncrement (WA j) (MA j))) ∧ (∀ (j : ℕ),
MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h actualOuterConstant qbig
(PhysicalStageBounds.directStages MB j)) ∧ ∀ (j : ℕ),
MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h actualOuterConstant qbig
(PhysicalStageBounds.pressureIncrement (WP j) (MP j))
@[reducible, inline]
The actual mean-domain type retains the strict normalized range
(1/2,2) used by the construction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
NavierStokes.PhysicalStageSupport.ActualNativeSupport
{degree : ℝ}
{N gap : ℕ}
(D : ActualMeanFamily degree N gap)
:
Native support on the single fixed actual patch.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.PhysicalStageSupport.actual_coherent_families_support
{DA DP : Type}
[NormedAddCommGroup DA]
[NormedSpace ℝ DA]
[NormedAddCommGroup DP]
[NormedSpace ℝ DP]
{IA : Type u_1}
{KA : Type u_2}
{IP : Type u_3}
{KP : Type u_4}
(WA : ℕ → PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DA IA KA (Fin 3))
(WP : ℕ → PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DP IP KP Unit)
{NA GA NB GB NP GP : ℕ → ℕ}
(MA : (j : ℕ) → ActualMeanFamily (CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h - 1 / 2) (NA j) (GA j))
(MB : (j : ℕ) → ActualMeanFamily (CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) (NB j) (GB j))
(MP : (j : ℕ) → ActualMeanFamily (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) (NP j) (GP j))
(hsA : ∀ (j : ℕ), ActualNativeSupport (MA j))
(hsB : ∀ (j : ℕ), ActualNativeSupport (MB j))
(hsP : ∀ (j : ℕ), ActualNativeSupport (MP j))
{qbig : ℝ}
(hqA : ∀ (j : ℕ), qbig ≤ ChartScales.Q (NA j))
(hqB : ∀ (j : ℕ), qbig ≤ ChartScales.Q (NB j))
(hqP : ∀ (j : ℕ), qbig ≤ ChartScales.Q (NP j))
(hWA : ∀ (j : ℕ), (WA j).upperRadius ≤ 2 * ActualInitialization.geometry.patch.b)
(hWP : ∀ (j : ℕ), (WP j).upperRadius ≤ 2 * ActualInitialization.geometry.patch.b)
:
(∀ (j : ℕ),
MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h actualOuterConstant qbig
fun (w : ProblemStatement.SpaceTime) =>
(WA j).vector w + PhysicalMeanJetBounds.CoherentFamily.angularField (MA j) w) ∧ (∀ (j : ℕ),
MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h actualOuterConstant qbig
(PhysicalMeanJetBounds.CoherentFamily.angularField (MB j))) ∧ ∀ (j : ℕ),
MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h actualOuterConstant qbig
fun (w : ProblemStatement.SpaceTime) => (WP j).pressure w + PhysicalMeanJetBounds.CoherentFamily.field (MP j) w
One constant for the literal coherent mean families and actual wave
representations. This is the valid-domain alternative to MeanData's wider
cover interface. Stage zero is included in each increment family.