continuousOn_rpowIntegrand₀₁_uncurry

English

Let hp ∈ (0,1) and s ⊆ [0,∞). Then the uncurry of p ↦ rpowIntegrand₀₁ p is continuous on the product Ioi(0) × s.

Русский

Пусть hp ∈ (0,1) и s ⊆ [0,∞). Тогда развёртка функции p ↦ rpowIntegrand₀₁(p) непрерывна на произведении Ioi(0) × s.

LaTeX

$$$\\text{ContinuousOn}\\bigl(\\text{uncurry }\\bigl(p \\mapsto rpowIntegrand_{01} p\\bigr)\\bigr)\\bigl(I^+_0 \\times\\, s\\bigr)$$$

Lean4

theorem continuousOn_rpowIntegrand₀₁_uncurry (hp : p ∈ Ioo 0 1) (s : Set ℝ) (hs : s ⊆ Ici 0) :
    ContinuousOn (rpowIntegrand₀₁ p).uncurry (Ioi 0 ×ˢ s) :=
  by
  let g : ℝ × ℝ → ℝ := fun q => q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
  refine ContinuousOn.congr (f := g) ?_ fun q => ?_
  · simp only [g]
    refine ContinuousOn.mul ?_ ?_
    · refine ContinuousOn.mul ?_ (by fun_prop)
      exact ContinuousOn.rpow_const (by fun_prop) (by grind)
    · exact ContinuousOn.inv₀ (by fun_prop) (by grind)
  · intro hq
    simp [Function.uncurry, g, rpowIntegrand₀₁_eq_pow_div hp (le_of_lt hq.1) (hs hq.2)]

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