RelativeError: actual low cutoff plus analytic high tail #
Positive exponential decay exponent in the Fourier trace tail estimate.
Instances For
Multiplicative constant in the Fourier trace tail estimate.
Equations
Instances For
theorem
AVenhance.Infra.Section5.RelativeError.TraceInstanceCutoff.e44_high_remainder_bound_for_combination
{g : Homogenization.Vec 2 → ℝ}
{R r A c : ℝ}
(M : ℕ)
(hR : 0 < R)
(hgeom : c * R * (A / r) ≤ R * (↑M + 1) / 1024)
(hg : ContDiff ℝ (↑⊤) g)
(hper : IsZ2Periodic g)
(hθ : IsThetaAnalytic R g)
(hscale : 1 ≤ R / 2 * (↑M + 1))
(w : List (Fin 2))
(hw : 1 ≤ w.length)
:
√(∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, orderedRealDerivative w (Ergodic.highRemainder g M) x ^ 2) ≤ e44TailConstant * ↑w.length.factorial * (e44TailConstant / R) ^ w.length * Real.exp (-c * R * (A / r)) * √(l2NormSq g)
The analytic complement has exactly the factorial/radius form required by
the scalar low/high combination, once the cutoff lies below A/r.
theorem
AVenhance.Infra.Section5.RelativeError.e44_initialTrace_of_classical_cutoff
{κ A r R B : ℝ}
(M : ℕ)
{g : Homogenization.Vec 2 → ℝ}
{u : ℝ → Homogenization.Vec 2 → ℝ}
{X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2}
(φ : ℝ → Homogenization.Vec 2 → ℝ)
(hφ : IsAdmissibleStream φ)
(hX : IsFlow (streamVel φ) X)
(hsol : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g u)
(hθ : IsThetaAnalytic R g)
(hmean : ∫ (x : Homogenization.Vec 2) in unitCube, g x = 0)
(hκ : 0 < κ)
(hκ1 : κ ≤ 1)
(hr : 0 < r)
(hR : 0 < R)
(hA : 1 ≤ A)
(hRr : r ≤ R)
(hB : 0 ≤ B)
(hDb : ∀ (t : ℝ) (x : Homogenization.Vec 2), ‖Flow.jointSpatialFDeriv (streamVel φ) t x‖ ≤ B)
(hM : 0 < M)
(hKup : 2 * Real.pi * √2 * ↑M ≤ A / r)
(hKlow : A / r ≤ 2 * Real.pi * √2 * (↑M + 1))
(hmax : max 1 B ≤ κ * (2 * Real.pi * √2 * ↑M) ^ 2)
(hTailScale : 1 ≤ R / 2 * (↑M + 1))
(hAbsorb : (√κ)⁻¹ * Real.exp (-e44TailExponent * R * (A / r)) ≤ 1)
(w : List (Fin 2))
:
Instantiate (7) for a smooth periodic classical solution. The geometric cutoff facts and the explicit exponential absorption remain named inputs.