fun_smul — Mathlib

English

If f is absolutely continuous on [a,b], and g is absolutely continuous on [a,b], then the pointwise product x ↦ f(x) · g(x) is absolutely continuous on [a,b].

Русский

Если f и g абсолютно непрерывны на [a,b], то произведение f(x)g(x) абсолютно непрерывно на [a,b].

LaTeX

$$$\text{AbsolutelyContinuousOnInterval}(f,a,b) \wedge \text{AbsolutelyContinuousOnInterval}(g,a,b) \Rightarrow \text{AbsolutelyContinuousOnInterval}(x\mapsto f(x)\,g(x), a,b)$$$

Lean4

/-- If `f` and `g` are absolutely continuous on `uIcc a b`, then `f • g` is absolutely continuous
on `uIcc a b`. -/
theorem fun_smul {M : Type*} [SeminormedRing M] [Module M F] [NormSMulClass M F] {f : ℝ → M} {g : ℝ → F}
    (hf : AbsolutelyContinuousOnInterval f a b) (hg : AbsolutelyContinuousOnInterval g a b) :
    AbsolutelyContinuousOnInterval (fun x ↦ f x • g x) a b :=
  by
  obtain ⟨C, hC⟩ := hf.exists_bound
  obtain ⟨D, hD⟩ := hg.exists_bound
  unfold AbsolutelyContinuousOnInterval at hf hg
  apply squeeze_zero' ?_ ?_ (by simpa using (hg.const_mul C).add (hf.const_mul D))
  · exact Filter.Eventually.of_forall <| fun _ ↦ Finset.sum_nonneg (fun i hi ↦ by exact dist_nonneg)
  rw [eventually_inf_principal]
  filter_upwards with (n, I) hnI
  simp only [Finset.mul_sum, ← Finset.sum_add_distrib]
  gcongr with i hi
  trans dist (f (I i).1 • g (I i).1) (f (I i).1 • g (I i).2) + dist (f (I i).1 • g (I i).2) (f (I i).2 • g (I i).2)
  · exact dist_triangle _ _ _
  · simp only [disjWithin, mem_setOf_eq] at hnI
    gcongr
    · rw [dist_smul₀]
      gcongr
      exact hC _ (hnI.left i hi |>.left)
    · rw [mul_comm]
      grw [dist_pair_smul]
      gcongr
      rw [dist_zero_right]
      exact hD _ (hnI.left i hi |>.right)

Похожие утверждения