Omitted labels in the actual current signed fields

The current potential and pressure are constructed from the same signed copy sum as the correction cycle. Their support implies membership in the actual active-label set, before any physical pullback or finite sum.

@[reducible, inline]

abbrev NavierStokes.ActualSignedCurrentSupport.Point : Type

Point: an abbreviation for ActualSignedCoherence.Point.

Equations

• NavierStokes.ActualSignedCurrentSupport.Point = NavierStokes.ActualSignedCoherence.Point

@[reducible, inline]

abbrev NavierStokes.ActualSignedCurrentSupport.FullPoint : Type

Full point: an abbreviation for ActualSignedCoherence.FullPoint.

Equations

• NavierStokes.ActualSignedCurrentSupport.FullPoint = NavierStokes.ActualSignedCoherence.FullPoint

@[reducible, inline]

abbrev NavierStokes.ActualSignedCurrentSupport.Index (B N0 : ℕ) : Type

Index: an abbreviation for ActualInitialization.Index.

Equations

• NavierStokes.ActualSignedCurrentSupport.Index = NavierStokes.ActualInitialization.Index

theorem NavierStokes.ActualSignedCurrentSupport.outside_core {B N0 : ℕ} (l : Index B N0) (n : ℕ) {x : Point} (hx : x ∈ ActualInitialization.geometry.domain) (hn : l ∉ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) : x ∉ ActualCoreSupport.refinedCarrier l n

theorem NavierStokes.ActualSignedCurrentSupport.common_zero {B N0 : ℕ} (l : Index B N0) (u : CorrectionState.State Point) (n : ℕ) {x : FullPoint} (hx : x.1 ∈ ActualInitialization.geometry.domain) (hn : l ∉ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) : (ActualSignedCoherence.copies l u).common.amplitude n x = 0 ∧ (ActualSignedCoherence.copies l u).common.pressure n x = 0

Zero values of the literal common coefficient, with arbitrary current state and no smoothness or residual bound hypothesis.

theorem NavierStokes.ActualSignedCurrentSupport.potentialCoefficient_zero {B N0 : ℕ} (l : Index B N0) (u : CorrectionState.State Point) (n : ℕ) {x : FullPoint} (hx : x.1 ∈ ActualInitialization.geometry.domain) (hn : l ∉ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) : ActualSignedPotentialCoherence.potentialCoefficient l u n x = 0

theorem NavierStokes.ActualSignedCurrentSupport.potential_zero {B N0 : ℕ} (l : Index B N0) (u : CorrectionState.State Point) (n : ℕ) {x : FullPoint} (hx : x.1 ∈ ActualInitialization.geometry.domain) (hn : l ∉ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) : ActualSignedPotentialCoherence.potential l u n x = 0

theorem NavierStokes.ActualSignedCurrentSupport.pressureMode_zero {B N0 : ℕ} (l : Index B N0) (u : CorrectionState.State Point) (n : ℕ) {x : FullPoint} (hx : x.1 ∈ ActualInitialization.geometry.domain) (hn : l ∉ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) : ActualSignedPotentialCoherence.pressureMode l u n x = 0

theorem NavierStokes.ActualSignedCurrentSupport.native_zero_germs {B N0 : ℕ} (l : Index B N0) (u : CorrectionState.State Point) (n : ℕ) {x : FullPoint} (hx : x.1 ∈ ActualInitialization.geometry.domain) (hn : l ∉ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) : (ActualSignedPotentialCoherence.potential l u n =ᶠ[nhds x] fun (x : FullPoint) => 0) ∧ ActualSignedPotentialCoherence.pressureMode l u n =ᶠ[nhds x] fun (x : FullPoint) => 0

theorem NavierStokes.ActualSignedCurrentSupport.cylindrical_zero {B N0 : ℕ} (l : Index B N0) (u : CorrectionState.State Point) (n : ℕ) {z : ProblemStatement.SpaceTime} (hz : z ∈ ActualSignedPotentialCoherence.physicalDomain n) (hn : l ∉ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) : ActualSignedPotentialCoherence.cylindricalPotential l u n z = 0 ∧ ActualSignedPotentialCoherence.cylindricalPressureMode l u n z = 0

theorem NavierStokes.ActualSignedCurrentSupport.physicalDomain_of_source (n : ℕ) {z : ProblemStatement.SpaceTime} (hz : z ∈ ActualPhysicalPrefixFields.source n) : z ∈ ActualSignedPotentialCoherence.physicalDomain n

theorem NavierStokes.ActualSignedCurrentSupport.currentPotential_zero {B N0 : ℕ} (l : Index B N0) (u : CorrectionState.State Point) (n : ℕ) {qbig a : ℝ} {i : PolarCharts.Index} {z : ProblemStatement.SpaceTime} (hz : z ∈ ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i) (hn : l ∉ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) : CurrentSignedCurl.currentPotential l u n a i z = 0

theorem NavierStokes.ActualSignedCurrentSupport.currentPressure_zero {B N0 : ℕ} (l : Index B N0) (u : CorrectionState.State Point) (n : ℕ) {qbig a : ℝ} {i : PolarCharts.Index} {z : ProblemStatement.SpaceTime} (hz : z ∈ ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i) (hn : l ∉ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) : CurrentSignedCurl.currentPressure l u n a i z = 0

theorem NavierStokes.ActualSignedCurrentSupport.currentPotential_zero_germ {B N0 : ℕ} (l : Index B N0) (u : CorrectionState.State Point) (n : ℕ) {qbig a : ℝ} (ha : 0 < a) {i : PolarCharts.Index} {z : ProblemStatement.SpaceTime} (hz : z ∈ ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i) (hn : l ∉ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) : CurrentSignedCurl.currentPotential l u n a i =ᶠ[nhds z] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.ActualSignedCurrentSupport.currentPressure_zero_germ {B N0 : ℕ} (l : Index B N0) (u : CorrectionState.State Point) (n : ℕ) {qbig a : ℝ} (ha : 0 < a) {i : PolarCharts.Index} {z : ProblemStatement.SpaceTime} (hz : z ∈ ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i) (hn : l ∉ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) : CurrentSignedCurl.currentPressure l u n a i =ᶠ[nhds z] fun (x : ProblemStatement.SpaceTime) => 0

The canonical sum is the finite current active-label sum

theorem NavierStokes.ActualSignedCurrentSupport.finsum_eq_active_sum {B N0 : ℕ} {E : Type u_1} [AddCommMonoid E] (n : ℕ) (f : Index B N0 → E) (hz : ∀ l ∉ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, f l = 0) : ∑ᶠ (l : Index B N0), f l = ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, f l

theorem NavierStokes.ActualSignedCurrentSupport.finsum_eq_labels_sum {B N0 : ℕ} {E : Type u_1} [AddCommMonoid E] (v : CorrectionStep.CycleCoefficients (Index B N0)) (hv : v.labels = CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0) (n : ℕ) (f : Index B N0 → E) (hz : ∀ l ∉ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, f l = 0) : ∑ᶠ (l : Index B N0), f l = ∑ l ∈ v.labels n, f l

theorem NavierStokes.ActualSignedCurrentSupport.potential_finsum {B N0 : ℕ} (u : CorrectionState.State Point) (n : ℕ) {x : FullPoint} (hx : x.1 ∈ ActualInitialization.geometry.domain) : ∑ᶠ (l : Index B N0), ActualSignedPotentialCoherence.potential l u n x = ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, ActualSignedPotentialCoherence.potential l u n x

theorem NavierStokes.ActualSignedCurrentSupport.pressureMode_finsum {B N0 : ℕ} (u : CorrectionState.State Point) (n : ℕ) {x : FullPoint} (hx : x.1 ∈ ActualInitialization.geometry.domain) : ∑ᶠ (l : Index B N0), ActualSignedPotentialCoherence.pressureMode l u n x = ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, ActualSignedPotentialCoherence.pressureMode l u n x

theorem NavierStokes.ActualSignedCurrentSupport.currentPotential_finsum {B N0 : ℕ} (u : CorrectionState.State Point) (n : ℕ) {qbig a : ℝ} {i : PolarCharts.Index} {z : ProblemStatement.SpaceTime} (hz : z ∈ ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i) : ∑ᶠ (l : Index B N0), CurrentSignedCurl.currentPotential l u n a i z = ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, CurrentSignedCurl.currentPotential l u n a i z

theorem NavierStokes.ActualSignedCurrentSupport.currentPressure_finsum {B N0 : ℕ} (u : CorrectionState.State Point) (n : ℕ) {qbig a : ℝ} {i : PolarCharts.Index} {z : ProblemStatement.SpaceTime} (hz : z ∈ ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i) : ∑ᶠ (l : Index B N0), CurrentSignedCurl.currentPressure l u n a i z = ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, CurrentSignedCurl.currentPressure l u n a i z

theorem NavierStokes.ActualSignedCurrentSupport.currentPotential_finsum_germ {B N0 : ℕ} (u : CorrectionState.State Point) (n : ℕ) {qbig a : ℝ} (ha : 0 < a) {i : PolarCharts.Index} {z : ProblemStatement.SpaceTime} (hz : z ∈ ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i) : (fun (w : ProblemStatement.SpaceTime) => ∑ᶠ (l : Index B N0), CurrentSignedCurl.currentPotential l u n a i w) =ᶠ[nhds z] fun (w : ProblemStatement.SpaceTime) => ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, CurrentSignedCurl.currentPotential l u n a i w

theorem NavierStokes.ActualSignedCurrentSupport.currentPressure_finsum_germ {B N0 : ℕ} (u : CorrectionState.State Point) (n : ℕ) {qbig a : ℝ} (ha : 0 < a) {i : PolarCharts.Index} {z : ProblemStatement.SpaceTime} (hz : z ∈ ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i) : (fun (w : ProblemStatement.SpaceTime) => ∑ᶠ (l : Index B N0), CurrentSignedCurl.currentPressure l u n a i w) =ᶠ[nhds z] fun (w : ProblemStatement.SpaceTime) => ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, CurrentSignedCurl.currentPressure l u n a i w

theorem NavierStokes.ActualSignedCurrentSupport.current_finsums_eq_labels {B N0 : ℕ} (u : CorrectionState.State Point) (v : CorrectionStep.CycleCoefficients (Index B N0)) (hv : v.labels = CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0) (n : ℕ) {qbig a : ℝ} {i : PolarCharts.Index} {z : ProblemStatement.SpaceTime} (hz : z ∈ ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i) : ∑ᶠ (l : Index B N0), CurrentSignedCurl.currentPotential l u n a i z = ∑ l ∈ v.labels n, CurrentSignedCurl.currentPotential l u n a i z ∧ ∑ᶠ (l : Index B N0), CurrentSignedCurl.currentPressure l u n a i z = ∑ l ∈ v.labels n, CurrentSignedCurl.currentPressure l u n a i z