Cutoff error estimate, indicator on the second variable

-- Generated by skeleton subtraction from QuadraticFormsSobolev/Section32.lean
-- source: quadratic-forms-sobolev@7a1a680db212
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 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. -/

theorem QFS.lintegral_cutoff_error_le_prime {Γ : Configuration (EuclideanSpace ℝ (Fin d))}
    {α Λ : ℝ} {k : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d) → ℝ≥0∞}
    (hk : KernelBounds Γ α Λ k) (hd : 0 < d) {δ : ℝ} (hδ : 0 < δ)
    (hα : 0 < α) (hα2 : α < 2)
    {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : Measurable f)
    (hkm : Measurable fun p : EuclideanSpace ℝ (Fin d) × EuclideanSpace ℝ (Fin d) =>
      k p.1 p.2)
    (S : Set (EuclideanSpace ℝ (Fin d))) (hSm : MeasurableSet S) :
    ∫⁻ p : EuclideanSpace ℝ (Fin d) × EuclideanSpace ℝ (Fin d),
        ENNReal.ofReal (S.indicator (fun z => f z ^ 2) p.2 *
          min (‖p.1 - p.2‖ ^ 2 / δ ^ 2) 1) * k p.1 p.2
      ≤ ENNReal.ofReal Λ *
          (∫⁻ u : EuclideanSpace ℝ (Fin d),
            ENNReal.ofReal (min (‖u‖ ^ 2 / δ ^ 2) 1 * ‖u‖ ^ (-(d : ℝ) - α))) *
          ∫⁻ x in S, ENNReal.ofReal (f x ^ 2) := by sorry