Coarse-graining support: Support.Sobolev.CubeEmbedding.OneDimIBP

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

One-dimensional integration by parts across a kink

Standalone real-analysis lemma feeding the Fubini assembly of the single-face even reflection. A function that is C¹ on each side of a point a and continuous across it integrates by parts against a C¹ compactly supported test with no interface term — the two boundary contributions at a cancel because the function matches there.

theorem HCPolySupport.integral_mul_deriv_piecewise_eq_neg (a : ℝ) {f₁ f₂ f₁' f₂' φ φ' : ℝ → ℝ} (hf₁ : ∀ (x : ℝ), HasDerivAt f₁ (f₁' x) x) (hf₁' : Continuous f₁') (hf₂ : ∀ (x : ℝ), HasDerivAt f₂ (f₂' x) x) (hf₂' : Continuous f₂') (hmatch : f₁ a = f₂ a) (hφ : ∀ (x : ℝ), HasDerivAt φ (φ' x) x) (hφ' : Continuous φ') (hφ_supp : HasCompactSupport φ) : ∫ (t : ℝ), (if t ≤ a then f₁ t else f₂ t) * φ' t = -∫ (t : ℝ), (if t ≤ a then f₁' t else f₂' t) * φ t

Integration by parts across a kink. If f₁, f₂ : ℝ → ℝ are C¹ (globally, via HasDerivAt with continuous derivatives) and agree at a, and φ is C¹ with compact support, then the piecewise function t ↦ if t ≤ a then f₁ t else f₂ t integrates by parts against φ' with derivative the piecewise t ↦ if t ≤ a then f₁' t else f₂' t and no boundary term.

theorem HCPolySupport.integral_mul_deriv_eq_neg {f f' φ φ' : ℝ → ℝ} (hf : ∀ (x : ℝ), HasDerivAt f (f' x) x) (hf' : Continuous f') (hφ : ∀ (x : ℝ), HasDerivAt φ (φ' x) x) (hφ' : Continuous φ') (hφ_supp : HasCompactSupport φ) : ∫ (t : ℝ), f t * φ' t = -∫ (t : ℝ), f' t * φ t

One-dimensional integration by parts (globally C¹ special case). No interface, no boundary term.

theorem HCPolySupport.integral_mul_deriv_two_kink_eq_neg (b₁ b₂ : ℝ) (hb : b₁ ≤ b₂) {f₁ f₂ f₃ f₁' f₂' f₃' φ φ' : ℝ → ℝ} (hf₁ : ∀ (x : ℝ), HasDerivAt f₁ (f₁' x) x) (hf₁' : Continuous f₁') (hf₂ : ∀ (x : ℝ), HasDerivAt f₂ (f₂' x) x) (hf₂' : Continuous f₂') (hf₃ : ∀ (x : ℝ), HasDerivAt f₃ (f₃' x) x) (hf₃' : Continuous f₃') (hm₁ : f₁ b₁ = f₂ b₁) (hm₂ : f₂ b₂ = f₃ b₂) (hφ : ∀ (x : ℝ), HasDerivAt φ (φ' x) x) (hφ' : Continuous φ') (hφc : HasCompactSupport φ) : ∫ (t : ℝ), (if t < b₁ then f₁ t else if b₂ < t then f₃ t else f₂ t) * φ' t = -∫ (t : ℝ), (if t < b₁ then f₁' t else if b₂ < t then f₃' t else f₂' t) * φ t

Integration by parts across two kinks. If f₁, f₂, f₃ are globally C¹ and match at b₁ ≤ b₂ (f₁ b₁ = f₂ b₁, f₂ b₂ = f₃ b₂), the continuous piecewise function t ↦ if t < b₁ then f₁ t else if b₂ < t then f₃ t else f₂ t integrates by parts against a C¹ compactly supported test with the piecewise derivative and no boundary term.