Theorems · Theorem · real analysis

LipschitzWith.integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {C : NNReal} {f g : E → ℝ} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure],
  LipschitzWith C f →
    MeasureTheory.Integrable g μ →
      ∀ (v : E),
        Filter.Tendsto (fun t => ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (nhdsWithin 0 (Set.Ioi 0))
          (nhds (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))

Defined in

Mathlib.Analysis.Calculus.Rademacher

Cited by

1 results in Mathlib

Foundations

Depth 286 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceMeasurableSpaceBorelSpaceFiniteDimensionalMeasureTheory.Measure.IsAddHaarMeasure