Smooth even Hadamard factorisation of the odd part
Provedexists_contDiff_even_sub_comp_neg_eq_two_mul_smulLet be a finite-dimensional real normed space and a complete real normed space, and let be (ContDiff ℝ ⊤). Then there exists a map which is again , which is even in its last variable in the sense that for all and all , and which satisfies
for all and , the scalar acting on by its real scalar multiplication. Thus the odd part of in the last variable factors as times a globally smooth function that is even in ; no compact support or decay assumption is imposed on , and the statement is an existence assertion, with no uniqueness or explicit formula for claimed.
This is Hadamard's division lemma with parameters, in the form adapted to reflection in the last variable: the odd part of a smooth function vanishes to first order on and the quotient may be chosen smooth and even. It is used in the even-reflection step that splits a smooth function of into a smooth even part plus times a smooth factor, and is cited by MeasureTheory.exists_contDiff_integral_mul_log_sq_add_sq_eq_add_abs_mul_of_hasCompactSupport.
import Mathlib set_option maxHeartbeats 4000000 set_option synthInstance.maxHeartbeats 400000 set_option backward.isDefEq.respectTransparency.types false set_option autoImplicit false
theorem exists_contDiff_even_sub_comp_neg_eq_two_mul_smul
{E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
{F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
(B : E × ℝ → F) (hB : ContDiff ℝ (⊤ : ℕ∞) B) :
∃ Q : E × ℝ → F, ContDiff ℝ (⊤ : ℕ∞) Q ∧ (∀ (e : E) (ρ : ℝ), Q (e, -ρ) = Q (e, ρ)) ∧
∀ (e : E) (ρ : ℝ), B (e, ρ) - B (e, -ρ) = (2 * ρ) • Q (e, ρ) := by sorry