HomFinitePSource #

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

the general coarse-graining proposition at finite `p`: the printed vocabulary #

THE CONDITIONAL EDGE — `hCG'`, transcribed, NOT proved here #

The general coarse-graining proposition is a declared dependency and a declared source hypothesis of the Step-3a node of Theorem B. It is a hypothesis of this tree, exactly as hCG and hC are entered elsewhere in it. Nothing below proves it; this file transcribes the vocabulary of its printed display — the energy slot, the right-hand side and the geometric factor — and every consumer carries the display itself as an explicit binder.

This file replaces the hCG hypothesis (the p → ∞ reading) by the printed finite-p proposition:

Let m,n ∈ ℤ with n < m, 𝐚: □_m → ℝ^{d×d}_+ uniformly elliptic and σ₀ ∈ (0,∞). Fix p ∈ [2,∞) and s, s₁, s₂ ∈ (0,1) with s₁ < s < s₂ < 1. There is C(p,d) < ∞ such that for every 𝐠 ∈ W^{s₂,p}(□_m;ℝ^d) and every pair u, v ∈ H¹(□_m) with -∇·𝐚∇u = ∇·𝐠, -∇·σ₀∇v = ∇·𝐠 in □_m and u - v ∈ H¹₀(□_m),
  3^{-ms} σ₀ ‖∇u - ∇v‖_{W_hat^{-s,p}(□_m)} + 3^{-ms} ‖𝐚∇u - σ₀∇v‖_{W_hat^{-s,p}(□_m)}
    ≤ C s^{-1} σ₀^{1/2} 𝓔_{s₁,∞,1}(□_m,n;𝐚,σ₀)
        ( Σ_{k ≤ n} 3^{-(s-s₁)p(n-k)} avsum_{z ∈ 3^k ℤ^d ∩ □_m}
             ‖σ^{1/2}∇u‖_{L²(z+□_k)}^p )^{1/p}
      + C s^{-9/2} (s₂-s)^{-1} (1 + 𝓔²_{s₁/2,∞,2}(□_m,n;𝐚,σ₀))
          3^{s₂ n} [𝐠]_{W^{s₂,p}(□_m)}.

No extension, no p-limit and no correction is used: p = 4d is inside the printed range [2,∞), and C(p,d) is the printed constant.

Which parts are pinned, and which are carried abstractly #

Following the established conditional-edge device, the objects this file does not consume are carried as abstract reals: the coefficient field, the two 𝓔 quantities (E1, E2), the forcing seminorm (Dg), the constant (Ccg) and the elliptic pair itself. Two things ARE pinned, because they are consumed:

the energy slot — the printed ℓ^p sum over the printed grid, at coarseGrainingEnergyPartial: the grid of the sum is the pure lattice 3^k ℤ^d ∩ □_m, i.e. CoarseGraining's descendantsAtDepth, and the outer index is a partial sum (no summability side hypothesis);
the left-hand negative norms, at BOTH readings — see next.

TWO READINGS, both transcribed #

The manuscript never defines ‖·‖_{W_hat^{-s,p}(□_m)} (the manuscript defines only the order -1 duals). The correction records — machine-checked — that the two consumption sites need inequivalent objects:

Step 3c (the L^∞ upgrade) needs the multiscale reading: a single-scale duality bound loses r^{-d};
Step 4 (the pairing) needs the duality reading: pairing a Hölder test field against the multiscale depth maxima diverges logarithmically over the triadic depths.

Neither implies the other. An honest transcription of ONE printed display whose symbol is undefined therefore has to carry both readings of that display: a multiscale clause, at the finite-p grid carrier of HomFinitePGauge, and two duality clauses, at the WeakNegDualBoundOn levels. No clause is derived from another anywhere in this tree, and the disclosure travels with every consumer.

Main definitions and results #

coarseGrainingEnergyPartial — the printed ℓ^p mesoscale energy slot;
coarseGrainingFinitePRHS — the printed right-hand side;
coarseGrainingGeomFactor — the geometric factor (1 - 3^{-wp})^{-1/p} the energy slot is summed against, with the elementary ℓ^p geometric-sum bounds it needs.

1. The printed `ℓ^p` mesoscale energy slot #

source

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.coarseGrainingEnergyPartial {d : ℕ} (Q : HCPolySupport.TriadicCube d) (p w : ℝ) (jn N : ℕ) (Gen : HCPolySupport.TriadicCube d → ℝ) :

ℝ

The printed energy slot, as a partial sum.

With k = n - i and the mesoscale depth jn = m - n, the printed Σ_{k ≤ n} 3^{-(s-s₁)p(n-k)} avsum_{z ∈ 3^k ℤ^d ∩ □_m} G(z+□_k)^p becomes a sum over i ≥ 0 of 3^{-(w p) i} times the depth-(jn + i) grid average of G^p, where w = s - s₁. The grid is the printed one: the pure lattice, i.e. CoarseGraining's descendantsAtDepth.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Algsuperdiff.Section4.Provider.Homogenization.coarseGrainingEnergyPartial_def {d : ℕ} (Q : HCPolySupport.TriadicCube d) (p w : ℝ) (jn N : ℕ) (Gen : HCPolySupport.TriadicCube d → ℝ) :

coarseGrainingEnergyPartial Q p w jn N Gen = (∑ i ∈ Finset.range (N + 1), 3 ^ (-(w * p) * ↑i) * HCPolySupport.descendantsAverage Q (jn + i) fun (R : HCPolySupport.TriadicCube d) => Gen R ^ p) ^ (1 / p)

source

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.coarseGrainingFinitePRHS (Ccg s s2 sigma E1 E2 Dg S : ℝ) (n : ℤ) :

ℝ

The printed right-hand side, with the energy slot supplied as the abstract upper bound S.

Every factor is the printed one: C s^{-1} σ₀^{1/2} 𝓔₁ · S and C s^{-9/2} (s₂-s)^{-1} (1 + 𝓔₂²) · 3^{s₂ n} [𝐠].

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Algsuperdiff.Section4.Provider.Homogenization.coarseGrainingFinitePRHS_def (Ccg s s2 sigma E1 E2 Dg S : ℝ) (n : ℤ) :

coarseGrainingFinitePRHS Ccg s s2 sigma E1 E2 Dg S n = Ccg * s⁻¹ * √sigma * E1 * S + Ccg * s ^ (-(9 / 2)) * (s2 - s)⁻¹ * (1 + E2 ^ 2) * (3 ^ (s2 * ↑n) * Dg)