GammaTenInteriorGeometry

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

The interior mesh refines into the interior mesh, at cost 2

ABK26, e.nablaw.oscillations, e.lower.bound.oscillations, e.recurrence.params.

What this module supplies

Closure.GammaTenInteriorFamily.exists_besovEnvelope_of_family_depth_oscillation runs the Besov envelope device on an arbitrary sub-mesh I, and asks for the per-depth input in the form

  avsum_{R in I} avsum_{R' in desc(R,i)} E[ osc_{n-i}(u)(R')^4 ]  <=  D i .

The depth-indexed endpoints of Closure.GammaTenDepthOscillation deliver instead the interior grid average at scale n - i,

  avsum_{R' in interiorMesoCubeGrid d K (n-i) (m-h-1)} E[ osc_{n-i}(u)(R')^4 ] .

Two facts connect them, and both are proved here.

• Refinement stays interior (mem_interiorMesoCubeGrid_of_mem_descendantsAtDepth). If the cell R of scale n has its enlarged window z_R + cu_{outer+1} inside cu_K, then every depth-i descendant R' has z_{R'} + cu_{outer} inside cu_K, because the site z_{R'} is a point of R and therefore within 3^n/2 of z_R, and 3^n/2 + 3^{outer}/2 <= 3^{outer+1}/2 as soon as n <= outer. So the source mesh is read at the window scale one larger than the target: interiorMesoCubeGrid d K n (m-h) refines into interiorMesoCubeGrid d K (n-i) (m-h-1), the exact carrier.

• The interior mesh is at least half the full mesh (card_mesoCubeGrid_le_two_mul_card_interiorMesoCubeGrid). This is the boundary count of LocalizationFluctuationMeshTransfer.one_sub_interior_card_ratio_le read once, under the recurrence's own large-cube gate; the resulting cardinality ratio |T| / (|I| 3^{d i}) is then below 2 at every depth, since numerator and denominator both gain the factor 3^{d i}.

The composite cubeFamilyAverage_descendantsAverage_interiorMesoCubeGrid_le is the per-depth input of the family device, at the cost 2 and no other.

Binders

Cube-index arithmetic and finite combinatorics, plus the two scale gates n <= K, n <= outer and the numerical boundary gate d 3^{g-p} <= 1/2, which Closure.GammaTenInteriorGeometry.mesh_boundary_half_of_gamma_threshold produces from LocalizationFluctuationGammaFold.exists_gamma_threshold_mesh_boundary and the large-cube gate. No smallness gate is assumed, nothing about the corrector, the coefficient field or the sample space occurs.

Scope

Internal Provider infrastructure for the Step-2 fluctuation estimate. There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.

References

• ABK26, e.nablaw.oscillations, e.lower.bound.oscillations, e.recurrence.params.

The site of a descendant is a point of the parent

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.abs_triadicCubeShift_sub_lt_of_mem_descendantsAtDepth {d : ℕ} {R R' : HCPolySupport.TriadicCube d} {i : ℕ} (hR' : R' ∈ HCPolySupport.descendantsAtDepth R i) (k : Fin d) : |HCPolySupport.triadicCubeShift R' k - HCPolySupport.triadicCubeShift R k| < 3 ^ R.scale / 2

The site of a descendant is inside the parent cube. Unconditional.

Refinement of the interior mesh

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.mem_interiorMesoCubeGrid_of_mem_descendantsAtDepth {d : ℕ} {K n outer : ℤ} {R R' : HCPolySupport.TriadicCube d} {i : ℕ} (hnK : n ≤ K) (hno : n ≤ outer) (hR : R ∈ interiorMesoCubeGrid d K n outer) (hR' : R' ∈ HCPolySupport.descendantsAtDepth R i) : R' ∈ interiorMesoCubeGrid d K (n - ↑i) (outer - 1)

The descendants of an interior cell are interior at the finer scale.

If R is a cell of the interior mesh at scale n and window scale outer + 1, then every depth-i descendant of R is a cell of the interior mesh at scale n - i and window scale outer. The window scale drops by one and nothing else moves.

only on the two scale gates n <= K and n <= outer.

The interior mesh is at least half the full mesh

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.card_mesoCubeGrid_le_two_mul_card_interiorMesoCubeGrid (d : ℕ) {K n outer : ℤ} {p g : ℕ} (hK : K = n + ↑p) (houter : outer + 1 = n + ↑g) (hgp : g ≤ p) (hsmall : ↑d * (3 ^ g / 3 ^ p) ≤ 1 / 2) : ↑(mesoCubeGrid d K n).card ≤ 2 * ↑(interiorMesoCubeGrid d K n outer).card

The interior mesh carries at least half the cells, once the boundary fraction is below 1/2.

only on the scale bookkeeping and on the numerical gate hsmall.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.card_interiorMesoCubeGrid_refined_le (d : ℕ) {K n outer : ℤ} {p g : ℕ} (i : ℕ) (hK : K = n + ↑p) (houter : outer + 1 = n + ↑g) (hgp : g ≤ p) (hsmall : ↑d * (3 ^ g / 3 ^ p) ≤ 1 / 2) : ↑(interiorMesoCubeGrid d K (n - ↑i) (outer - 1)).card ≤ 2 * (↑(interiorMesoCubeGrid d K n outer).card * (3 ^ d) ^ i)

The refined interior mesh is small compared with the source mesh. The cardinality ratio the family device pays is below 2 at every depth.

on the scale bookkeeping and the boundary gate.

The per-depth input of the family device, on the interior mesh

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeFamilyAverage_descendantsAverage_interiorMesoCubeGrid_le (d : ℕ) {K n outer : ℤ} {p g : ℕ} (i : ℕ) (hK : K = n + ↑p) (houter : outer + 1 = n + ↑g) (hgp : g ≤ p) (hno : n ≤ outer) (hsmall : ↑d * (3 ^ g / 3 ^ p) ≤ 1 / 2) (f : HCPolySupport.TriadicCube d → ℝ) (hf : ∀ R' ∈ interiorMesoCubeGrid d K (n - ↑i) (outer - 1), 0 ≤ f R') : (cubeFamilyAverage (interiorMesoCubeGrid d K n outer) fun (R : HCPolySupport.TriadicCube d) => HCPolySupport.descendantsAverage R i f) ≤ 2 * cubeFamilyAverage (interiorMesoCubeGrid d K (n - ↑i) (outer - 1)) f

The per-depth input of the interior-mesh Besov device.

The depth-i descendant average over the interior mesh at scale n is below twice the interior-grid average at scale n - i, which is the carrier of the depth-indexed endpoints of Closure.GammaTenDepthOscillation.

on the scale bookkeeping, on the boundary gate, and on the nonnegativity of the cell functional.

The boundary gate, produced

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.exists_gamma_threshold_mesh_boundary_half (d : ℕ) : ∃ (gamma0 : ℝ), 0 < gamma0 ∧ gamma0 ≤ 1 / 4 ∧ ∀ (gamma : ℝ), 0 < gamma → gamma ≤ gamma0 → ∀ (p g : ℕ), 10 ^ 10 * gamma⁻¹ ≤ ↑p - ↑g → ↑d * (3 ^ g / 3 ^ p) ≤ 1 / 2

The boundary fraction is below 1/2 once cgamma is small. The threshold is produced by LocalizationFluctuationGammaFold.exists_gamma_threshold_mesh_boundary at the absolute constant 1, and the gate consumed is the recurrence's own large-cube gate read on the mesh.