Related estimates used together by the same construction modules.

Weighted removal of root regularization, preserving the signed derivative of the radius.

theorem EulerWeightedRootLimit.regularized_integral_tendsto (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) : Filter.Tendsto (fun (n : ℕ) => ∫ (u : ℝ) in s..t, A u * √(Q u + EulerNoncompactTransport.cutoffScale n ^ 2) + F u) Filter.atTop (nhds (∫ (u : ℝ) in s..t, A u * √(Q u) + F u))

Dominated convergence for the regularized scalar energy integrand on a fixed finite interval.

theorem EulerWeightedRootLimit.weighted_root_integral_limit (Q A F w : ℝ → ℝ) (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 < δ → w t * √(Q t + δ ^ 2) - w s * √(Q s + δ ^ 2) ≤ ∫ (u : ℝ) in s..t, A u * √(Q u + δ ^ 2) + F u) : w t * √(Q t) - w s * √(Q s) ≤ ∫ (u : ℝ) in s..t, A u * √(Q u) + F u

Endpoint weights pass through the same genuine regularization limit.

theorem EulerWeightedRootLimit.weighted_root_integral_of_deriv_bound (Q a F w w' : ℝ → ℝ) (s t : ℝ) (hst : s ≤ t) (hQ : ContinuousOn Q (Set.Icc s t)) (hQ0 : ∀ u ∈ Set.Icc s t, 0 ≤ Q u) (hwc : ContinuousOn w (Set.Icc s t)) (hw : ∀ u ∈ Set.Ioo s t, 0 ≤ w u) (hwd : ∀ u ∈ Set.Ioo s t, HasDerivAt w (w' u) u) (hregd : ∀ (δ : ℝ), 0 < δ → ∀ u ∈ Set.Ioo s t, DifferentiableAt ℝ (fun (v : ℝ) => √(Q v + δ ^ 2)) u) (hreg : ∀ (δ : ℝ), 0 < δ → ∀ u ∈ Set.Ioo s t, deriv (fun (v : ℝ) => √(Q v + δ ^ 2)) u ≤ a u * √(Q u + δ ^ 2) + F u) (hA : MeasureTheory.IntegrableOn (fun (u : ℝ) => w u * a u + w' u) (Set.Icc s t) MeasureTheory.volume) (hF : MeasureTheory.IntegrableOn (fun (u : ℝ) => w u * F u) (Set.Icc s t) MeasureTheory.volume) : w t * √(Q t) - w s * √(Q s) ≤ ∫ (u : ℝ) in s..t, (w u * a u + w' u) * √(Q u) + w u * F u

A nonnegative differentiable weight preserves an energy differential bound with its signed derivative.

Weighted Energy

theorem EulerWeightedEnergy.weight_hasDerivAt (ρ : ℝ → ℝ) (ρ' t : ℝ) (hρ : HasDerivAt ρ ρ' t) (hpos : 0 < ρ t) (n : ℕ) : HasDerivAt (fun (s : ℝ) => EulerPacketWeights.weight (ρ s) n) (ρ' / ρ t * ↑n * EulerPacketWeights.weight (ρ t) n) t

theorem EulerWeightedEnergy.finite_weighted_energy_hasDerivAt (ρ : ℝ → ℝ) (ρ' t : ℝ) (hρ : HasDerivAt ρ ρ' t) (hpos : 0 < ρ t) (E : ℕ → ℝ → ℝ) (E' : ℕ → ℝ) (N : ℕ) (hE : ∀ n ∈ Finset.range (N + 1), HasDerivAt (E n) (E' n) t) : HasDerivAt (fun (s : ℝ) => ∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight (ρ s) n * E n s) (∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight (ρ t) n * E' n + ρ' / ρ t * ∑ n ∈ Finset.range (N + 1), ↑n * EulerPacketWeights.weight (ρ t) n * E n t) t

Exact differentiation of the finite weighted Gevrey energy, including radius loss.