English
For hp ∈ (0,1) and hx ≥ 0, the function t ↦ rpowIntegrand₀₁ p t x is integrable on Ioi 0.
Русский
Для hp ∈ (0,1) и hx ≥ 0 интегрируемость на Ioi 0 функции t ↦ rpowIntegrand₀₁ p t x.
LaTeX
$$$\\text{IntegrableOn}\\bigl(t \\mapsto rpowIntegrand_{01} p\\, t\\, x\\bigr)\\,(Ioi 0)\\;\\text{Real.measureSpace.volume}$$$
Lean4
theorem cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one {p t : ℝ} (hp : p ∈ Ioo 0 1) (ht : 0 < t) (a : A)
(ha : 0 ≤ a) : cfcₙ (rpowIntegrand₀₁ p t) a = t ^ (p - 1) • cfcₙ (rpowIntegrand₀₁ p 1) (t⁻¹ • a) :=
by
have hspec : quasispectrum ℝ a ⊆ Ici 0 := by intro; grind
have h_mapsTo : MapsTo (t⁻¹ • · : ℝ → ℝ) (Ici 0) (Ici 0) :=
by
intro x hx
simp only [mem_Ici, smul_eq_mul] at hx ⊢
positivity
calc
_ = cfcₙ (fun x => t ^ ((p : ℝ) - 1) * (rpowIntegrand₀₁ p 1 (t⁻¹ • x))) a :=
by
refine cfcₙ_congr ?_
refine Set.EqOn.mono hspec (rpowIntegrand₀₁_eqOn_mul_rpowIntegrand₀₁_one ht)
_ = t ^ ((p : ℝ) - 1) • cfcₙ (fun x => rpowIntegrand₀₁ p 1 (t⁻¹ • x)) a :=
by
refine cfcₙ_smul (R := ℝ) (t ^ ((p : ℝ) - 1)) _ a ?_
refine ContinuousOn.mono ?_ hspec
have := continuousOn_rpowIntegrand₀₁_Ici hp zero_lt_one
fun_prop (disch := assumption)
_ = t ^ ((p : ℝ) - 1) • cfcₙ (rpowIntegrand₀₁ p 1) (t⁻¹ • a) :=
by
congr! 1
refine cfcₙ_comp_smul (R := ℝ) t⁻¹ (fun x => rpowIntegrand₀₁ p 1 x) a ?_
exact continuousOn_rpowIntegrand₀₁_Ici hp zero_lt_one |>.mono <| (h_mapsTo.mono_left hspec).image_subset
