ClassicalGradient

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

The classical C¹ carrier, Support-layer home

The queued cleanup is DONE: the provider's duplicate copies were deleted and AffineSplitLift.lean now imports this module, so slope, slope and HasGradientOn have exactly one home and no Iff.rfl conversion is needed anywhere.

def Algsuperdiff.Section4.Support.slopeCLM {d : ℕ} (A : HCPolySupport.Vec d) : HCPolySupport.Vec d →L[ℝ] ℝ

The continuous linear functional v ↦ A · v attached to a slope A.

Equations

• Algsuperdiff.Section4.Support.slopeCLM A = ∑ i : Fin d, A i • ContinuousLinearMap.proj i

@[simp]

theorem Algsuperdiff.Section4.Support.slopeCLM_apply {d : ℕ} (A v : HCPolySupport.Vec d) : (slopeCLM A) v = HCPolySupport.vecDot A v

def Algsuperdiff.Section4.Support.HasGradientOn {d : ℕ} (W : Set (HCPolySupport.Vec d)) (f : HCPolySupport.Vec d → ℝ) (G : HCPolySupport.Vec d → HCPolySupport.Vec d) : Prop

f is differentiable on W with gradient field G. This is the classical C¹ half of the source hypothesis h ∈ C^{1,1/2}(□_m), written against Vec d's sup-norm through slopeCLM.

Equations

• Algsuperdiff.Section4.Support.HasGradientOn W f G = ∀ y ∈ W, HasFDerivWithinAt f (Algsuperdiff.Section4.Support.slopeCLM (G y)) W y

theorem Algsuperdiff.Section4.Support.HasGradientOn.mono_set {d : ℕ} {U V : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → ℝ} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} (hf : HasGradientOn U f G) (hVU : V ⊆ U) : HasGradientOn V f G

HasGradientOn is antitone in the window: the Fréchet derivative within a set restricts to any subset. Consolidated here from the two identically named provider copies in Provider/ExcessDecay/OneStepAssembly.lean and Provider/ExcessDecay/BoundaryAssemblyTransport.lean, so that dot notation h.mono_set hsub keeps working on the single Support-layer carrier.