exact (continuousOn_const.rpow continuousOn_id fun _ _ ↦ Or.inl <| ne_of_gt (abs_pos_of_pos xpos))
  |>.const_isThetaUniformlyOn_isCompact isCompact_uIcc (by norm_num)
  (fun i _ ↦ ne_of_gt <| rpow_pos_of_pos (abs_pos_of_pos xpos) _) _
case refine_1
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
⊢ (fun x_1 =>
      match x_1 with
      | (σ, _y) => |x| ^ σ) =Θ[l]
    fun x => 1
no goals