Planar fibre estimate for two non-parallel cone axes, integrating in the second endpoint

-- 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. -/

/-! ## The open statement, for configurations with a common cone direction

The lower bound of (2) turns the cone-restricted weight into `k`, so the local
Poincaré inequality above becomes exactly the statement §3.2 is missing —
restricted to configurations all of whose cones share a direction. -/

/-! ## Localising to a set

Corollary 2.4 reduces a configuration to finitely many cone types, so `ℝ^d`
splits into finitely many measurable pieces `U_m` on which a common direction is
available. To exploit that, the chaining estimate must hold with the *endpoints*
confined to a set — the intermediate point `z` may still range freely, since the
conversion to `k` only ever uses the cone at an endpoint. Restricting the outer
integrals is all that is required; the exchange lemmas apply unchanged. -/

/-! ## The obstruction to the cross blocks, as a theorem

The cross blocks are not merely harder — one intermediate point provably cannot
handle them. In dimension three, two double cones of aperture `ϑ < π/4` whose
axes are orthogonal and skew are **disjoint**, so no `z` at all lies in both,
let alone a set of positive measure. Chains of length two are therefore
unavoidable, and their middle edge runs between two points whose cones the
configuration assigns arbitrarily — which is exactly the difficulty §§5–6
address, in the discrete setting. -/

/-! ## The diagonal blocks of the canonical decomposition

Corollary 2.4 supplies, for any `ϑ`-bounded configuration, a finite family of
reference cones of aperture `ϑ/3` covering it pointwise. The sets
`U_V = {x | V ⊆ Γ(x)}` are measurable by Debreu's condition (carried, as
elsewhere in this repository, as the explicit hypothesis `QFS.CondMeas`), they
cover `ℝ^d`, and on each of them a common cone direction is available. So every
diagonal block is controlled, with **one constant** for all of them: `chainConst`
depends on the aperture, which is `ϑ/3` throughout, and not on the axis. -/

/-! ## Dimension two: the toolkit

In the plane the cross blocks *are* reachable: two double cones whose axes are
not parallel have intersecting axis-lines, and the "not already a cone pair"
condition supplies exactly the quantitative separation the chaining needs. The
first step is a concrete orthogonal complement. -/

/-! ## The planar averaging family, named

To feed the planar balls through `lintegral_swap_of_fibre_bound` they must be an
explicit function of the pair, and the fibre estimate needs the comparability of
`‖z − s‖`, `‖z − t‖` and `‖s − t‖` in **both** directions. -/

/-! ## The planar fibre estimate

The averaging family, packaged as a set-valued function with the side conditions
folded in, and the estimate that lets `lintegral_swap_of_fibre_bound` apply to
it. Pairs that are already cone pairs, and the diagonal, get the empty ball —
they need no chaining. -/

theorem QFS.lintegral_planarBall_fibre_le {vs vt : EuclideanSpace ℝ (Fin 2)} (hvs : ‖vs‖ = 1)
    (hvt : ‖vt‖ = 1) {ϑ : ℝ} (hϑ : 0 < ϑ) (hϑ' : ϑ ≤ π / 2) {α : ℝ} (hα : 0 ≤ α)
    (hD : cross2 vs vt ≠ 0) (s z : EuclideanSpace ℝ (Fin 2)) :
    ∫⁻ t in {t | z ∈ planarBall vs vt ϑ s t},
        ENNReal.ofReal (‖s - t‖ ^ (-(4 : ℝ) - α))
      ≤ ENNReal.ofReal (planarConst vs vt ϑ α * ‖z - s‖ ^ (-(2 : ℝ) - α)) * unitBallVol 2 := by sorry