EquationRestriction

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

Restricting the anchor's equation to the parent window

This module performs the restriction.

CoarseGraining proves exactly this for triadic descendants (Ch03.ABK26.IsForcedEquation.restrictToDescendant) by zero-extending the descendant test function; the window z + □_{n+2} is a translate by an arbitrary real z and is not a triadic cube, so the descendant version does not apply. The general statement — restriction to an arbitrary open subset — is proved here by the same two-line mechanism at h10ExtendToSuperset (EquationRestrictionZeroExtension.lean: the p = 2 re-derivation of CoarseGraining's unavailable H10Function.extendByZeroToOpenSuperset) and H1Function.restrict.

Sign conventions

Support.IsDivFormWeakSolutionOn renders -∇·a∇u = ∇·g with the minus sign on the right (⟪∇·g, φ⟫ = -∫ g·∇φ); CoarseGraining's Ch03.IsForcedEquation fixes the opposite convention. The bridge below is therefore stated at the negated forcing, exactly as Support/Dirichlet.lean documents for CoarseGraining's IsZeroTraceDirichletRhsWeakSolution. Every right-hand side of the frozen theorem is a seminorm of g, invariant under g ↦ -g.

Main results

• isDivFormWeakSolutionOn_restrict — the weak equation restricts to every open subset.
• isDivFormWeakSolutionOn_translateWindow_of_frontier_inter_empty — the same at the anchor's own gate and window z + □_k ⊆ □_m.
• isForcedEquation_of_isDivFormWeakSolutionOn (and the converse) — the convention bridge to CoarseGraining's cube predicate.

References

• ABK26, l.harmonic.approximation.good.scales.
• CoarseGraining, Homogenization/Book/Ch03/ABK26/LocalCoarseGraining.lean (IsForcedEquation.restrictToDescendant), Homogenization/Sobolev/H1/BasicLemmas.lean (H1Function.restrict).

1. The zero-extension identity for set integrals

2. The restriction to an arbitrary open subset

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isDivFormWeakSolutionOn_restrict {d : ℕ} {W V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (hVW : V ⊆ W) {a : HCPolySupport.CoeffField d} {u : HCPolySupport.H1Function W} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (h : Support.IsDivFormWeakSolutionOn a W u g) : Support.IsDivFormWeakSolutionOn a V (u.restrict hV hVW) g

The divergence-form weak equation restricts to every open subset.

If -∇·a∇u = ∇·g weakly on W and V ⊆ W is open, then the same equation holds weakly on V for the restriction of u. The arbitrary-open-subset generalization of Ch03.ABK26.IsForcedEquation.restrictToDescendant.

4. The convention bridge to CoarseGraining's cube predicate

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isForcedEquation_neg_of_isDivFormWeakSolutionOn {d : ℕ} {Q : HCPolySupport.TriadicCube d} {a : HCPolySupport.Book.Ch03.CoeffFamily d} {u : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain Q).carrier} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (h : Support.IsDivFormWeakSolutionOn (a.coeffOn Q).toCoeffField (HCPolySupport.Book.Ch02.cubeDomain Q).carrier u g) : HCPolySupport.Book.Ch03.IsForcedEquation Q a u fun (x : HCPolySupport.Vec d) => -g x

The forcing-sign variant consumed by the translated-frame assembly: an unnegated IsDivFormWeakSolutionOn datum produces CoarseGraining's predicate at the negated forcing.