Ball comparability transfers from locally integrable to L² functions

-- Generated by skeleton subtraction from QuadraticFormsSobolev/Section32.lean
-- source: quadratic-forms-sobolev@cc13121ff7b6
import Definitions.Def_QFS_Translate
import Definitions.Def_QFS_Defs
import Definitions.Def_QFS_ConeGap
import Definitions.Def_QFS_RefCones
import Definitions.Def_QFS_Section4
import Definitions.Def_QFS_Cubes
import Definitions.Def_QFS_Section3
import Definitions.Def_QFS_Section5
import Definitions.Def_QFS_Section1
import Definitions.Def_QFS_ThinCones
import Definitions.Def_QFS_Section3Kernel
import Definitions.Def_QFS_LebesgueDiff
import Definitions.Def_QFS_LebesgueDiff2
import Definitions.Def_QFS_Renormalization
import Definitions.Def_QFS_FirstJump
import Definitions.Def_QFS_Assembly
import Definitions.Def_QFS_PathAssembly
import Definitions.Def_QFS_BlockPaths
import Definitions.Def_QFS_Section6
import Definitions.Def_QFS_Rescaling
import Definitions.Def_QFS_Section32
import Definitions.Def_QFS_FavoredGraph
import Definitions.Def_QFS_Indicator
import Definitions.Def_QFS_FunctionSpaces
import Mathlib

set_option autoImplicit true
set_option relaxedAutoImplicit false
set_option maxSynthPendingDepth 3

/-!
# The limit procedure of Section 3.2

Section 3.2 passes from the discrete inequality `(15)` to the continuous
one by letting `h → 0`. On the left it uses Fatou. On the right it asserts

> For the right hand side in (15) this implies with help of dominated
> convergence … `∫ g_h → ∫ g`

without exhibiting a dominating function, and none is available unconditionally
(see the README).

This file carries out the whole procedure, supplying the missing ingredient
along the way.

**The dominant.** A *varying* dominant suffices, and the tile-averaging operator
provides one. For a function of a pair it is `tileAvg₂`: an averaging
(conditional expectation) operator, so it **preserves the integral exactly**
(`lintegral_tileAvg₂`), and it converges almost everywhere by Lemma A.2 on the
product space (`tendsto_tileAvg₂`). Jensen's inequality for the step function
(`ofReal_sq_cubeAvg_sub_le`) and the comparability of the jump kernel across a
well-separated pair of tiles (`jumpKernel_le_of_mem_cubes`) show that it
dominates the paper's `g_h` up to the constant `Λ2^{d+α}`
(`stepG_le_tileAvg₂`). With `limsup_lintegral_le_of_dominant` — the generalized
(Vitali) form of dominated convergence, in which the dominants are allowed to
move — this justifies the paper's step for every `f` lying in `H^{α/2}` of the
enlarged ball (`limsup_lintegral_stepG_le`).

**The rest of the procedure.** `(15)` becomes an inequality between
integrals (`discret_lintegral`); the left-hand integrand converges almost
everywhere (`tendsto_discreteC_jump_ae`) so Fatou applies
(`formHs_ball_le_liminf`); the right-hand one is the integral of `g_h`
(`lintegral_stepG_eq`), whose limit the dominant controls. The assembly is
`formHs_ball_le_form_of_formHs_ne_top`: Lemma 3.7's enlarged-ball form, with
`κ` and `c` depending only on `ϑ`, `Λ` and `α`.

The one hypothesis that remains is that `f` already lie in `H^{α/2}` of the
enlarged ball — exactly what the paper's dominated-convergence step needs and
does not supply. See the README for why the natural routes to removing it are
circular, and `BeyondThePaper.lean` for its proof in dimension two.
-/

open MeasureTheory Filter Set Metric
open scoped ENNReal NNReal Topology

open QFS

variable {d : ℕ}

/-! ## The tile-averaging operator -/

/-! ## Dominated convergence with a moving dominant -/

/-! ## Why the Lipschitz reduction is circular

The natural way to supply the a priori hypothesis is to mollify: `f_ε = f * ρ_ε`
is smooth, hence Lipschitz on a ball, hence in `H^{α/2}`, so the dominated
convergence step above applies to it. What the reduction then needs is that
mollification does not inflate the right-hand side, `|f_ε|_{H_k(B*)} ≲
|f|_{H_k(B**)}`.

That is *not* false — but it is not available either, because `k` is neither
translation invariant nor bounded below off the cone set `E`, and the only route
to it runs through Theorem 1.1 itself. The theorem below makes the circularity
precise: **granted Theorem 1.1, any approximation bounded on `H^{α/2}` is
automatically bounded on `H_k`.** So the hypothesis the reduction would need is a
consequence of the statement it is meant to prove. -/

/-! ## Lipschitz functions satisfy the a priori hypothesis

This is the half of the Lipschitz reduction that does work: a Lipschitz function
lies in `H^{α/2}` of a ball whenever `α < 2`, because
`(f(s) − f(t))²|s − t|^{-d-α} ≤ L²|s − t|^{2-d-α}` and the exponent `2 − d − α`
exceeds `−d`. So mollification does supply the a priori hypothesis of the
dominated-convergence step above; what it does not supply is the bound on the
right-hand side, for the reason recorded in `form_le_of_theoremOneOneBall`. -/

/-! ## Reducing the open statement to a modulus of continuity

The obstruction in §3.2 is the a priori hypothesis `f ∈ H^{α/2}(B*)`. It can be
weakened substantially, and the weakening is worth recording because it replaces
a singular double integral by a quantity with no singularity at all.

Decompose the difference of two cube averages as
`f_h(x) − f_h(y) = (f_h(x) − f(s)) + (f(s) − f(t)) + (f(t) − f_h(y))`, multiply by
`k(s,t)` and integrate over `Ã_h(x) × Ã_h(y)`. Summing over the pairs, the middle
term contributes `|f|²_{H_k(B*)}`, and each outer term contributes
`‖f − E_h f‖²_{L²(B*)}` times `sup_s ∫_{|s−t| > h/2} k(s,t) dt = O(Λ h^{-α})`:

  `∫∫ g_h ≤ 9 |f|²_{H_k(B*)} + C(d,α,Λ) · A_h`,   `A_h := h^{-α}‖f − E_h f‖²_{L²(B*)}`.

Fatou on the left of `(15)` then gives `|f|_{H^{α/2}(B)} < ∞` as soon as
`liminf_{h→0} A_h < ∞` — no dominated convergence and no limit on the right at
all. So:

> **It suffices that `liminf_{h→0} h^{-α}‖f − E_h f‖²_{L²(B*)} < ∞`.**

`A_h` is an `L²` modulus of continuity at a single scale — a Besov `B^{α/2}_{2,∞}`
quantity, strictly weaker than the `B^{α/2}_{2,2} = H^{α/2}` membership the paper's
argument assumes.

And `A_h` splits into a cone part and an off-cone part, of which **the cone part
is already bounded, uniformly in `h`** — that is `oscillation_same_tile_le_form`
below. The residual is the off-cone oscillation inside single tiles: for `s,t` in
one cube of side `h` with `t ∉ V^Γ[s]`, the difference `f(s) − f(t)` must be
recovered by chaining through cone pairs. That is exactly what §§4–6 do, but in
the discrete setting, where the tiles are points and the within-tile oscillation
is invisible. -/

/-! ## A Lipschitz cutoff

The standard radial cutoff, with the one estimate the jump kernel needs:
`(χ(x) − χ(y))² ≤ min (‖x−y‖²/δ², 1)`, which is exactly the factor
`lintegral_cutoff_kernel_lt_top` integrates. -/

/-! ## The cutoff estimate, pointwise

Multiplying by the cutoff costs two things: the oscillation of `f` on the outer
ball, and an `L²` term weighted by the cutoff factor. The point of the case
analysis below is that **neither ever sees `f` outside the outer ball** — where
one endpoint escapes, the cutoff vanishes there and the surviving term is
`χ(x)² f(x)²` with `x` inside, and `χ(x)² = (χ(x) − χ(y))²` is again bounded by
the cutoff factor. That is what makes the zero-extension legitimate here, where
a sharp cutoff would fail. -/
/-! ## The tiling of pairs

§3.2's `(15)` is an inequality between sums over pairs of lattice points,
and the limit acts on integrals. The bridge is the product tiling: `ℝ^d × ℝ^d`
is tiled by the products `Ã_h(x) × Ã_h(y)`, so a function constant on each such
product integrates to the corresponding sum times `h^{2d}`. -/

/-! ## The discrete form as an integral

Corollary 3.1 states `(15)` as an inequality between sums over pairs of
lattice points; the limit `h → 0` acts on integrals. This section converts the
one into the other. The intermediary is the summand extended by zero to all of
`ℝ^d × ℝ^d`: both the subtype sum of `discreteFormOn` and the sum over the
tiling's index set `(Fin d → ℤ)²` equal that total sum, because in each case the
summand vanishes off the relevant set. -/

/-! ## The step index converges to the identity

Everything in the limit `h → 0` rests on the tiling shrinking to points. -/

/-! ## The left-hand integrand converges

Fatou needs only a lower bound on the limit inferior, and the limit itself is
available wherever the two coordinates are interior to the ball, distinct, and
Lebesgue points — a set of full measure. Outside the ball the bound is trivial,
so the boundary never has to be discussed. -/

/-! ## Measurability of the discretized integrands

Fatou's lemma and the dominated convergence theorem both want the functions
they are applied to to be measurable.  A function of the two lattice indices
is measurable for a soft reason, whatever it does on the lattice: it is
constant on each product cube of the tiling, and the tiling is countable. -/

/-! ## Off the ball the discretized integrand vanishes

The remaining half of the convergence: at a point strictly outside the closed
ball, the lattice point is eventually outside the ball too, so the constraint
of the discrete form fails and the integrand is eventually zero.  The sphere,
where neither argument applies, is a null set. -/

/-! ## Fatou on the left-hand side

The `H^{α/2}` form of the ball is at most the limit inferior of the
discretized forms of the step functions.  This is the first half of the
passage to the limit in Section 3.2. -/

/-! ## The tile average of a function of a pair

The dominant Section 3.2 needs is the tile average of the `H^{α/2}` integrand,
a function of a *pair*.  It has the two properties the generalized dominated
convergence theorem asks of a moving dominant: its integral does not depend on
`h` (`lintegral_tileAvg₂`), and it converges almost everywhere to the function
it averages (`tendsto_tileAvg₂`), by Lemma A.2 on the product. -/

/-! ## Jensen's inequality for the step function

The step function is an average, so the square of a difference of its values is
at most the average of the squares of the differences.  That is what makes the
tile average a dominant for the discretized integrand. -/

/-! ## The jump kernel is comparable on tiles

Away from the diagonal the jump kernel varies by a bounded factor over a pair
of tiles.  Taking the separation parameter `R₀ = 3√d` rather than the `√d` of
Corollary 3.6 -- which only strengthens the constraint, so the corollary still
applies -- makes the factor `2^{d+α}`. -/

/-! ## The dominant

Putting Jensen and the tile comparability of the kernel together: the
discretized integrand of the right-hand side of `(15)`, with the kernel `k`
itself rather than its lattice average, is dominated by a constant multiple of
the tile average of the `H^{α/2}` integrand of a slightly larger ball. -/

/-! ## The right-hand side of `(15)` as an integral

The paper's identity: the sum on the right of `(15)`, whose kernel is the
lattice average `ω^k_h`, is the integral of `g_h`, whose kernel is `k` itself.
The two differ only by which representative of the tile one integrates. -/

/-! ## Dominated convergence on the right

Everything is now in place: `stepG_le_tileAvg₂` dominates, `lintegral_tileAvg₂`
keeps the integral of the dominant constant, `tendsto_tileAvg₂` and
`tendsto_stepG_ae` supply the two convergences, and the finiteness of the
`H^{α/2}` form of the larger ball makes the dominant integrable. -/

/-! ## Corollary 3.6, packaged as assumption (4)

`cor_rescaled_kernel` gives the two bounds on `ω^k_h` for pairs separated by
more than `√d h`; `(15)` consumes them as a `DiscreteKernelBounds`, which
also asks for symmetry and for a constant at least one. -/

/-! ## Lemma 3.7 on a ball

The assembly of Section 3.2: Fatou on the left, `(15)` in the middle,
dominated convergence with the moving dominant on the right.  The one
hypothesis the paper does not state is the finiteness of the `H^{α/2}` form of
the larger ball, which is what its own appeal to dominated convergence needs;
see the README. -/

/-! ## Theorem 1.1's ball form, with the hypotheses this formalisation carries

`QFS.TheoremOneOneBall` is the paper's statement.  Two of its hypotheses are not
the ones available here: the paper's condition (M) is used through Debreu's
theorem, which is carried as `CondMeas`, and the kernel is assumed measurable,
which the paper leaves implicit.  This variant records exactly what §3.2's
argument proves. -/

theorem QFS.ballComparability_of_measurable {α c κ : ℝ} (hκ : 1 ≤ κ)
    {k : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d) → ℝ≥0∞}
    {x₀ : EuclideanSpace ℝ (Fin d)} {R : ℝ} (hR : 0 < R)
    (H : ∀ f : EuclideanSpace ℝ (Fin d) → ℝ, Measurable f → LocallyIntegrable f volume →
      (∫⁻ x in ball x₀ (κ * R), ENNReal.ofReal (f x ^ 2)) ≠ ⊤ →
      formHs (ball x₀ R) α f ≤ ENNReal.ofReal c * form (ball x₀ (κ * R)) k f)
    (f : EuclideanSpace ℝ (Fin d) → ℝ)
    (hf : MemLp f 2 (volume.restrict (ball x₀ (κ * R)))) :
    formHs (ball x₀ R) α f ≤ ENNReal.ofReal c * form (ball x₀ (κ * R)) k f := by sorry


/-! ## The scaling of the kernel's tail

`∫_{|z| > r} |z|^{-d-α} dz = r^{-α} ∫_{|z| > 1} |z|^{-d-α} dz`, by the dilation
`z ↦ rz`. With `lintegral_compl_ball_rpow_lt_top` at `r = 1` this turns the
qualitative finiteness into the quantitative `O(r^{-α})` that a splitting
argument needs. -/

/-! ## The splitting route

An alternative to the dominant: split
`f_h(x) − f_h(y) = (f_h(x) − f(s)) + (f(s) − f(t)) + (f(t) − f_h(y))`. The middle
term contributes the `H_k` form; the two outer ones contribute the tile
oscillation of `f`, weighted by the mass of the kernel at distance more than
`2√d h`, which `lintegral_jumpKernel_far` prices at `C h^{-α}`. Fatou on the
left of `(15)` then needs only `liminf_h h^{-α}‖f − E_h f‖²_{L²} < ∞`,
which is weaker than membership of `H^{α/2}`; see the README. -/