Theorem 1.1's enlarged-ball form in the plane, unconditionally

-- Generated by skeleton subtraction from QuadraticFormsSobolev/BeyondThePaper.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_AppendixA
import Definitions.Def_QFS_BeyondThePaper
import Definitions.Def_QFS_Regimes
import Definitions.Def_QFS_FavoredGraph
import Definitions.Def_QFS_Indicator
import Definitions.Def_QFS_WhitneyDomain
import Definitions.Def_QFS_FunctionSpaces
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. -/

/-! ### The `t` side of the planar family -/

/-! ### Assembling the planar cross blocks -/

/-! ### The dichotomy in the plane

Two reference cones of the same aperture either have non-parallel axes — and then
`formHs_le_form_planar_cross` applies — or they are the *same* double cone, and
then the block is diagonal and `formHs_le_form_of_commonDirection_on` applies. In
the plane there is no third possibility, which is exactly why *this* argument
closes here and not in higher dimensions; the higher-dimensional regimes are
reached below by other means. -/

/-! ### One block of the planar decomposition -/

/-! ## The open statement, in dimension two

Corollary 2.4 covers `ℝ²` by finitely many pieces on each of which a reference
cone is available; the squares of that cover exhaust `ℝ² × ℝ²`; every block is
controlled by `planar_block_le`; and a finite sum of finite constants is
finite. -/

/-! ## The ball-localised form, in dimension two

§3.2 consumes the inclusion on a ball, not on the whole plane. A Lipschitz
cutoff bridges the two: `χf` agrees with `f` on the inner ball and is supported
in the outer one, so the whole-space theorem applies to it, and
`form_cutoff_le` says the cost is the `H_k` form on the outer ball plus an `L²`
term. Both are finite for `f ∈ H_k(B*)`, which is exactly the hypothesis §3.2
has. -/

/-! ## Theorem 1.1 on a ball, unconditionally, in the plane

Section 3.2 leaves one hypothesis undischarged: the `H^{α/2}` form of the
larger ball must be known to be finite before the dominated convergence step
can run (`QFS.formHs_ball_le_form_of_formHs_ne_top`).  In the plane
`formHs_ball_ne_top_of_planar` -- proved above, and *not* in the paper --
supplies exactly that for every `f ∈ H_k`, so the two combine into the paper's
statement with no hypothesis beyond `f ∈ L²` of the larger ball.

The mathematics closing the gap is new; the statement obtained is the paper's. -/

theorem QFS.formHs_ball_le_form_planar {ϑ α Λ : ℝ} (hϑ : 0 < ϑ) (hϑ' : ϑ ≤ Real.pi / 2)
    (hα : 0 < α) (hα2 : α < 2) (hΛ : 1 ≤ Λ) :
    ∃ κ c : ℝ, 1 ≤ κ ∧ 1 ≤ c ∧
      ∀ Γ : Configuration (EuclideanSpace ℝ (Fin 2)), IsBounded Γ ϑ → CondMeas Γ →
      ∀ k : EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) → ℝ≥0∞,
        KernelBounds Γ α Λ k →
        (Measurable fun p : EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2) =>
          k p.1 p.2) →
      ∀ (x₀ : EuclideanSpace ℝ (Fin 2)) (R : ℝ), 0 < R →
      ∀ f : EuclideanSpace ℝ (Fin 2) → ℝ, 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 := by sorry


/-! ## Theorem 1.4 for `Ω = ℝ²`

The paper deduces the whole-space case from Theorem 1.1 by monotone convergence,
the constant being independent of the radius.  `QFS.theoremOneFourUniv_of_theoremOneOne`
is that deduction from the paper's `Prop`; here it is run on the planar theorem
instead. -/

/-! ## Theorem 1.4 for a domain, in the plane

Lemma A.1 for a domain (`QFS.formHs_le_form_domain`) turns the ball
comparability into the comparability on `Ω`, given the Whitney family of `Ω` and
Dyda's inequality — the two inputs the paper quotes.  With the planar ball
theorem it gives the inclusion `H_k(Ω) ⊆ H^{α/2}(Ω)` for every planar domain
that has such a family. -/

/-! ## Lemma 3.7's own statement, in the plane

Lemma 3.7 says the two spaces coincide on a ball.  That follows from the
same-ball comparability, which in the plane is `formHs_le_form_planar`. -/

/-! ### The planar hypotheses are satisfiable -/

/-! ## Theorem 1.1 itself, in the plane

Everything above assembles into the paper's own Theorem 1.1, in dimension two,
with the two hypotheses this formalisation carries and the one input Lemma A.1
quotes. -/

/-! ## Wide cones: dimension three and above

The obstruction to the cross blocks is that two double cones with skew axes can
be disjoint (`no_common_neighbour_of_skew_axes`). That cannot happen when the
cones are **wide**: the angle between two axes, read as an angle between lines,
is at most `π/2`, so two double cones of apex angle more than `π/4` always
overlap in a cone of aperture `apex − π/4`. Their bisector is its axis.

Everything else is already in place: the chaining machinery
(`formHs_le_form_of_commonDirection_on`) asks only that the two ends admit a
*common* cone, not that the configuration be constant, so with the bisector in
hand every block — diagonal or cross — is controlled, in every dimension. -/

/-! ## Pairwise overlapping cones: narrow cones without a common direction

Chains of length three or more are what the general narrow case would need (see
the note below), and they are out of reach here: their interior legs run between
two intermediate points whose types the configuration assigns adversarially. But
chains of length two reach further than the wide-cone case suggests. All they need is that
the two cones **overlap** — the intermediate point is then seen by both
endpoints' own cones, and no constraint is placed on its type. Overlapping is
strictly weaker than sharing a direction: three cones can pairwise overlap with
no direction common to all three, and that happens for narrow cones in dimension
three and above. -/

/-! ### When do two cones overlap?

The bisector argument of `exists_common_subcone` is not about `π/4`: two double
cones of apex `θ` overlap in a cone of aperture `θ − β`, where `β` is half the
angle between their axes. The `π/4` threshold is what makes *every* pair overlap;
a particular pair needs only its own axes to be close. -/

/-! ## Theorem 1.1 when the axis spread is below twice the apex bound

The same assembly as in the plane, with `formHs_ball_ne_top_of_spread` in place
of `formHs_ball_ne_top_of_planar`. The wide-cone statements below are the case
`γ = π/2`. -/

/-! ## Theorem 1.4 for small axis spread -/

/-! ## The wide-cone regime, as the case `γ = π/2`

Two lines are never more than `π/2` apart, so a configuration with apex bound
`ϑ > π/4` has axis spread below `2ϑ` automatically. Every wide-cone statement
below is therefore an instance of the corresponding small-spread statement. -/

/-! ## Dimension one is trivial

On the line a double cone of positive apex angle is everything but the origin,
so *every* pair of distinct points is a cone pair and the lower bound of (2)
gives the inclusion directly, with the constant `Λ/2`. This is what makes the
open case precisely "narrow cones in dimension at least three". -/

/-! ### The wide-cone hypotheses are satisfiable -/

/-! ## Narrow cones: a densely visible type

The obstruction in dimension three and above is that the cones at `s` and at `t`
can be disjoint, so no single point sees both. But the chaining never needed the
intermediate point to be seen *by the cones of the endpoints*: it needs the three
points to be joined by cone pairs, and a pair `(s,z)` is a cone pair as soon as
`s − z` lies in the cone at `z`. So it is enough that the intermediate points be
of one fixed type — the balls of `exists_ball_in_two_cones` are available for
*every* pair, since that lemma constrains only the direction `v`, not the
configuration.

What has to be paid for is measure: the average is over the part of the ball
that has the right type. The hypothesis below asks exactly that this part be a
fixed fraction. -/

/-! ### The same, for one pair at a time and on a set of pairs

The density of the visible type is used only at the ball the chaining averages
over, once per pair. Isolating that is what lets the type vary from pair to
pair. -/

/-! ## Local domination: the type may vary from point to point

The chaining needs, for each pair `(s,t)`, only that *some* reference cone is
contained in the cones of a fixed fraction of the one ball it averages over — and
that ball is determined by `s`, by `‖s−t‖` and by the reference direction, not by
the direction of `t−s`. The type may therefore vary from pair to pair, and the
Lebesgue density theorem supplies the fraction at almost every point. What it
does not supply is a *uniform* radius below which the fraction is there; that
uniformity, `QFS.LocallyDominated`, is exactly what separates the theorem below
from the open statement. -/

/-! ### The consequence for §3.2

The same cutoff argument as in the wide and small-spread regimes, with the extra
`L²` term of `QFS.formHs_univ_le_of_locallyDominated` absorbed. -/


/-! ### A configuration no earlier theorem reaches

Two arbitrary cone types, as narrow as one likes and pointing in unrelated
directions, split by a hyperplane. At every point one of the two closed
half-spaces contains at least half of the ball the chaining averages over — a
point reflection in its centre carries the outside part into the inside part — so
the configuration is locally dominated, and Theorem 1.1 holds for it. -/

/-! ### Continuous configurations are locally dominated

If the cone axis varies uniformly continuously, then near any point every cone
still contains one fixed reference cone, so the whole chaining ball is of a single
type and the hypothesis holds with a uniform radius. Theorem 1.1 therefore holds
for every uniformly continuous configuration, in every dimension and at any apex
angle. -/

/-! ### A measurable domination radius, for every configuration

The pointwise radius of `QFS.ae_exists_dominating_type` is not measurable as it
stands. Restricting the density requirement to the dyadic scales makes the sets
`QFS.denseFrom` measurable, and their union over the finitely many types gives an
explicit measurable radius `QFS.domRadius` which is positive everywhere and below
which the chaining always serves the pair. What is left of the open statement is
then the size of that radius: `∫ f²ρ^{-α} < ∞`. -/

/-! ### How far the one-point chaining reaches

The hypothesis of `formHs_le_form_of_visibleDense` asks for density at *every*
scale, because pairs at every distance need intermediate points. By the Lebesgue
density theorem that forces the visible set to be co-null: a set of uniform
positive density at all scales has null complement. So the theorem above is
exactly the almost-everywhere form of the common-direction theorem, and **no
sparser set of good types can serve a chaining argument with a single
intermediate point** — which is why the narrow-cone case in dimension three and
above needs chains of length at least three, and with them the continuum
analogue of §§5–6. -/

/-! ### The overlap hypothesis is not vacuous, and is strictly weaker

Three unit vectors in `ℝ³` with pairwise inner product `8/9`, and the apex
`θ = arccos √(14/15) ≈ 15°` — far below the `π/4` at which every pair of double
cones is forced to meet. The three cones still overlap pairwise, because half the
angle between two axes is `arccos √(17/18) < θ`; but no direction lies in all
three at once, because for a unit `u`

  `∑ᵢ ⟪vᵢ, u⟫² = (8 (u₀+u₁+u₂)² + 1)/9 ≤ 25/9 < 3 · 14/15`,

so some `|⟪vᵢ, u⟫|` falls below `cos θ = √(14/15)`. Neither
`sobolevInclusion_wide` nor `formHs_le_form_of_commonDirection` applies to such a
configuration; `sobolevInclusion_of_overlapping` does. -/

/-! ## Theorem 1.4 for a domain, under small axis spread

The planar assembly of `QFS.Hk_domain_eq_Hs_domain_planar`, with
`QFS.ballComparability_spread` in place of the planar ball comparability. Taking
`γ = π/2` gives the wide-cone case in every dimension. -/