CubeJensen

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

Binder descriptions below are an informal inventory only, NOT a source certification; certification vocabulary is reserved for frozen source-facing declarations.

Portable: cube-average Jensen at the fourth and eighth powers

This file contains generic mathematics only. It imports nothing but Mathlib and Homogenization.*, mentions no ABK26 object, and is a candidate for relocation into CoarseGraining beside the p = 2 statements it consumes.

What is here, and what was already upstream

CoarseGraining already proves the scalar p = 2 normalized cube-average Jensen inequality, Homogenization.sq_cubeAverage_le_cubeAverage_sq_of_memLp:

  (cubeAverage Q f)^2 <= cubeAverage Q (f^2)   for f in L^2(normalizedCubeMeasure Q),

together with its coordinatewise vector consequence vecNormSq_cubeAverageVec_le_sum_cubeAverage_sq_of_memLp. What is not upstream, and is supplied here, is the higher-power form needed whenever a volume-normalized L^4 quantity has to be compared with a volume-normalized L^8 quantity on the same cube:

• sq_cubeAverage_pow_four_le_cubeAverage_pow_eight_of_memLp -- the volume-normalized L^4 <= L^8 comparison, in the form (cubeAverage Q (f^4))^2 <= cubeAverage Q (f^8).

It is the same convexity fact, the p = 2 statement applied to f^4. The membership bookkeeping (f in L^8 implies f^4 in L^2 on the normalized cube, a finite measure) is done once in the private helper below.

Note on hypotheses

The statement carries exactly the membership its own proof needs and nothing more, MemLp f 8. The normalized cube measure is finite, so the weaker memberships used inside are derived, not assumed.

Main results

• sq_cubeAverage_pow_four_le_cubeAverage_pow_eight_of_memLp

Membership bookkeeping on the normalized cube

The volume-normalized L^4 <= L^8 comparison

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.sq_cubeAverage_pow_four_le_cubeAverage_pow_eight_of_memLp {d : ℕ} (Q : HCPolySupport.TriadicCube d) (f : HCPolySupport.Vec d → ℝ) (hf : MeasureTheory.MemLp f 8 (HCPolySupport.normalizedCubeMeasure Q)) : (HCPolySupport.cubeAverage Q fun (x : HCPolySupport.Vec d) => f x ^ 4) ^ 2 ≤ HCPolySupport.cubeAverage Q fun (x : HCPolySupport.Vec d) => f x ^ 8

The volume-normalized L^4 <= L^8 comparison on a triadic cube. Equivalently (avg (f^4))^{1/4} <= (avg (f^8))^{1/8}: on a normalized (hence probability) cube measure the L^4 average never exceeds the L^8 one.