compContinuousLinearMap — Mathlib

English

If HasFPowerSeriesWithinOnBall f pf s x r holds for a linear map u, then HasFPowerSeriesWithinOnBall for the composed function with pf.compContinuousLinearMap u and the preimage set holds, with radius adjusted by ‖u‖.

Русский

Если существует разложение сдвига для f относительно x и линейного отображения u, то для композиции f∘u существует разложение внутри шара с радиусом, откорректированным нормой u.

LaTeX

$$HasFPowerSeriesWithinOnBall f pf s (ContinuousLinearMap.funLike.coe u x) r → HasFPowerSeriesWithinOnBall (Function.comp f (ContinuousLinearMap.funLike.coe u)) (pf.compContinuousLinearMap u) (Set.preimage (ContinuousLinearMap.funLike.coe u) s) x$$

Lean4

theorem compContinuousLinearMap (hf : HasFPowerSeriesWithinOnBall f pf s (u x) r) :
    HasFPowerSeriesWithinOnBall (f ∘ u) (pf.compContinuousLinearMap u) (u ⁻¹' s) x (r / ‖u‖ₑ)
    where
  r_le := by
    calc
      _ ≤ pf.radius / ‖u‖ₑ := by
        gcongr
        exact hf.r_le
      _ ≤ _ := pf.div_le_radius_compContinuousLinearMap _
  r_pos := by
    simp only [ENNReal.div_pos_iff, ne_eq, enorm_ne_top, not_false_eq_true, and_true]
    exact pos_iff_ne_zero.mp hf.r_pos
  hasSum hy1
    hy2 := by
    convert hf.hasSum _ _
    · simp
    · simp only [Set.mem_insert_iff, add_eq_left, Set.mem_preimage, map_add] at hy1 ⊢
      rcases hy1 with (hy1 | hy1) <;> simp [hy1]
    · simp only [EMetric.ball, edist_zero_right, Set.mem_setOf_eq] at hy2 ⊢
      exact lt_of_le_of_lt (ContinuousLinearMap.le_opNorm_enorm _ _) (mul_lt_of_lt_div' hy2)

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