JBesovPrefactor

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

A uniform scalar envelope for the diagonal coarse Caccioppoli prefactor

The upstream coarse-grained Caccioppoli estimate keeps its exact parameter factors: at parameters s, t its prefactor is

`(C/(1-s-t))^{2+4s/(1-s-t)} * s^{-2s/(1-s-t)} * \Theta_{s,t}^{s/(1-s-t)}

• \Lambda_s * 3^{-2m}`.

In the range used by Section 3.5 of ABK26, namely the diagonal t = s with 0 < s \le 1/4, the first two factors depend only on s and on the dimension-only Caccioppoli constant C, and they are uniformly bounded there. This module proves that uniform bound, so that those two factors may be absorbed into the dimension-only constant of the manuscript display while the three displayed factors \Theta^{s/(1-2s)}, \Lambda_s and 3^{-2m} are retained verbatim.

The file is deliberately scalar-only: it neither applies nor restates the Caccioppoli estimate, and it packages none of the response or duality terms. The whole content is the scalar inequality caccioppoliScalarFactors_diag_le_jBesovEnvelope, stated over abstract reals; the second theorem is only its transcription onto the upstream prefactor.

noncomputable def Algsuperdiff.Section3.Provider.Besov.jBesovCaccioppoliEnvelope (C : ℝ) : ℝ

An explicit envelope for the two s-dependent scalar factors of the diagonal coarse Caccioppoli prefactor. It depends only on the upstream dimension-only Caccioppoli constant.

Equations

• Algsuperdiff.Section3.Provider.Besov.jBesovCaccioppoliEnvelope C = Real.exp 4 * (max 1 (2 * C)).rpow 4

theorem Algsuperdiff.Section3.Provider.Besov.jBesovCaccioppoliEnvelope_pos (C : ℝ) : 0 < jBesovCaccioppoliEnvelope C

theorem Algsuperdiff.Section3.Provider.Besov.caccioppoliScalarFactors_diag_le_jBesovEnvelope {C s : ℝ} (hC : 0 ≤ C) (hs : 0 < s) (hs_quarter : s ≤ 1 / 4) : (C / (1 - 2 * s)).rpow (2 + 4 * s / (1 - 2 * s)) * s.rpow (-(2 * s / (1 - 2 * s))) ≤ jBesovCaccioppoliEnvelope C

The scalar core. On the manuscript range 0 < s \le 1/4, the product of the two s-dependent factors of the diagonal Caccioppoli prefactor is bounded by an envelope depending only on C. The statement involves no cube, no coefficient field and no dimension.

theorem Algsuperdiff.Section3.Provider.Besov.caccioppoliPrefactor_diag_le_jBesovEnvelope {d : ℕ} (C : ℝ) (hC : 0 ≤ C) (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) {s : ℝ} (hs : 0 < s) (hs_quarter : s ≤ 1 / 4) : HCPolySupport.Book.Ch03.caccioppoliPrefactor C Q a s s ≤ jBesovCaccioppoliEnvelope C * ((HCPolySupport.Book.Ch02.ThetaRatio Q s s a).rpow (s / (1 - 2 * s)) * HCPolySupport.Book.Ch02.LambdaS Q s a * Real.rpow 3 (-2 * ↑Q.scale))

The diagonal Caccioppoli prefactor on the manuscript range. For 0 < s \le 1/4 the exact upstream prefactor at t = s is bounded by a scalar depending only on its dimension-only Caccioppoli constant, times the three factors displayed in the manuscript: the coarse ellipticity ratio raised to s/(1-2s), the coarse upper ellipticity \Lambda_s, and the scale weight 3^{-2m}.