EnergyMinimality #

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Dirichlet energy minimality of the weakly harmonic replacement #

The corrector v₁ of the boundary datum split is the weakly harmonic function on the window W carrying the trace of the datum deviation Φ = h − ℓ_h. Pricing it in L² (OneStepL2) needs its Dirichlet energy, and the only handle on that is the defining orthogonality of IsUnitWeaklyHarmonicOn — ∫_W ∇v₁ · ∇φ = 0 for every φ ∈ H¹₀(W) — read at the admissible test function φ = v₁ − Φ.

The whole content is one expansion:

  0 ≤ ∫_W |∇v₁ − ∇Φ|²
    = ∫_W |∇v₁|² − 2 ∫_W ∇v₁·∇Φ + ∫_W |∇Φ|²
    = ∫_W |∇v₁|² − 2 ∫_W |∇v₁|²  + ∫_W |∇Φ|²        (orthogonality)
    = ∫_W |∇Φ|² − ∫_W |∇v₁|² ,

the middle step because ∫_W ∇v₁·∇Φ = ∫_W ∇v₁·∇v₁ − ∫_W ∇v₁·∇(v₁ − Φ) and the second summand vanishes. No positivity of a quadratic form, no Cauchy–Schwarz: the test function v₁ − Φ is exactly the one that makes the discriminant argument collapse to the single evaluation t = 1.

The hypothesis is stated against the H¹₀ witness rho rather than against MemH10 W (v₁ − Φ), because MemH10 pins only the value representative and the energy is a statement about gradients; Corrector.exists_unitWeaklyHarmonicOn_of_datum builds its corrector as Φ + rho.toH1Function, so the gradient identity below is available at its construction site by H1Function.add_grad.