The actual finite signed-wave assembly #
The selected primary slots, physical windows, and absolute auxiliary coordinate are shared by the current block and both wave increments. Support comes from the canonical source carrier and the actual native mask/cutoff product. Quantitative wave bounds are separate inputs.
The same label map used by the actual primary covariance.
Equations
Instances For
theorem
NavierStokes.ActualCycleAssembly.supported_of_zero_outside
{B N0 : ℕ}
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(u : Index B N0 → CorrectionState.Oscillation Point)
(hz :
∀ (l : ActualInitialization.Index B N0) (n : ℕ),
∀ x ∈ ActualInitialization.geometry.strip.domain,
x ∉ ActualInitialization.labelCarrier l n → ∀ (θ : ℝ) (i : Fin 3), u l n (x, θ) i = 0)
:
Canonical carrier support gives both pieces of the actual slot/window support predicate. This applies to any real oscillatory field.
theorem
NavierStokes.ActualCycleAssembly.oscillation_zero_of_inputSupport
(b : CorrectionState.HarmonicBlock Point)
(G A : HarmonicResidual.BlockCoefficients Point)
{U : Set Point}
{K : ℕ → Set Point}
(hs : HarmonicSourceSupport.InputSupportOn U K b G A)
(hzero : HarmonicWaveInteraction.ZeroMode b)
(n : ℕ)
{x : Point}
(hx : x ∈ U)
(hn : x ∉ K n)
(θ : ℝ)
(i : Fin 3)
:
Zero nonconstant real coefficients and an actual zero mode imply zero real field; no angular cancellation is postulated.
theorem
NavierStokes.ActualCycleAssembly.supported_of_inputSupport
{B N0 : ℕ}
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(b : Index B N0 → CorrectionState.HarmonicBlock Point)
(G A : Index B N0 → HarmonicResidual.BlockCoefficients Point)
(hs :
∀ (l : ActualInitialization.Index B N0),
HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualInitialization.labelCarrier l)
(b l) (G l) (A l))
(hzero : ∀ (l : Index B N0), HarmonicWaveInteraction.ZeroMode (b l))
:
theorem
NavierStokes.ActualCycleAssembly.signed_mask_cutoff_source
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(k : TorusInverse.Frequency)
(x : Point × ℝ)
(hm : ActualSignedStageControls.mask l k n x ≠ 0)
(hc : ActualSignedStageControls.cutoff l k n x ≠ 0)
:
Nonzero values of the actual spatial mask and native cutoff locate the point in the fixed closed source carrier.
theorem
NavierStokes.ActualCycleAssembly.signed_mask_or_cutoff_zero
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(k : TorusInverse.Frequency)
{x : Point × ℝ}
(hx : x.1 ∉ ActualInitialization.labelCarrier l n)
:
theorem
NavierStokes.ActualCycleAssembly.signed_localized_zero
{B N0 : ℕ}
(l : Index B N0)
(s : WeightedClasses.StripData Point)
(request : ℕ → Point × ℝ → SignedWaveUpdate.Vec2)
(n : ℕ)
(k : TorusInverse.Frequency)
{x : Point × ℝ}
(hx : x.1 ∉ ActualInitialization.labelCarrier l n)
:
theorem
NavierStokes.ActualCycleAssembly.signed_common_zero
{B N0 : ℕ}
(l : Index B N0)
(s : WeightedClasses.StripData Point)
(request : ℕ → Point × ℝ → SignedWaveUpdate.Vec2)
(n : ℕ)
{x : Point × ℝ}
(hx : x.1 ∉ ActualInitialization.labelCarrier l n)
:
theorem
NavierStokes.ActualCycleAssembly.signed_common_zero_germs
{B N0 : ℕ}
(l : Index B N0)
(s : WeightedClasses.StripData Point)
(request : ℕ → Point × ℝ → SignedWaveUpdate.Vec2)
(n : ℕ)
{x : Point × ℝ}
(hx : x.1 ∉ ActualInitialization.labelCarrier l n)
:
have a := (ActualSignedStageControls.parameters l).copyData s request;
(a.common.amplitude n =ᶠ[nhds x] fun (x : Point × ℝ) => 0) ∧ ((a.commonCorrected (HarmonicWaveInteraction.productStrip s)
(ActualSignedStageControls.parameters l).directions).amplitude
n =ᶠ[nhds x] fun (x : Point × ℝ) => 0) ∧ a.common.pressure n =ᶠ[nhds x] fun (x : Point × ℝ) => 0
The common tangent and the exact curl-corrected amplitude both vanish as genuine ambient germs outside the same closed carrier.
theorem
NavierStokes.ActualCycleAssembly.tangent_inputSupport
{B N0 : ℕ}
(l : Index B N0)
(s : WeightedClasses.StripData Point)
(request : ℕ → Point × ℝ → SignedWaveUpdate.Vec2)
:
theorem
NavierStokes.ActualCycleAssembly.exact_inputSupport
{B N0 : ℕ}
(l : Index B N0)
(s : WeightedClasses.StripData Point)
(request : ℕ → Point × ℝ → SignedWaveUpdate.Vec2)
:
theorem
NavierStokes.ActualCycleAssembly.inputSupport_subBlock
{U : Set Point}
{K : ℕ → Set Point}
{a b : CorrectionState.HarmonicBlock Point}
(ha : HarmonicSourceSupport.InputSupportOn U K a 0 0)
(hb : HarmonicSourceSupport.InputSupportOn U K b 0 0)
:
HarmonicSourceSupport.InputSupportOn U K (LabelSumBounds.subBlock a b) 0 0
theorem
NavierStokes.ActualCycleAssembly.curl_inputSupport
{B N0 : ℕ}
(l : Index B N0)
(s : WeightedClasses.StripData Point)
(request : ℕ → Point × ℝ → SignedWaveUpdate.Vec2)
:
theorem
NavierStokes.ActualCycleAssembly.tangent_zeroMode
{B N0 : ℕ}
(l : Index B N0)
(s : WeightedClasses.StripData Point)
(request : ℕ → Point × ℝ → SignedWaveUpdate.Vec2)
:
theorem
NavierStokes.ActualCycleAssembly.curl_zeroMode
{B N0 : ℕ}
(l : Index B N0)
(s : WeightedClasses.StripData Point)
(request : ℕ → Point × ℝ → SignedWaveUpdate.Vec2)
:
theorem
NavierStokes.ActualCycleAssembly.tangent_supported
{B N0 : ℕ}
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(s : WeightedClasses.StripData Point)
(request : ℕ → Point × ℝ → SignedWaveUpdate.Vec2)
:
LabelSumBounds.SupportedOscillations CorrectionInitialization.ActualPrimary.slots label
ActualPrimaryCovariance.physicalWindow ActualPrimaryCovariance.absoluteAuxiliary
ActualInitialization.geometry.strip.domain fun (l : Index B N0) =>
((ActualSignedStageControls.parameters l).tangentBlock s request).oscillation
theorem
NavierStokes.ActualCycleAssembly.curl_supported
{B N0 : ℕ}
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(s : WeightedClasses.StripData Point)
(request : ℕ → Point × ℝ → SignedWaveUpdate.Vec2)
:
LabelSumBounds.SupportedOscillations CorrectionInitialization.ActualPrimary.slots label
ActualPrimaryCovariance.physicalWindow ActualPrimaryCovariance.absoluteAuxiliary
ActualInitialization.geometry.strip.domain fun (l : Index B N0) =>
((ActualSignedStageControls.parameters l).curlBlock s request).oscillation
theorem
NavierStokes.ActualCycleAssembly.signed_cutoff_sourceCell
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(k : TorusInverse.Frequency)
{x : Point × ℝ}
(hc : ActualSignedStageControls.cutoff l k n x ≠ 0)
:
theorem
NavierStokes.ActualCycleAssembly.signed_cutoff_or_mask_germ
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
(k : TorusInverse.Frequency)
{x : Point × ℝ}
(hx : x.1 ∉ ActualInitialization.labelCarrier l n)
:
Outside the broad carrier the actual cutoff or the actual slow mask vanishes on a neighborhood. This also controls cutoff derivatives.
theorem
NavierStokes.ActualCycleAssembly.signed_exact_gaussian_zero_germs
{B N0 : ℕ}
(l : Index B N0)
(s : WeightedClasses.StripData Point)
(request : ℕ → Point × ℝ → SignedWaveUpdate.Vec2)
(n : ℕ)
{x : Point × ℝ}
(hx : x.1 ∉ ActualInitialization.labelCarrier l n)
:
have a := (ActualSignedStageControls.parameters l).copyData s request;
((a.commonCorrected (HarmonicWaveInteraction.productStrip s)
(ActualSignedStageControls.parameters l).directions).amplitude
n =ᶠ[nhds x] fun (x : Point × ℝ) => 0) ∧ (a.common.pressure n =ᶠ[nhds x] fun (x : Point × ℝ) => 0) ∧ a.globalGaussian (ActualSignedStageControls.parameters l).directions n =ᶠ[nhds x] fun (x : Point × ℝ) => 0
theorem
NavierStokes.ActualCycleAssembly.refined_signed_localized_zero
{B N0 : ℕ}
(l : Index B N0)
(s : WeightedClasses.StripData Point)
(request : ℕ → Point × ℝ → SignedWaveUpdate.Vec2)
(n : ℕ)
(k : TorusInverse.Frequency)
{x : Point × ℝ}
(hx : x.1 ∈ ActualInitialization.geometry.domain)
(hn : x.1 ∉ ActualCoreSupport.refinedCarrier l n)
:
The refined radial and dyadic constraints are literal factors of the signed target and mask, for any request.
theorem
NavierStokes.ActualCycleAssembly.refined_signed_common_zero
{B N0 : ℕ}
(l : Index B N0)
(s : WeightedClasses.StripData Point)
(request : ℕ → Point × ℝ → SignedWaveUpdate.Vec2)
(n : ℕ)
{x : Point × ℝ}
(hx : x.1 ∈ ActualInitialization.geometry.domain)
(hn : x.1 ∉ ActualCoreSupport.refinedCarrier l n)
:
theorem
NavierStokes.ActualCycleAssembly.refined_signed_common_zero_germs
{B N0 : ℕ}
(l : Index B N0)
(s : WeightedClasses.StripData Point)
(request : ℕ → Point × ℝ → SignedWaveUpdate.Vec2)
(n : ℕ)
{x : Point × ℝ}
(hx : x.1 ∈ ActualInitialization.geometry.domain)
(hn : x.1 ∉ ActualCoreSupport.refinedCarrier l n)
:
have a := (ActualSignedStageControls.parameters l).copyData s request;
(a.common.amplitude n =ᶠ[nhds x] fun (x : Point × ℝ) => 0) ∧ ((a.commonCorrected (HarmonicWaveInteraction.productStrip s)
(ActualSignedStageControls.parameters l).directions).amplitude
n =ᶠ[nhds x] fun (x : Point × ℝ) => 0) ∧ a.common.pressure n =ᶠ[nhds x] fun (x : Point × ℝ) => 0
theorem
NavierStokes.ActualCycleAssembly.refined_signed_gaussian_zero
{B N0 : ℕ}
(l : Index B N0)
(s : WeightedClasses.StripData Point)
(request : ℕ → Point × ℝ → SignedWaveUpdate.Vec2)
(n : ℕ)
{x : Point × ℝ}
(hx : x.1 ∈ ActualInitialization.geometry.domain)
(hn : x.1 ∉ ActualCoreSupport.refinedCarrier l n)
:
((ActualSignedStageControls.parameters l).copyData s request).globalGaussian
(ActualSignedStageControls.parameters l).directions n x = 0
theorem
NavierStokes.ActualCycleAssembly.refined_signed_inputSupport
{B N0 : ℕ}
(l : Index B N0)
(s : WeightedClasses.StripData Point)
(request : ℕ → Point × ℝ → SignedWaveUpdate.Vec2)
:
The exact signed block and its actual Gaussian error preserve the refined source carrier. Neither the request nor its support is assumed.
theorem
NavierStokes.ActualCycleAssembly.refined_tangent_inputSupport
{B N0 : ℕ}
(l : Index B N0)
(s : WeightedClasses.StripData Point)
(request : ℕ → Point × ℝ → SignedWaveUpdate.Vec2)
:
theorem
NavierStokes.ActualCycleAssembly.refined_curl_inputSupport
{B N0 : ℕ}
(l : Index B N0)
(s : WeightedClasses.StripData Point)
(request : ℕ → Point × ℝ → SignedWaveUpdate.Vec2)
:
theorem
NavierStokes.ActualCycleAssembly.inputSupport_reindex_on
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(e : D ≃ₗᵢ[ℝ] E)
{U : Set E}
{K : ℕ → Set E}
{V : Set D}
{T : ℕ → Set D}
{b : CorrectionState.HarmonicBlock E}
{G A : HarmonicResidual.BlockCoefficients E}
(hs : HarmonicSourceSupport.InputSupportOn U K b G A)
(hU : ∀ z ∈ V, e z ∈ U)
(hK : ∀ (n : ℕ), ∀ z ∈ V, e z ∈ K n → z ∈ T n)
:
theorem
NavierStokes.ActualCycleAssembly.associated_inputSupport
{B N0 : ℕ}
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(l : Index B N0)
{b : CorrectionState.HarmonicBlock Point}
{G A : HarmonicResidual.BlockCoefficients Point}
(hs :
HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualInitialization.labelCarrier l) b G A)
:
HarmonicSourceSupport.InputSupportOn (ActualCarrierTransportBase.parameterDomain ×ˢ Set.univ)
(ActualCarrierTransportBase.canonicalSourceRegion l) (StateReindex.block CorrectionStep.cycleAssoc.symm b)
(StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm G)
(StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm A)
theorem
NavierStokes.ActualCycleAssembly.canonical_copyData_eq_scalar
{B N0 : ℕ}
(l : Index B N0)
(c : CorrectionState.Context (CorrectionStep.CycleSlow × TorusInverse.Plane))
(u : CorrectionState.State (CorrectionStep.CycleSlow × TorusInverse.Plane))
(b : CorrectionState.HarmonicBlock (CorrectionStep.CycleSlow × TorusInverse.Plane))
(G A : HarmonicResidual.BlockCoefficients (CorrectionStep.CycleSlow × TorusInverse.Plane))
(j : ℤ)
:
have p := ActualParticularStageControls.canonicalParameters (l.2, l.1);
p.copyData c u b G A j = ScalarParticularSupport.scalarData (ParticularWaveAssembly.actualCarrier p.background b j)
(fun (n : ℕ) => ParticularWaveAssembly.angleTangent (p.tangent j n))
(ParticularWaveAssembly.sourceFamily c u b G A j) (ActualCarrierTransportBase.geometry l)
(fun (x : ℕ) => CorrectionInitialization.ActualPrimary.slots.radius)
(fun (x : ℕ) => ActualCarrierTransportBase.referenceLength l) (ActualCarrierTransportBase.clock l) ⋯ ⋯ ⋯
Particular cells, constructed using ScalarParticularSupport.scalarCells.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ActualCycleAssembly.canonical_cutoff_support
{B N0 : ℕ}
(l : Index B N0)
(c : CorrectionState.Context (CorrectionStep.CycleSlow × TorusInverse.Plane))
(u : CorrectionState.State (CorrectionStep.CycleSlow × TorusInverse.Plane))
(b : CorrectionState.HarmonicBlock (CorrectionStep.CycleSlow × TorusInverse.Plane))
(G A : HarmonicResidual.BlockCoefficients (CorrectionStep.CycleSlow × TorusInverse.Plane))
(j : ℤ)
(n : ℕ)
(k : TorusInverse.Frequency)
:
Function.support (((ActualParticularStageControls.canonicalParameters (l.2, l.1)).copyData c u b G A j).cutoff n k) ⊆
(particularCells l).carrier n k
theorem
NavierStokes.ActualCycleAssembly.canonical_source_zero_germ
{B N0 : ℕ}
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(l : Index B N0)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(b : CorrectionState.HarmonicBlock Point)
(G A : HarmonicResidual.BlockCoefficients Point)
(hs :
HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualInitialization.labelCarrier l) b G A)
(j : ℤ)
(n : ℕ)
{z : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane}
(hz : z.1.1 ∈ ActualCarrierTransportBase.parameterDomain)
(hn : (z.1.1, z.2) ∉ ActualCarrierTransportBase.canonicalSourceRegion l n)
:
ParticularWaveAssembly.sourceFamily (StateReindex.context CorrectionStep.cycleAssoc.symm c)
(StateReindex.state CorrectionStep.cycleAssoc.symm u) (StateReindex.block CorrectionStep.cycleAssoc.symm b)
(StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm G)
(StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm A) j n =ᶠ[nhds z] fun (x : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane) => 0
theorem
NavierStokes.ActualCycleAssembly.canonical_copy_zero_germs
{B N0 : ℕ}
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(l : Index B N0)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(b : CorrectionState.HarmonicBlock Point)
(G A : HarmonicResidual.BlockCoefficients Point)
(hs :
HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualInitialization.labelCarrier l) b G A)
(j : ℤ)
(s : WeightedClasses.StripData ((CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane))
(d : LinearWaveBounds.GraphDirections ((CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane))
(n : ℕ)
{z : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane}
(hz : z.1.1 ∈ ActualCarrierTransportBase.parameterDomain)
(hn : (z.1.1, z.2) ∉ ActualCarrierTransportBase.canonicalSourceRegion l n)
:
have a :=
(ActualParticularStageControls.canonicalParameters (l.2, l.1)).copyData
(StateReindex.context CorrectionStep.cycleAssoc.symm c) (StateReindex.state CorrectionStep.cycleAssoc.symm u)
(StateReindex.block CorrectionStep.cycleAssoc.symm b)
(StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm G)
(StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm A) j;
((a.commonCorrected s d).amplitude n =ᶠ[nhds z] fun (x : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane) => 0) ∧ (a.common.pressure n =ᶠ[nhds z] fun (x : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane) => 0) ∧ a.globalGaussian d n =ᶠ[nhds z] fun (x : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane) => 0
theorem
NavierStokes.ActualCycleAssembly.source_zero_germ_of_factorization
{B N0 : ℕ}
(l : Index B N0)
(K : ℕ → Set Point)
(slowCarrier : ℕ → Set CorrectionStep.CycleSlow)
(hK : ∀ (n : ℕ), IsClosed (K n))
(hfactor :
∀ (n : ℕ),
∀ p ∈ ActualCarrierTransportBase.parameterDomain,
∀ (Y : ActualCarrierTransportBase.Plane),
ActualCarrierTransportBase.associatedPoint p Y ∈ K n ↔ (p, Y) ∈ ActualGaussianCoverage.sourceRegion (slowCarrier n) (ActualCarrierTransportBase.geometry l n)
CorrectionInitialization.ActualPrimary.slots.radius (ActualCarrierTransportBase.referenceLength l)
(ActualCarrierTransportBase.clock l n))
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(b : CorrectionState.HarmonicBlock Point)
(G A : HarmonicResidual.BlockCoefficients Point)
(hs : HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain K b G A)
(j : ℤ)
(n : ℕ)
{z : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane}
(hz : z.1.1 ∈ ActualCarrierTransportBase.parameterDomain)
(hn :
(z.1.1, z.2) ∉
ActualGaussianCoverage.sourceRegion (slowCarrier n) (ActualCarrierTransportBase.geometry l n)
CorrectionInitialization.ActualPrimary.slots.radius (ActualCarrierTransportBase.referenceLength l)
(ActualCarrierTransportBase.clock l n))
:
ParticularWaveAssembly.sourceFamily (StateReindex.context CorrectionStep.cycleAssoc.symm c)
(StateReindex.state CorrectionStep.cycleAssoc.symm u) (StateReindex.block CorrectionStep.cycleAssoc.symm b)
(StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm G)
(StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm A) j n =ᶠ[nhds z] fun (x : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane) => 0
A closed incoming carrier with slow-coordinate factors supplies the whole-path source germs, including additional refined slow constraints.
theorem
NavierStokes.ActualCycleAssembly.native_zero_alternative_of_factorization
{B N0 : ℕ}
(l : Index B N0)
(K : ℕ → Set Point)
(slowCarrier : ℕ → Set CorrectionStep.CycleSlow)
(hK : ∀ (n : ℕ), IsClosed (K n))
(hfactor :
∀ (n : ℕ),
∀ p ∈ ActualCarrierTransportBase.parameterDomain,
∀ (Y : ActualCarrierTransportBase.Plane),
ActualCarrierTransportBase.associatedPoint p Y ∈ K n ↔ (p, Y) ∈ ActualGaussianCoverage.sourceRegion (slowCarrier n) (ActualCarrierTransportBase.geometry l n)
CorrectionInitialization.ActualPrimary.slots.radius (ActualCarrierTransportBase.referenceLength l)
(ActualCarrierTransportBase.clock l n))
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(b : CorrectionState.HarmonicBlock Point)
(G A : HarmonicResidual.BlockCoefficients Point)
(hs : HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain K b G A)
(j : ℤ)
(n : ℕ)
(k : TorusInverse.Frequency)
{z : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane}
(hz : z.1.1 ∈ ActualCarrierTransportBase.parameterDomain)
(hk : z ∈ (particularCells l).carrier n k)
(hn :
(z.1.1, z.2) ∉
ActualGaussianCoverage.sourceRegion (slowCarrier n) (ActualCarrierTransportBase.geometry l n)
CorrectionInitialization.ActualPrimary.slots.radius (ActualCarrierTransportBase.referenceLength l)
(ActualCarrierTransportBase.clock l n))
:
have a :=
(ActualParticularStageControls.canonicalParameters (l.2, l.1)).copyData
(StateReindex.context CorrectionStep.cycleAssoc.symm c) (StateReindex.state CorrectionStep.cycleAssoc.symm u)
(StateReindex.block CorrectionStep.cycleAssoc.symm b)
(StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm G)
(StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm A) j;
(a.cutoff n k =ᶠ[nhds z] fun (x : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane) => 0) ∨ (a.amplitude n k =ᶠ[nhds z] fun (x : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane) => 0) ∧ (a.pressure n k =ᶠ[nhds z] fun (x : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane) => 0) ∧ a.source n =ᶠ[nhds z] fun (x : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane) => 0
The source germ is retained in the raw-zero branch, as required by the actual linear cancellation identity.
theorem
NavierStokes.ActualCycleAssembly.common_raw_zero_germ_of_factorization
{B N0 : ℕ}
(l : Index B N0)
(K : ℕ → Set Point)
(slowCarrier : ℕ → Set CorrectionStep.CycleSlow)
(hK : ∀ (n : ℕ), IsClosed (K n))
(hfactor :
∀ (n : ℕ),
∀ p ∈ ActualCarrierTransportBase.parameterDomain,
∀ (Y : ActualCarrierTransportBase.Plane),
ActualCarrierTransportBase.associatedPoint p Y ∈ K n ↔ (p, Y) ∈ ActualGaussianCoverage.sourceRegion (slowCarrier n) (ActualCarrierTransportBase.geometry l n)
CorrectionInitialization.ActualPrimary.slots.radius (ActualCarrierTransportBase.referenceLength l)
(ActualCarrierTransportBase.clock l n))
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(b : CorrectionState.HarmonicBlock Point)
(G A : HarmonicResidual.BlockCoefficients Point)
(hs : HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain K b G A)
(j : ℤ)
(n : ℕ)
{z : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane}
(hz : z.1.1 ∈ ActualCarrierTransportBase.parameterDomain)
(hn :
(z.1.1, z.2) ∉
ActualGaussianCoverage.sourceRegion (slowCarrier n) (ActualCarrierTransportBase.geometry l n)
CorrectionInitialization.ActualPrimary.slots.radius (ActualCarrierTransportBase.referenceLength l)
(ActualCarrierTransportBase.clock l n))
:
have a :=
(ActualParticularStageControls.canonicalParameters (l.2, l.1)).copyData
(StateReindex.context CorrectionStep.cycleAssoc.symm c) (StateReindex.state CorrectionStep.cycleAssoc.symm u)
(StateReindex.block CorrectionStep.cycleAssoc.symm b)
(StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm G)
(StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm A) j;
a.common.amplitude n =ᶠ[nhds z] fun (x : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane) => 0
theorem
NavierStokes.ActualCycleAssembly.copy_zero_germs_of_factorization
{B N0 : ℕ}
(l : Index B N0)
(K : ℕ → Set Point)
(slowCarrier : ℕ → Set CorrectionStep.CycleSlow)
(hK : ∀ (n : ℕ), IsClosed (K n))
(hfactor :
∀ (n : ℕ),
∀ p ∈ ActualCarrierTransportBase.parameterDomain,
∀ (Y : ActualCarrierTransportBase.Plane),
ActualCarrierTransportBase.associatedPoint p Y ∈ K n ↔ (p, Y) ∈ ActualGaussianCoverage.sourceRegion (slowCarrier n) (ActualCarrierTransportBase.geometry l n)
CorrectionInitialization.ActualPrimary.slots.radius (ActualCarrierTransportBase.referenceLength l)
(ActualCarrierTransportBase.clock l n))
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(b : CorrectionState.HarmonicBlock Point)
(G A : HarmonicResidual.BlockCoefficients Point)
(hs : HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain K b G A)
(j : ℤ)
(s : WeightedClasses.StripData ((CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane))
(d : LinearWaveBounds.GraphDirections ((CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane))
(n : ℕ)
{z : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane}
(hz : z.1.1 ∈ ActualCarrierTransportBase.parameterDomain)
(hn :
(z.1.1, z.2) ∉
ActualGaussianCoverage.sourceRegion (slowCarrier n) (ActualCarrierTransportBase.geometry l n)
CorrectionInitialization.ActualPrimary.slots.radius (ActualCarrierTransportBase.referenceLength l)
(ActualCarrierTransportBase.clock l n))
:
have a :=
(ActualParticularStageControls.canonicalParameters (l.2, l.1)).copyData
(StateReindex.context CorrectionStep.cycleAssoc.symm c) (StateReindex.state CorrectionStep.cycleAssoc.symm u)
(StateReindex.block CorrectionStep.cycleAssoc.symm b)
(StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm G)
(StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm A) j;
((a.commonCorrected s d).amplitude n =ᶠ[nhds z] fun (x : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane) => 0) ∧ (a.common.pressure n =ᶠ[nhds z] fun (x : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane) => 0) ∧ a.globalGaussian d n =ᶠ[nhds z] fun (x : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane) => 0
theorem
NavierStokes.ActualCycleAssembly.associated_update_inputSupport
{B N0 : ℕ}
(l : Index B N0)
(K : ℕ → Set Point)
(slowCarrier : ℕ → Set CorrectionStep.CycleSlow)
(hK : ∀ (n : ℕ), IsClosed (K n))
(hfactor :
∀ (n : ℕ),
∀ p ∈ ActualCarrierTransportBase.parameterDomain,
∀ (Y : ActualCarrierTransportBase.Plane),
ActualCarrierTransportBase.associatedPoint p Y ∈ K n ↔ (p, Y) ∈ ActualGaussianCoverage.sourceRegion (slowCarrier n) (ActualCarrierTransportBase.geometry l n)
CorrectionInitialization.ActualPrimary.slots.radius (ActualCarrierTransportBase.referenceLength l)
(ActualCarrierTransportBase.clock l n))
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(b : CorrectionState.HarmonicBlock Point)
(G A : HarmonicResidual.BlockCoefficients Point)
(hs : HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain K b G A)
(s : WeightedClasses.StripData (CorrectionStep.CycleSlow × TorusInverse.Plane))
(N : ℕ)
:
have p := ActualParticularStageControls.canonicalParameters (l.2, l.1);
HarmonicSourceSupport.InputSupportOn (ActualCarrierTransportBase.parameterDomain ×ˢ Set.univ)
(fun (n : ℕ) =>
ActualGaussianCoverage.sourceRegion (slowCarrier n) (ActualCarrierTransportBase.geometry l n)
CorrectionInitialization.ActualPrimary.slots.radius (ActualCarrierTransportBase.referenceLength l)
(ActualCarrierTransportBase.clock l n))
(p.updateBlock s (StateReindex.context CorrectionStep.cycleAssoc.symm c)
(StateReindex.state CorrectionStep.cycleAssoc.symm u) (StateReindex.block CorrectionStep.cycleAssoc.symm b)
(StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm G)
(StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm A) N)
(p.gaussianBlock (StateReindex.context CorrectionStep.cycleAssoc.symm c)
(StateReindex.state CorrectionStep.cycleAssoc.symm u) (StateReindex.block CorrectionStep.cycleAssoc.symm b)
(StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm G)
(StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm A) N).velocity
0
theorem
NavierStokes.ActualCycleAssembly.particular_inputSupport_of_factorization
{B N0 : ℕ}
(l : Index B N0)
(K : ℕ → Set Point)
(slowCarrier : ℕ → Set CorrectionStep.CycleSlow)
(hK : ∀ (n : ℕ), IsClosed (K n))
(hfactor :
∀ (n : ℕ),
∀ p ∈ ActualCarrierTransportBase.parameterDomain,
∀ (Y : ActualCarrierTransportBase.Plane),
ActualCarrierTransportBase.associatedPoint p Y ∈ K n ↔ (p, Y) ∈ ActualGaussianCoverage.sourceRegion (slowCarrier n) (ActualCarrierTransportBase.geometry l n)
CorrectionInitialization.ActualPrimary.slots.radius (ActualCarrierTransportBase.referenceLength l)
(ActualCarrierTransportBase.clock l n))
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(b : CorrectionState.HarmonicBlock Point)
(G A : HarmonicResidual.BlockCoefficients Point)
(hs : HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain K b G A)
(s : WeightedClasses.StripData Point)
(N : ℕ)
:
have p := ActualParticularStageControls.canonicalParameters (l.2, l.1);
HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain K
(StateReindex.block CorrectionStep.cycleAssoc
(p.updateBlock (ParticularWaveBounds.reindexStrip CorrectionStep.cycleAssoc.symm s)
(StateReindex.context CorrectionStep.cycleAssoc.symm c) (StateReindex.state CorrectionStep.cycleAssoc.symm u)
(StateReindex.block CorrectionStep.cycleAssoc.symm b)
(StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm G)
(StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm A) N))
(StateReindex.block CorrectionStep.cycleAssoc
(p.gaussianBlock (StateReindex.context CorrectionStep.cycleAssoc.symm c)
(StateReindex.state CorrectionStep.cycleAssoc.symm u) (StateReindex.block CorrectionStep.cycleAssoc.symm b)
(StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm G)
(StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm A) N)).velocity
0
The literal finite particular update and its Gaussian error preserve the closed incoming carrier. Only its slow-factor geometry is required.
noncomputable def
NavierStokes.ActualCycleAssembly.refinedSlowCore
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
:
Refined slow core, constructed using ActualCarrierTransport.activeSlowCore.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ActualCycleAssembly.refined_carrier_factorization
{B N0 : ℕ}
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(l : Index B N0)
(n : ℕ)
(p : CorrectionStep.CycleSlow)
(hp : p ∈ ActualCarrierTransportBase.parameterDomain)
(Y : TorusInverse.Plane)
:
ActualCarrierTransportBase.associatedPoint p Y ∈ ActualCoreSupport.refinedCarrier l n ↔ (p, Y) ∈ ActualGaussianCoverage.sourceRegion (refinedSlowCore l n) (ActualCarrierTransportBase.geometry l n)
CorrectionInitialization.ActualPrimary.slots.radius (ActualCarrierTransportBase.referenceLength l)
(ActualCarrierTransportBase.clock l n)
theorem
NavierStokes.ActualCycleAssembly.cycle_particular_inputSupport
{B N0 : ℕ}
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(x : CorrectionStep.CycleState (Index B N0))
(c : CorrectionState.Context Point)
(hs :
∀ (l : ActualInitialization.Index B N0),
HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualInitialization.labelCarrier l)
(x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l))
(l : Index B N0)
:
HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualInitialization.labelCarrier l)
((ActualCycleParameters.fixedParameters B N0).particularBlock x.coefficients c x.state l)
((ActualCycleParameters.fixedParameters B N0).particularGaussianBlock x.coefficients c x.state l).velocity 0
theorem
NavierStokes.ActualCycleAssembly.cycle_refined_particular_inputSupport
{B N0 : ℕ}
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(x : CorrectionStep.CycleState (Index B N0))
(c : CorrectionState.Context Point)
(hs :
∀ (l : ActualCoreSupport.Index B N0),
HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier l)
(x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l))
(l : Index B N0)
:
HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier l)
((ActualCycleParameters.fixedParameters B N0).particularBlock x.coefficients c x.state l)
((ActualCycleParameters.fixedParameters B N0).particularGaussianBlock x.coefficients c x.state l).velocity 0
theorem
NavierStokes.ActualCycleAssembly.refined_particular_zero_germs
{B N0 : ℕ}
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(l : Index B N0)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(b : CorrectionState.HarmonicBlock Point)
(G A : HarmonicResidual.BlockCoefficients Point)
(hs :
HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier l) b G A)
(j : ℤ)
(s : WeightedClasses.StripData ((CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane))
(n : ℕ)
{z : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane}
(hz : z.1.1 ∈ ActualCarrierTransportBase.parameterDomain)
(hn : ActualCarrierTransportBase.associatedPoint z.1.1 z.2 ∉ ActualCoreSupport.refinedCarrier l n)
:
have p := ActualParticularStageControls.canonicalParameters (l.2, l.1);
have a :=
p.copyData (StateReindex.context CorrectionStep.cycleAssoc.symm c)
(StateReindex.state CorrectionStep.cycleAssoc.symm u) (StateReindex.block CorrectionStep.cycleAssoc.symm b)
(StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm G)
(StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm A) j;
(a.common.amplitude n =ᶠ[nhds z] fun (x : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane) => 0) ∧ ((a.commonCorrected s p.directions).amplitude n =ᶠ[nhds z] fun (x : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane) => 0) ∧ (a.common.pressure n =ᶠ[nhds z] fun (x : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane) => 0) ∧ a.globalGaussian p.directions n =ᶠ[nhds z] fun (x : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane) => 0
All four actual common fields have zero germs off the refined carrier. The uncorrected amplitude is retained for edge continuation.
theorem
NavierStokes.ActualCycleAssembly.cycle_refined_signed_inputSupport
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Index B N0))
(c : CorrectionState.Context Point)
(l : Index B N0)
:
HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier l)
((ActualCycleParameters.fixedParameters B N0).signedBlock x.coefficients c x.state l)
((ActualCycleParameters.fixedParameters B N0).signedGaussianBlock x.coefficients c x.state l).velocity 0
The literal recomputed signed request is allowed, so this is the fixed cycle's exact block and Gaussian coefficient support.
noncomputable def
NavierStokes.ActualCycleAssembly.family
{B N0 : ℕ}
{σ κ : ℝ}
{P : Index B N0 → ℕ → Point → ℝ}
{carrier : Index B N0 → ℕ → Set Point}
(x : CorrectionStep.CycleState (Index B N0))
(H :
CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry
(CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock P carrier σ x)
(hσ : 1 / 5 ≤ σ)
(hpart :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass ActualInitialization.geometry.strip P (1 / 2 + σ)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) =>
(((ActualCycleParameters.fixedParameters B N0).particularBlock x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
n i).coeff
j z)
(htangent :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass ActualInitialization.geometry.strip P (1 / 2 + σ - κ)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) =>
(((ActualCycleParameters.fixedParameters B N0).signedTangent x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
n i).coeff
j z)
(hcurl :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass ActualInitialization.geometry.strip P (1 + σ - 2 * κ)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) =>
(((ActualCycleParameters.fixedParameters B N0).signedCurl x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
n i).coeff
j z)
(hP0 : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.strip.domain, 0 ≤ P l n z)
(hP1 : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.strip.domain, P l n z ≤ 1)
:
LabelSumBounds.SignedFamily ActualInitialization.geometry.strip P (1 / 2) (17 / 25) (1 / 2 + σ - κ) (1 + σ - 2 * κ)
The family is the literal cycle constructor, using the current coefficients and the fixed primary choice.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ActualCycleAssembly.inputSupport_mono
{U : Set Point}
{K T : ℕ → Set Point}
{b : CorrectionState.HarmonicBlock Point}
{G A : HarmonicResidual.BlockCoefficients Point}
(hs : HarmonicSourceSupport.InputSupportOn U K b G A)
(hKT : ∀ (n : ℕ), K n ⊆ T n)
:
HarmonicSourceSupport.InputSupportOn U T b G A
theorem
NavierStokes.ActualCycleAssembly.old_supported
{B N0 : ℕ}
{σ : ℝ}
{P : Index B N0 → ℕ → Point → ℝ}
{carrier : Index B N0 → ℕ → Set Point}
(x : CorrectionStep.CycleState (Index B N0))
(H :
CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry
(CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock P carrier σ x)
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(hcarrier : ∀ (l : Index B N0) (n : ℕ), carrier l n ⊆ ActualInitialization.labelCarrier l n)
:
theorem
NavierStokes.ActualCycleAssembly.particular_supported_of_inputSupport
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Index B N0))
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(hpartSupport :
∀ (l : ActualInitialization.Index B N0),
HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualInitialization.labelCarrier l)
((ActualCycleParameters.fixedParameters B N0).particularBlock x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l)
((ActualCycleParameters.fixedParameters B N0).particularGaussianBlock x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
0)
:
LabelSumBounds.SupportedOscillations CorrectionInitialization.ActualPrimary.slots label
ActualPrimaryCovariance.physicalWindow ActualPrimaryCovariance.absoluteAuxiliary
ActualInitialization.geometry.strip.domain fun (l : Index B N0) =>
((ActualCycleParameters.fixedParameters B N0).particularBlock x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillation
noncomputable def
NavierStokes.ActualCycleAssembly.assemblyOfParticularSupport
{B N0 : ℕ}
{σ κ : ℝ}
{P : Index B N0 → ℕ → Point → ℝ}
{carrier : Index B N0 → ℕ → Set Point}
(x : CorrectionStep.CycleState (Index B N0))
(H :
CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry
(CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock P carrier σ x)
(hσ : 1 / 5 ≤ σ)
(hpart :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass ActualInitialization.geometry.strip P (1 / 2 + σ)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) =>
(((ActualCycleParameters.fixedParameters B N0).particularBlock x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
n i).coeff
j z)
(htangent :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass ActualInitialization.geometry.strip P (1 / 2 + σ - κ)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) =>
(((ActualCycleParameters.fixedParameters B N0).signedTangent x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
n i).coeff
j z)
(hcurl :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass ActualInitialization.geometry.strip P (1 + σ - 2 * κ)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) =>
(((ActualCycleParameters.fixedParameters B N0).signedCurl x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
n i).coeff
j z)
(hP0 : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.strip.domain, 0 ≤ P l n z)
(hP1 : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.strip.domain, P l n z ≤ 1)
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(hcarrier : ∀ (l : Index B N0) (n : ℕ), carrier l n ⊆ ActualInitialization.labelCarrier l n)
(hpartSupport :
∀ (l : ActualInitialization.Index B N0),
HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualInitialization.labelCarrier l)
((ActualCycleParameters.fixedParameters B N0).particularBlock x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l)
((ActualCycleParameters.fixedParameters B N0).particularGaussianBlock x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
0)
:
SignedMeanGain.Assembly (family x H hσ hpart htangent hcurl hP0 hP1)
The geometric record uses the same fixed slots and the current finite label set. The particular support adapter is supplied below.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ActualCycleAssembly.assemblyOfParticularSupport_labels
{B N0 : ℕ}
{σ κ : ℝ}
{P : Index B N0 → ℕ → Point → ℝ}
{carrier : Index B N0 → ℕ → Set Point}
(x : CorrectionStep.CycleState (Index B N0))
(H :
CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry
(CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock P carrier σ x)
(hσ : 1 / 5 ≤ σ)
(hpart :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass ActualInitialization.geometry.strip P (1 / 2 + σ)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) =>
(((ActualCycleParameters.fixedParameters B N0).particularBlock x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
n i).coeff
j z)
(htangent :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass ActualInitialization.geometry.strip P (1 / 2 + σ - κ)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) =>
(((ActualCycleParameters.fixedParameters B N0).signedTangent x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
n i).coeff
j z)
(hcurl :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass ActualInitialization.geometry.strip P (1 + σ - 2 * κ)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) =>
(((ActualCycleParameters.fixedParameters B N0).signedCurl x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
n i).coeff
j z)
(hP0 : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.strip.domain, 0 ≤ P l n z)
(hP1 : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.strip.domain, P l n z ≤ 1)
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(hcarrier : ∀ (l : Index B N0) (n : ℕ), carrier l n ⊆ ActualInitialization.labelCarrier l n)
(hpartSupport :
∀ (l : ActualInitialization.Index B N0),
HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualInitialization.labelCarrier l)
((ActualCycleParameters.fixedParameters B N0).particularBlock x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l)
((ActualCycleParameters.fixedParameters B N0).particularGaussianBlock x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
0)
:
(assemblyOfParticularSupport x H hσ hpart htangent hcurl hP0 hP1 hN hcarrier hpartSupport).labels = x.coefficients.labels
noncomputable def
NavierStokes.ActualCycleAssembly.assembly
{B N0 : ℕ}
{σ κ : ℝ}
{P : Index B N0 → ℕ → Point → ℝ}
{carrier : Index B N0 → ℕ → Set Point}
(x : CorrectionStep.CycleState (Index B N0))
(H :
CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry
(CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock P carrier σ x)
(hσ : 1 / 5 ≤ σ)
(hpart :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass ActualInitialization.geometry.strip P (1 / 2 + σ)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) =>
(((ActualCycleParameters.fixedParameters B N0).particularBlock x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
n i).coeff
j z)
(htangent :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass ActualInitialization.geometry.strip P (1 / 2 + σ - κ)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) =>
(((ActualCycleParameters.fixedParameters B N0).signedTangent x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
n i).coeff
j z)
(hcurl :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass ActualInitialization.geometry.strip P (1 + σ - 2 * κ)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) =>
(((ActualCycleParameters.fixedParameters B N0).signedCurl x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
n i).coeff
j z)
(hP0 : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.strip.domain, 0 ≤ P l n z)
(hP1 : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.strip.domain, P l n z ≤ 1)
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(hcarrier : ∀ (l : Index B N0) (n : ℕ), carrier l n ⊆ ActualInitialization.labelCarrier l n)
:
SignedMeanGain.Assembly (family x H hσ hpart htangent hcurl hP0 hP1)
The actual geometric constructor. Incoming primitive support is transported through the particular solve; signed support is proved above.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ActualCycleAssembly.assembly_labels
{B N0 : ℕ}
{σ κ : ℝ}
{P : Index B N0 → ℕ → Point → ℝ}
{carrier : Index B N0 → ℕ → Set Point}
(x : CorrectionStep.CycleState (Index B N0))
(H :
CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry
(CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock P carrier σ x)
(hσ : 1 / 5 ≤ σ)
(hpart :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass ActualInitialization.geometry.strip P (1 / 2 + σ)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) =>
(((ActualCycleParameters.fixedParameters B N0).particularBlock x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
n i).coeff
j z)
(htangent :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass ActualInitialization.geometry.strip P (1 / 2 + σ - κ)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) =>
(((ActualCycleParameters.fixedParameters B N0).signedTangent x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
n i).coeff
j z)
(hcurl :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass ActualInitialization.geometry.strip P (1 + σ - 2 * κ)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) =>
(((ActualCycleParameters.fixedParameters B N0).signedCurl x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
n i).coeff
j z)
(hP0 : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.strip.domain, 0 ≤ P l n z)
(hP1 : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.strip.domain, P l n z ≤ 1)
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(hcarrier : ∀ (l : Index B N0) (n : ℕ), carrier l n ⊆ ActualInitialization.labelCarrier l n)
:
theorem
NavierStokes.ActualCycleAssembly.family_primary
{B N0 : ℕ}
{σ κ : ℝ}
{P : Index B N0 → ℕ → Point → ℝ}
{carrier : Index B N0 → ℕ → Set Point}
(x : CorrectionStep.CycleState (Index B N0))
(H :
CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry
(CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock P carrier σ x)
(hσ : 1 / 5 ≤ σ)
(hpart :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass ActualInitialization.geometry.strip P (1 / 2 + σ)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) =>
(((ActualCycleParameters.fixedParameters B N0).particularBlock x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
n i).coeff
j z)
(htangent :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass ActualInitialization.geometry.strip P (1 / 2 + σ - κ)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) =>
(((ActualCycleParameters.fixedParameters B N0).signedTangent x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
n i).coeff
j z)
(hcurl :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass ActualInitialization.geometry.strip P (1 + σ - 2 * κ)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) =>
(((ActualCycleParameters.fixedParameters B N0).signedCurl x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
n i).coeff
j z)
(hP0 : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.strip.domain, 0 ≤ P l n z)
(hP1 : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.strip.domain, P l n z ≤ 1)
:
theorem
NavierStokes.ActualCycleAssembly.family_tangent
{B N0 : ℕ}
{σ κ : ℝ}
{P : Index B N0 → ℕ → Point → ℝ}
{carrier : Index B N0 → ℕ → Set Point}
(x : CorrectionStep.CycleState (Index B N0))
(H :
CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry
(CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock P carrier σ x)
(hσ : 1 / 5 ≤ σ)
(hpart :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass ActualInitialization.geometry.strip P (1 / 2 + σ)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) =>
(((ActualCycleParameters.fixedParameters B N0).particularBlock x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
n i).coeff
j z)
(htangent :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass ActualInitialization.geometry.strip P (1 / 2 + σ - κ)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) =>
(((ActualCycleParameters.fixedParameters B N0).signedTangent x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
n i).coeff
j z)
(hcurl :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass ActualInitialization.geometry.strip P (1 + σ - 2 * κ)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) =>
(((ActualCycleParameters.fixedParameters B N0).signedCurl x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
n i).coeff
j z)
(hP0 : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.strip.domain, 0 ≤ P l n z)
(hP1 : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.strip.domain, P l n z ≤ 1)
:
(family x H hσ hpart htangent hcurl hP0 hP1).tangent = (ActualCycleParameters.fixedParameters B N0).signedTangent x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state
theorem
NavierStokes.ActualCycleAssembly.assembly_supports
{B N0 : ℕ}
{σ κ : ℝ}
{P : Index B N0 → ℕ → Point → ℝ}
{carrier : Index B N0 → ℕ → Set Point}
(x : CorrectionStep.CycleState (Index B N0))
(H :
CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry
(CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock P carrier σ x)
(hσ : 1 / 5 ≤ σ)
(hpart :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass ActualInitialization.geometry.strip P (1 / 2 + σ)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) =>
(((ActualCycleParameters.fixedParameters B N0).particularBlock x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
n i).coeff
j z)
(htangent :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass ActualInitialization.geometry.strip P (1 / 2 + σ - κ)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) =>
(((ActualCycleParameters.fixedParameters B N0).signedTangent x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
n i).coeff
j z)
(hcurl :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass ActualInitialization.geometry.strip P (1 + σ - 2 * κ)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) =>
(((ActualCycleParameters.fixedParameters B N0).signedCurl x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).velocity
n i).coeff
j z)
(hP0 : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.strip.domain, 0 ≤ P l n z)
(hP1 : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.strip.domain, P l n z ≤ 1)
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(hcarrier : ∀ (l : Index B N0) (n : ℕ), carrier l n ⊆ ActualInitialization.labelCarrier l n)
:
have a := assembly x H hσ hpart htangent hcurl hP0 hP1 hN hcarrier;
a.labels = x.coefficients.labels ∧ (LabelSumBounds.SupportedOscillations a.slots a.label a.window a.auxiliary ActualInitialization.geometry.strip.domain
fun (l : Index B N0) => (x.coefficients.blocks l).oscillation) ∧ LabelSumBounds.SupportedOscillations a.slots a.label a.window a.auxiliary ActualInitialization.geometry.strip.domain
fun (l : Index B N0) =>
((ActualCycleParameters.fixedParameters B N0).particularBlock x.coefficients
(CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillation
The two additional support predicates consumed by mean composition come from the same assembly and the same finite labels.