Integral adjoint of a finite family of normal reflection dilations
ProvedMeasureTheory.integral_finite_halfSpace_reflectionLet f be locally integrable with respect to volume restricted to the positive coordinate half-space H, let b_j be finitely many positive real dilation factors, and let c_j be arbitrary real coefficients. Retain f on H and extend it below the boundary by the sum of c_j f(x with normal coordinate replaced by -b_j x_i). Its integral against any continuous compactly supported test equals the integral on H of f against the adjoint test: the original test plus the sum of (c_j/b_j) times the test evaluated with normal coordinate -x_i/b_j. The separating hyperplane has zero volume, and the inverse absolute determinant is 1/b_j. No weak derivatives or moment conditions are involved. The empty family is allowed. This is an independent finite-family change-of-variables interface, extending the signed isometric coordinate fold to arbitrary positive dilations.
import Mathlib.MeasureTheory.Function.LocallyIntegrable import Mathlib.MeasureTheory.Integral.Bochner.Basic import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace open MeasureTheory set_option autoImplicit false
theorem MeasureTheory.integral_finite_halfSpace_reflection
{n N : ℕ} (i : Fin n) (b c : Fin N → ℝ) (hb : ∀ j, 0 < b j)
(f φ : EuclideanSpace ℝ (Fin n) → ℝ)
(hf : LocallyIntegrable f (volume.restrict {x | 0 < x i}))
(hφ : Continuous φ) (hcφ : HasCompactSupport φ) :
(∫ x, (if 0 < x i then f x else
∑ j : Fin N, c j * f (WithLp.toLp 2
(Function.update (fun k => x k) i (-b j * x i)))) * φ x) =
∫ x in {x : EuclideanSpace ℝ (Fin n) | 0 < x i},
f x * (φ x + ∑ j : Fin N, (c j / b j) *
φ (WithLp.toLp 2 (Function.update (fun k => x k) i (-(b j)⁻¹ * x i)))) := by sorry