Homogeneity of Taylor Tensors
ProvedFunctionalInequalities.Analysis.BakryEmery.taylorTensor_const_mul_readableThis statement proves homogeneity of the Taylor tensor taylorTensor under scalar multiplication.
Let be a real inner-product space with a measurable structure, let be any measure on , let , let , and let . Then
This is an algebraic scaling property of the Taylor-tensor construction and is useful for transporting scalar factors through tensor estimates.
Formalization Note No finite-dimensionality, Borel-space, finiteness, integrability, or square-integrability assumptions occur in the statement. Scalar multiplication on the target continuous multilinear map is Lean's SMul operation.
Original Lean declaration header
Within namespace FunctionalInequalities.Analysis.BakryEmery. Shown in its original module context. Proof omitted.
theorem taylorTensor_const_mul (μ : Measure E) (c : ℝ) (f : E → ℝ) (d : ℕ) :
taylorTensor μ (fun x => c * f x) d = c • taylorTensor μ f d
Module navigation
Module: Analysis/BakryEmery/Tilt/SquareIntegrable.
Definition modules: Analysis/BakryEmery/Tilt/Basic.
Previous: taylorTensor_add · Next: exists_norm_taylorTensor_le.
Source excerpt, lines 390–391 · Frozen source 408915f.
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Tilt_SquareIntegrable
open MeasureTheory Filter Topology FunctionalInequalities.Analysis.Tensor
universe u
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
omit [CompleteSpace E]
omit [FiniteDimensional ℝ E] [BorelSpace E]
theorem FunctionalInequalities.Analysis.BakryEmery.taylorTensor_const_mul_readable (μ : Measure E) (c : ℝ) (f : E → ℝ) (d : ℕ) :
taylorTensor μ (fun x => c * f x) d = c • taylorTensor μ f d := by sorry