Common source-scale target and scalar L²-to-HDot⁻¹ transfer.
The scale inputs in the term files are estimates on spatial L² quantities. They do not assume the desired negative-norm estimate.
noncomputable def
AVenhance.Infra.Section5.section5SourceScale
(β : ℝ)
(Λ m : ℕ)
(κm C : ℝ)
(θ₀ : Homogenization.Vec 2 → ℝ)
:
The requested Section 5 source scale, with the physical coefficient bounds left as explicit hypotheses in each term-specific estimate.
Equations
- AVenhance.Infra.Section5.section5SourceScale β Λ m κm C θ₀ = C * AVenhance.epsilon β Λ (m - 1) ^ AVenhance.delta β * √κm * √(AVenhance.l2NormSq θ₀)
Instances For
theorem
AVenhance.Infra.Section5.timeHMinusOneNorm_le_L2_of_sourceScale
{f : ℝ → Homogenization.Vec 2 → ℝ}
{S : ℝ}
(hL2 : ∀ t ∈ Set.Ioo 0 1, Homogenization.MemL2On unitCube (f t))
(hmean : ∀ t ∈ Set.Ioo 0 1, Homogenization.MeanZeroOn unitCube (f t))
(hscale :
(∫⁻ (t : ℝ) in Set.Ioo 0 1, ENNReal.ofReal ((2 * Real.pi)⁻¹ * √(l2NormSq (f t))) ^ 2) ^ (1 / 2) ≤ ENNReal.ofReal S)
:
Transfer a source-scale estimate on the spatial L² norms of a mean-zero scalar term to the exact time-integrated HDot⁻¹ norm.