Measurability of an integral over the moving averaging ball

-- Generated by skeleton subtraction from QuadraticFormsSobolev/BeyondThePaper.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 Definitions.Def_QFS_AppendixA
import Definitions.Def_QFS_BeyondThePaper
import Mathlib

set_option autoImplicit true
set_option relaxedAutoImplicit false
set_option maxSynthPendingDepth 3

/-!
# Beyond the paper — new mathematics, not a formalisation of Bux–Kassmann–Schulze

**Everything in this file is outside the scope of the paper being certified.**
None of it appears in arXiv:1707.09277, in any form: not the statements, not the
constants, not the proofs. It is an attempt to close the one gap the
formalisation of that paper leaves open, and it should be read as new (and
incomplete) research rather than as a record of what the authors wrote. No
mathematics elsewhere in this repository depends on this file: deleting it, and
its line in the root module, would leave the certification of the paper
intact.

## The problem

Section 3.2's dominated-convergence step needs an a priori hypothesis its own
argument never establishes: that `f ∈ H_k(B*)` already lies in `H^{α/2}(B*)`.
The formalisation of that step (`QFS.limsup_lintegral_stepG_le`) and of the
whole of §3.2 (`QFS.formHs_ball_le_form_of_formHs_ne_top`) carries the
hypothesis explicitly. This file discharges it in dimension two, in several
regimes in every dimension, and reduces it in general to one integrability
condition.

## What this file proves

The route is a local Poincaré inequality: for two points `s`, `t`,

  (★)  `(f(s) − f(t))²` is recovered by chaining through intermediate points
       that *do* see the relevant cones, averaged over a positive-measure set of
       such points,

which converts the cone-restricted energy into the full fractional energy.
`exists_ball_in_two_cones` is its geometric heart: for two distinct points
sharing a cone direction it supplies a **ball** of intermediate points lying in
both cones — a positive-measure strengthening of the paper's Lemma 4.3, which
produces a single point. In the plane the same is true without a shared
direction (`mem_two_cones_of_mem_planarBall`), because two non-parallel lines
meet; that is what closes dimension two, and `no_common_neighbour_of_skew_axes`
proves that *this* construction cannot be pushed to dimension three.

Stripped of hypotheses, what the chaining gives is one inequality
(`lintegral_visibility_le`): for every configuration satisfying the standing
assumptions — the kernel bounds (2) and condition (M) — the `H^{α/2}` energy of
a pair, weighted by how much of its averaging ball can see both endpoints, is at
most `C·|f|²_{H_k}`. Everything else here exhibits sets of pairs on which that
weight is bounded below:

* **dimension two**: `sobolevInclusion_planar`, `formHs_ball_ne_top_of_planar`,
  `formHs_ball_le_form_planar`, `theoremOneOneBallCondMeas_two`,
  `formHs_le_form_planar`, `Hk_ball_eq_Hs_ball_planar`,
  `formHs_univ_le_form_univ_planar`, `Hk_univ_eq_Hs_univ_planar`,
  `Hk_domain_eq_Hs_domain_planar` — Theorems 1.1 and 1.4 in the plane, granted
  the Whitney/Dyda input Lemma A.1 quotes;
* **dimension one**: `formHs_le_form_dim_one`, where every cone is `ℝ ∖ {0}`;
* **small axis spread** — the cone axes at most `γ` apart as lines with
  `γ < 2ϑ`: `sobolevInclusion_of_axisSpread` and the chain behind it
  (`formHs_ball_le_form_spread`, `Hk_univ_eq_Hs_univ_spread`,
  `Hk_domain_eq_Hs_domain_spread`). **Wide cones** (apex above `π/4`) are the
  case `γ = π/2`, and `sobolevInclusion_wide` is now derived from it;
* **pairwise overlapping cone types**: `sobolevInclusion_of_overlapping`, with
  `exists_narrow_overlapping_cones_without_common_direction` showing that this
  is strictly weaker than a common direction;
* **a densely visible type**, and its exact reach:
  `formHs_le_form_of_visibleDense`, `formHs_le_form_of_ae_commonDirection`;
* **local domination**, where the dominating type may vary from pair to pair:
  `LocallyDominatedRad`, `formHs_ball_le_form_locallyDominated`, together with
  two families that satisfy it — every uniformly continuous configuration
  (`formHs_ball_le_form_of_uniformContinuous`) and two arbitrary narrow cone
  types split by a hyperplane (`formHs_ball_le_form_twoSide`);
* **every admissible configuration**, up to one condition on `f`: there is an
  explicit measurable domination radius `ρ > 0`
  (`exists_measurable_dominationRadius`) with Theorem 1.1's enlarged-ball form
  for every `f` such that `∫ f²ρ^{-α} < ∞`
  (`formHs_ball_le_form_of_dominationRadius`).

`planar_hypotheses_nonvacuous` and `wide_hypotheses_nonvacuous` record that none
of this is vacuous.

## What this file does not prove

The general narrow case in dimension three and above: cones of apex at most `π/4`
whose types neither overlap nor are locally dominated. What is missing there is
precisely the size of the domination radius — that `∫ f²ρ^{-α} < ∞` for every
`f ∈ H_k`. Two thin double cones with skew axes need not meet at all, so one
intermediate point cannot suffice and genuinely longer chains would be required;
producing them, with a uniform bound on the length and with positive measure at
every link, is the continuous analogue of the paper's §§5–6. The paper
establishes that machinery only in the discrete setting — which is precisely why
it goes through `ℤ^d` — and reproducing it in the continuum is an open research
problem, not a gap in this formalisation.
-/

open Metric Set MeasureTheory
open scoped Real InnerProductSpace ENNReal

open QFS

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]

/-! ## Lemma 2.2 at an arbitrary aperture

The proof of Lemma 2.2 uses `ϑ/3` only through `2·(ϑ/3) ≤ ϑ`; a net of mesh
`ϑ − θ` gives reference cones of any aperture `θ < ϑ`, at the cost of a larger
family. Nothing in the paper needs this; it is infrastructure for what follows. -/

/-! ## The averaging set, explicitly

For the chaining average one needs the ball of common neighbours as an explicit
function of `(s,t)` — a measurable selection is not enough, since the estimate
must be integrated in `s` and `t`. The centre is an explicit continuous
function, which is what the next definition records. -/

/-! ## The fibre estimate

The chaining average is exchanged with the integration in `t` by Tonelli, and
what has to survive that exchange is the weight. This is the estimate that makes
it work, and it is the reason the argument is scale-invariant: the singular
weight `‖s − t‖^{-2d-α}` integrated over the `t`-fibre above a point `z` comes
back as `‖z − s‖^{-d-α}`, exactly the weight of the `H_k` form on the pair
`(s,z)` — which the lower bound of (2) then converts into `k(s,z)`. -/

/-! ## The averaging step

The other ingredient: the oscillation between `s` and `t` is dominated by the
*average* over the ball of common neighbours of the two oscillations along the
chain `s → z → t`. This is where a positive-measure set of intermediate points
is indispensable — with the single point of Lemma 4.3 the left-hand side would
be multiplied by zero. -/

/-! ## The exchange

With the averaging step and the fibre estimate in hand, the chaining argument is
one application of Tonelli: exchange the average over the ball of common
neighbours with the integration in `t`, and the fibre estimate converts the
weight into the one carried by the pair `(s,z)`. -/

/-! ## The mirror image, on the `t` side

The chained integrand `2(f(z) − f(s))² + 2(f(t) − f(z))²` has two terms. The
first is handled by the lemmas above; the second needs the same statements with
the roles of `s` and `t` exchanged. The displacement from `s` to `t` costs one
extra unit in the estimates — `3/sin ϑ ∓ 2` in place of `3/sin ϑ ∓ 1` — but
nothing else changes. -/

/-! ## Assembling the local Poincaré inequality

Averaging bounds the oscillation pointwise; the two exchanges dispose of the two
terms of the chained integrand. Tonelli in the outer pair, once in each order,
puts each term in front of the exchange that handles it. -/

theorem QFS.measurable_param_midBall {d : ℕ} (v : EuclideanSpace ℝ (Fin d)) (ϑ : ℝ)
    {H : (EuclideanSpace ℝ (Fin d) × EuclideanSpace ℝ (Fin d)) × EuclideanSpace ℝ (Fin d) → ℝ≥0∞}
    (hH : Measurable H) :
    Measurable fun p : EuclideanSpace ℝ (Fin d) × EuclideanSpace ℝ (Fin d) =>
      ∫⁻ z in closedBall (midCentre v ϑ p.1 p.2) ‖p.1 - p.2‖, H (p, z) := by sorry