The mean inverse with the source's actual nonlocal boundary operator. The boundary lower bound is proved from the spatial hypotheses (5), not an input.

The concrete boundary lower bound used in the mean time-variational solve.

The source localization estimate for the constructed nonlocal boundary operator.

noncomputable def EulerMeanHarmonic.boundaryLocalizationC1 : ℝ

Boundary localization C1, given by 36 * (2 + 4 * weakHarmonicSmallBallConstant).

Equations

• EulerMeanHarmonic.boundaryLocalizationC1 = 36 * (2 + 4 * EulerMeanHarmonic.weakHarmonicSmallBallConstant)

noncomputable def EulerMeanHarmonic.boundaryLocalizationC2 : ℝ

Boundary localization C2, given by 4 * weakHarmonicSmallBallConstant.

Equations

• EulerMeanHarmonic.boundaryLocalizationC2 = 4 * EulerMeanHarmonic.weakHarmonicSmallBallConstant

theorem EulerMeanHarmonic.boundaryLocalizationC1_nonneg : 0 ≤ boundaryLocalizationC1

theorem EulerMeanHarmonic.boundaryLocalizationC2_nonneg : 0 ≤ boundaryLocalizationC2

theorem EulerMeanHarmonic.norm_sub_sq_le_twice_L2 (z w : ↥EulerMeanSolenoidal.L2) : ‖z - w‖ ^ 2 ≤ 2 * ‖z‖ ^ 2 + 2 * ‖w‖ ^ 2

theorem EulerMeanHarmonic.boundary_localization (χ : EulerMeanBoundary.Cutoff) (R : ℝ) (hR : 0 < R) (z : ↥EulerMeanSolenoidal.L2) (hz : z ∈ EulerMeanSolenoidal.solenoidalSpace) (hχ : ∀ x ∈ Metric.ball 0 R, χ.field x = 1) (r : ℝ) (hr : 0 ≤ r) (hrquarter : r ≤ 1 / 4) : localL2Energy (Metric.ball 0 (R * r)) z ≤ boundaryLocalizationC1 * ‖(EulerMeanBoundary.weakPotential χ) z‖ ^ 2 + boundaryLocalizationC2 * r ^ 3 * ‖z‖ ^ 2

The literal local mass estimate (8), with fixed dimensional constants.

theorem EulerMeanHarmonic.boundary_localization_form (χ : EulerMeanBoundary.Cutoff) (R : ℝ) (hR : 0 < R) (z : ↥EulerMeanSolenoidal.L2) (hz : z ∈ EulerMeanSolenoidal.solenoidalSpace) (hχ : ∀ x ∈ Metric.ball 0 R, χ.field x = 1) (r : ℝ) (hr : 0 ≤ r) (hrquarter : r ≤ 1 / 4) : localL2Energy (Metric.ball 0 (R * r)) z ≤ boundaryLocalizationC1 * inner ℝ ((EulerMeanBoundary.boundaryOperator χ) z) z + boundaryLocalizationC2 * r ^ 3 * ‖z‖ ^ 2

The same estimate directly in terms of the actual boundary quadratic form.

Integrating the source's different lower bounds inside and outside the core.

theorem EulerMeanHarmonic.localized_coefficient_lower (M : EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hM : MeasureTheory.AEStronglyMeasurable M MeasureTheory.volume) (C : NNReal) (hC : ∀ (x : EulerSmoothLimit.Space), ‖M x‖ ≤ ↑C) (s : Set EulerSmoothLimit.Space) (hs : MeasurableSet s) (Be Bc : ℝ) (hBe : 0 ≤ Be) (hext : ∀ x ∉ s, ∀ (v : EulerSmoothLimit.Space), -Be * ‖v‖ ^ 2 ≤ inner ℝ ((M x) v) v) (hcore : ∀ x ∈ s, ∀ (v : EulerSmoothLimit.Space), -Bc * ‖v‖ ^ 2 ≤ inner ℝ ((M x) v) v) (z : ↥EulerMeanSolenoidal.L2) : -Be * ‖z‖ ^ 2 - Bc * localL2Energy s z ≤ inner ℝ ((EulerLiftedPressure.coefficientOperator M hM C hC) z) z

theorem EulerMeanHarmonic.mean_boundary_lower_bound (χ : EulerMeanBoundary.Cutoff) (R : ℝ) (hR : 0 < R) (hχ : ∀ x ∈ Metric.ball 0 R, χ.field x = 1) (M : EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hM : MeasureTheory.AEStronglyMeasurable M MeasureTheory.volume) (C : NNReal) (hC : ∀ (x : EulerSmoothLimit.Space), ‖M x‖ ≤ ↑C) (Be Bc L r : ℝ) (hBe : 0 ≤ Be) (hBc : 0 ≤ Bc) (hL : boundaryLocalizationC1 * Bc ≤ L) (hr : 0 ≤ r) (hrquarter : r ≤ 1 / 4) (hext : ∀ x ∉ Metric.ball 0 (R * r), ∀ (v : EulerSmoothLimit.Space), -Be * ‖v‖ ^ 2 ≤ inner ℝ ((M x) v) v) (hcore : ∀ x ∈ Metric.ball 0 (R * r), ∀ (v : EulerSmoothLimit.Space), -Bc * ‖v‖ ^ 2 ≤ inner ℝ ((M x) v) v) (z : ↥EulerMeanSolenoidal.L2) (hz : z ∈ EulerMeanSolenoidal.solenoidalSpace) : -(Be + boundaryLocalizationC2 * Bc * r ^ 3) * ‖z‖ ^ 2 ≤ inner ℝ ((EulerLiftedPressure.coefficientOperator M hM C hC) z) z + L * inner ℝ ((EulerMeanBoundary.boundaryOperator χ) z) z

The actual localized boundary operator compensates for the core's negative gradient.

theorem EulerMeanHarmonic.scaled_mean_boundary_lower_bound (ℓ : ℝ) (hℓ : 0 < ℓ) (M : EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hM : MeasureTheory.AEStronglyMeasurable M MeasureTheory.volume) (C : NNReal) (hC : ∀ (x : EulerSmoothLimit.Space), ‖M x‖ ≤ ↑C) (Be Bc L r : ℝ) (hBe : 0 ≤ Be) (hBc : 0 ≤ Bc) (hL : boundaryLocalizationC1 * Bc ≤ L) (hr : 0 ≤ r) (hrquarter : r ≤ 1 / 4) (hext : ∀ (x : EulerSmoothLimit.Space), r ≤ ‖ℓ • x‖ → ∀ (v : EulerSmoothLimit.Space), -Be * ‖v‖ ^ 2 ≤ inner ℝ ((M x) v) v) (hcore : ∀ (x : EulerSmoothLimit.Space), ‖ℓ • x‖ < r → ∀ (v : EulerSmoothLimit.Space), -Bc * ‖v‖ ^ 2 ≤ inner ℝ ((M x) v) v) (z : ↥EulerMeanSolenoidal.L2) (hz : z ∈ EulerMeanSolenoidal.solenoidalSpace) : -(Be + boundaryLocalizationC2 * Bc * r ^ 3) * ‖z‖ ^ 2 ≤ inner ℝ ((EulerLiftedPressure.coefficientOperator M hM C hC) z) z + L * inner ℝ ((EulerMeanBoundary.boundaryOperator (EulerMeanBoundary.scaledCutoff ℓ hℓ)) z) z

The exact cutoff and physical-label core from source (7)–(8).

noncomputable def EulerMeanSourceInverse.effectiveNegativeBound (Be Bc r : ℝ) : ℝ

Effective negative bound, given by Be + boundaryLocalizationC2 * Bc * r^3.

Equations

• EulerMeanSourceInverse.effectiveNegativeBound Be Bc r = Be + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * r ^ 3

theorem EulerMeanSourceInverse.effectiveNegativeBound_nonneg (Be Bc r : ℝ) (hBe : 0 ≤ Be) (hBc : 0 ≤ Bc) (hr : 0 ≤ r) : 0 ≤ effectiveNegativeBound Be Bc r

theorem EulerMeanSourceInverse.source_smallness (T K Be Bc r : ℝ) (hsmall : K * (T ^ 2 / 2) + Be * T + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * r ^ 3 * T ≤ 1 / 2) : K * (T ^ 2 / 2) + effectiveNegativeBound Be Bc r * T ≤ 1 / 2

noncomputable def EulerMeanSourceInverse.sourceMeanSolver (T : ℝ) (hT : 0 ≤ T) (ℓ : ℝ) (hℓ : 0 < ℓ) (M : EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hM : MeasureTheory.AEStronglyMeasurable M MeasureTheory.volume) (C : NNReal) (hC : ∀ (x : EulerSmoothLimit.Space), ‖M x‖ ≤ ↑C) (Be Bc L r : ℝ) (hBe : 0 ≤ Be) (hBc : 0 ≤ Bc) (hL : EulerMeanHarmonic.boundaryLocalizationC1 * Bc ≤ L) (hr : 0 ≤ r) (hrquarter : r ≤ 1 / 4) (hext : ∀ (x : EulerSmoothLimit.Space), r ≤ ‖ℓ • x‖ → ∀ (v : EulerSmoothLimit.Space), -Be * ‖v‖ ^ 2 ≤ inner ℝ ((M x) v) v) (hcore : ∀ (x : EulerSmoothLimit.Space), ‖ℓ • x‖ < r → ∀ (v : EulerSmoothLimit.Space), -Bc * ‖v‖ ^ 2 ≤ inner ℝ ((M x) v) v) (FInv H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (K : ℝ) (hK : 0 ≤ K) (hF0 : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2) (hH : ∀ (t : ↑(Set.Icc 0 T)) (z : ↥EulerMeanSolenoidal.L2), inner ℝ ((H t) z) z ≤ K * ‖z‖ ^ 2) (hsmall : K * (T ^ 2 / 2) + Be * T + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * r ^ 3 * T ≤ 1 / 2) : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2) →L[ℝ] ↥(EulerMeanVariationalInverse.meanDerivatives T hT FInv)

This is the actual Lax–Milgram mean inverse, with spatial coercivity discharged.

Equations

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

theorem EulerMeanSourceInverse.sourceMeanSolver_norm (T : ℝ) (hT : 0 ≤ T) (ℓ : ℝ) (hℓ : 0 < ℓ) (M : EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hM : MeasureTheory.AEStronglyMeasurable M MeasureTheory.volume) (C : NNReal) (hC : ∀ (x : EulerSmoothLimit.Space), ‖M x‖ ≤ ↑C) (Be Bc L r : ℝ) (hBe : 0 ≤ Be) (hBc : 0 ≤ Bc) (hL : EulerMeanHarmonic.boundaryLocalizationC1 * Bc ≤ L) (hr : 0 ≤ r) (hrquarter : r ≤ 1 / 4) (hext : ∀ (x : EulerSmoothLimit.Space), r ≤ ‖ℓ • x‖ → ∀ (v : EulerSmoothLimit.Space), -Be * ‖v‖ ^ 2 ≤ inner ℝ ((M x) v) v) (hcore : ∀ (x : EulerSmoothLimit.Space), ‖ℓ • x‖ < r → ∀ (v : EulerSmoothLimit.Space), -Bc * ‖v‖ ^ 2 ≤ inner ℝ ((M x) v) v) (FInv H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (K : ℝ) (hK : 0 ≤ K) (hF0 : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2) (hH : ∀ (t : ↑(Set.Icc 0 T)) (z : ↥EulerMeanSolenoidal.L2), inner ℝ ((H t) z) z ≤ K * ‖z‖ ^ 2) (hsmall : K * (T ^ 2 / 2) + Be * T + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * r ^ 3 * T ≤ 1 / 2) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : ‖(sourceMeanSolver T hT ℓ hℓ M hM C hC Be Bc L r hBe hBc hL hr hrquarter hext hcore FInv H K hK hF0 hH hsmall) f‖ ≤ 2 * T * ‖f‖

theorem EulerMeanSourceInverse.sourceMeanSolver_weak (T : ℝ) (hT : 0 ≤ T) (ℓ : ℝ) (hℓ : 0 < ℓ) (M : EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hM : MeasureTheory.AEStronglyMeasurable M MeasureTheory.volume) (C : NNReal) (hC : ∀ (x : EulerSmoothLimit.Space), ‖M x‖ ≤ ↑C) (Be Bc L r : ℝ) (hBe : 0 ≤ Be) (hBc : 0 ≤ Bc) (hL : EulerMeanHarmonic.boundaryLocalizationC1 * Bc ≤ L) (hr : 0 ≤ r) (hrquarter : r ≤ 1 / 4) (hext : ∀ (x : EulerSmoothLimit.Space), r ≤ ‖ℓ • x‖ → ∀ (v : EulerSmoothLimit.Space), -Be * ‖v‖ ^ 2 ≤ inner ℝ ((M x) v) v) (hcore : ∀ (x : EulerSmoothLimit.Space), ‖ℓ • x‖ < r → ∀ (v : EulerSmoothLimit.Space), -Bc * ‖v‖ ^ 2 ≤ inner ℝ ((M x) v) v) (FInv H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (K : ℝ) (hK : 0 ≤ K) (hF0 : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2) (hH : ∀ (t : ↑(Set.Icc 0 T)) (z : ↥EulerMeanSolenoidal.L2), inner ℝ ((H t) z) z ≤ K * ‖z‖ ^ 2) (hsmall : K * (T ^ 2 / 2) + Be * T + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * r ^ 3 * T ≤ 1 / 2) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) (v : ↥(EulerMeanVariationalInverse.meanDerivatives T hT FInv)) : have u := (sourceMeanSolver T hT ℓ hℓ M hM C hC Be Bc L r hBe hBc hL hr hrquarter hext hcore FInv H K hK hF0 hH hsmall) f; inner ℝ ↑u ↑v - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((EulerMeanVariationalInverse.meanPrimitive T hT FInv) u)) ((EulerMeanVariationalInverse.meanPrimitive T hT FInv) v) + inner ℝ ((EulerLiftedPressure.coefficientOperator M hM C hC) ((EulerMeanVariationalInverse.meanTrace T hT FInv) u)) ((EulerMeanVariationalInverse.meanTrace T hT FInv) v) + L * inner ℝ ((EulerMeanBoundary.boundaryOperator (EulerMeanBoundary.scaledCutoff ℓ hℓ)) ((EulerMeanVariationalInverse.meanTrace T hT FInv) u)) ((EulerMeanVariationalInverse.meanTrace T hT FInv) v) = -inner ℝ f ((EulerMeanVariationalInverse.meanPrimitive T hT FInv) v)

The literal mean weak equation, retaining both original initial boundary terms.

theorem EulerMeanSourceInverse.existsUnique_source_mean_weak_solution (T : ℝ) (hT : 0 ≤ T) (ℓ : ℝ) (hℓ : 0 < ℓ) (M : EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hM : MeasureTheory.AEStronglyMeasurable M MeasureTheory.volume) (C : NNReal) (hC : ∀ (x : EulerSmoothLimit.Space), ‖M x‖ ≤ ↑C) (Be Bc L r : ℝ) (hBe : 0 ≤ Be) (hBc : 0 ≤ Bc) (hL : EulerMeanHarmonic.boundaryLocalizationC1 * Bc ≤ L) (hr : 0 ≤ r) (hrquarter : r ≤ 1 / 4) (hext : ∀ (x : EulerSmoothLimit.Space), r ≤ ‖ℓ • x‖ → ∀ (v : EulerSmoothLimit.Space), -Be * ‖v‖ ^ 2 ≤ inner ℝ ((M x) v) v) (hcore : ∀ (x : EulerSmoothLimit.Space), ‖ℓ • x‖ < r → ∀ (v : EulerSmoothLimit.Space), -Bc * ‖v‖ ^ 2 ≤ inner ℝ ((M x) v) v) (FInv H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (K : ℝ) (hK : 0 ≤ K) (hF0 : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2) (hH : ∀ (t : ↑(Set.Icc 0 T)) (z : ↥EulerMeanSolenoidal.L2), inner ℝ ((H t) z) z ≤ K * ‖z‖ ^ 2) (hsmall : K * (T ^ 2 / 2) + Be * T + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * r ^ 3 * T ≤ 1 / 2) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : ∃! u : ↥(EulerMeanVariationalInverse.meanDerivatives T hT FInv), ∀ (v : ↥(EulerMeanVariationalInverse.meanDerivatives T hT FInv)), inner ℝ ↑u ↑v - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((EulerMeanVariationalInverse.meanPrimitive T hT FInv) u)) ((EulerMeanVariationalInverse.meanPrimitive T hT FInv) v) + inner ℝ ((EulerLiftedPressure.coefficientOperator M hM C hC) ((EulerMeanVariationalInverse.meanTrace T hT FInv) u)) ((EulerMeanVariationalInverse.meanTrace T hT FInv) v) + L * inner ℝ ((EulerMeanBoundary.boundaryOperator (EulerMeanBoundary.scaledCutoff ℓ hℓ)) ((EulerMeanVariationalInverse.meanTrace T hT FInv) u)) ((EulerMeanVariationalInverse.meanTrace T hT FInv) v) = -inner ℝ f ((EulerMeanVariationalInverse.meanPrimitive T hT FInv) v)

Existence and uniqueness from the actual source spatial and time assumptions.