Removal of square-root regularization in actual finite metric-energy integral inequalities.
theorem
EulerMetricRootLimit.regularized_root_tendsto
(q : ℝ)
:
Filter.Tendsto (fun (n : ℕ) => √(q + EulerNoncompactTransport.cutoffScale n ^ 2)) Filter.atTop (nhds √q)
The canonical positive regularization sequence converges at every quadratic energy value.
theorem
EulerMetricRootLimit.root_integral_limit
(Q A F : ℝ → ℝ)
(s t : ℝ)
(hst : s ≤ t)
(hQ : ContinuousOn Q (Set.Icc s t))
(hQ0 : ∀ u ∈ Set.Icc s t, 0 ≤ Q u)
(hA : MeasureTheory.IntegrableOn A (Set.Icc s t) MeasureTheory.volume)
(hF : MeasureTheory.IntegrableOn F (Set.Icc s t) MeasureTheory.volume)
(hineq : ∀ (δ : ℝ), 0 < δ → √(Q t + δ ^ 2) - √(Q s + δ ^ 2) ≤ ∫ (u : ℝ) in s..t, A u * √(Q u + δ ^ 2) + F u)
:
At fixed finite cutoff, an integrable energy inequality survives removal of the root regularization.
theorem
EulerMetricRootLimit.family_energy_integral_bound
{ι : Type u_1}
{H : Type u_2}
[Fintype ι]
[NormedAddCommGroup H]
[InnerProductSpace ℝ H]
(K : ℝ → H →L[ℝ] H)
(e : ι → ℝ → H)
(s t c ν : ℝ)
(K' : ℝ → H →L[ℝ] H)
(e' transport pressure forcing lap : ι → ℝ → H)
(B C : ℝ → ℝ)
(hst : s ≤ t)
(hc : 0 < c)
(hν : 0 ≤ ν)
(hKc : ContinuousOn K (Set.Icc s t))
(hec : ∀ (i : ι), ContinuousOn (e i) (Set.Icc s t))
(hB : ∀ u ∈ Set.Ioo s t, 0 ≤ B u)
(hC : ∀ u ∈ Set.Ioo s t, 0 ≤ C u)
(hcoercive : ∀ u ∈ Set.Icc s t, ∀ (v : H), c ^ 2 * ‖v‖ ^ 2 ≤ inner ℝ ((K u) v) v)
(hKd : ∀ u ∈ Set.Ioo s t, HasDerivAt K (K' u) u)
(hed : ∀ (i : ι), ∀ u ∈ Set.Ioo s t, HasDerivAt (e i) (e' i u) u)
(hsym : ∀ u ∈ Set.Ioo s t, ∀ (v w : H), inner ℝ ((K u) v) w = inner ℝ v ((K u) w))
(heq : ∀ (i : ι), ∀ u ∈ Set.Ioo s t, e' i u + transport i u + pressure i u = forcing i u + ν • lap i u)
(hp : ∀ (i : ι), ∀ u ∈ Set.Ioo s t, inner ℝ ((K u) (e i u)) (pressure i u) = 0)
(ht : ∀ (i : ι), ∀ u ∈ Set.Ioo s t, |inner ℝ ((K u) (e i u)) (transport i u)| ≤ B u * ‖e i u‖ ^ 2)
(hheat : ∀ (i : ι), ∀ u ∈ Set.Ioo s t, inner ℝ ((K u) (e i u)) (lap i u) ≤ C u * ‖e i u‖ ^ 2)
(hAint :
MeasureTheory.IntegrableOn (fun (u : ℝ) => (‖K' u‖ + 2 * B u + 2 * ν * C u) / (2 * c ^ 2)) (Set.Icc s t)
MeasureTheory.volume)
(hFint :
MeasureTheory.IntegrableOn (fun (u : ℝ) => ‖K u‖ / c * EulerFiniteMetricEnergy.familyNorm fun (i : ι) => forcing i u)
(Set.Icc s t) MeasureTheory.volume)
:
((EulerFiniteMetricEnergy.familyMetricNorm (K t) fun (i : ι) => e i t) - EulerFiniteMetricEnergy.familyMetricNorm (K s) fun (i : ι) => e i s) ≤ ∫ (u : ℝ) in s..t, ((‖K' u‖ + 2 * B u + 2 * ν * C u) / (2 * c ^ 2) * EulerFiniteMetricEnergy.familyMetricNorm (K u) fun (i : ι) => e i u) + ‖K u‖ / c * EulerFiniteMetricEnergy.familyNorm fun (i : ι) => forcing i u
The unregularized finite-family energy obeys an integral inequality even when the norm vanishes.