[Merged by Bors] - feat(ContinuousFunctionalCalculus): add integral representation for x ↦ x ^ p for p ∈ (1, 2)

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/IntegralRepresentation.lean

@@ -32,14 +32,17 @@ relevant in applications, and would needlessly complicate the proof.
 ## Main declarations
 
 + `rpowIntegrand₀₁ p t x := t ^ p * (t⁻¹ - (t + x)⁻¹)`
-+ `exists_measure_rpow_eq_integral`: there exists a measure on `ℝ` such that
-  `x ^ p = ∫ t, rpowIntegrand₀₁ p t x ∂μ`
-+ `CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁`: the corresponding statement where
++ `rpowIntegrand₁₂ p t x := t ^ (p - 1) * (x * t⁻¹ + t * (t + x)⁻¹ - 1)`
++ `exists_measure_rpow_eq_integral_rpowIntegrand₀₁` and
+  `exists_measure_rpow_eq_integral_rpowIntegrand₁₂`: there exists a measure on `ℝ` such that
+  `x ^ p = ∫ t, rpowIntegrand₀₁ p t x ∂μ` (resp `x ^ p = ∫ t, rpowIntegrand₁₂ p t x ∂μ`)
++ `CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁` and
+  `CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₁₂`: the corresponding statements where
   `x ^ p` is defined via the CFC.
 
 ## TODO
 
-+ Give analogous representations for the ranges `Ioo (-1) 0` and `Ioo 1 2`.
++ Give analogous representations for the range `Ioo (-1) 0`.
 
 ## References
 
@@ -57,6 +60,14 @@ namespace Real
 /-- Integrand for representing `x ↦ x ^ p` for `p ∈ (0,1)` -/
 noncomputable def rpowIntegrand₀₁ (p t x : ℝ) : ℝ := t ^ p * (t⁻¹ - (t + x)⁻¹)
 
+/-- Integrand for representing `x ↦ x^p` for `p ∈ (1,2)` -/
+noncomputable def rpowIntegrand₁₂ (p t x : ℝ) : ℝ := t ^ (p - 1) * (t⁻¹ * x + t * (t + x)⁻¹ - 1)
+
+section ZeroOne
+/-
+## `p ∈ (0,1)`
+-/
+
 variable {p t x : ℝ}
 
 @[simp]
@@ -327,7 +338,7 @@ lemma rpow_eq_const_mul_integral (hp : p ∈ Ioo 0 1) (hx : 0 ≤ x) :
       this, mul_one]
 
 /-- The integral representation of the function `x ↦ x ^ p` (where `p ∈ (0, 1)`) . -/
-lemma exists_measure_rpow_eq_integral (hp : p ∈ Ioo 0 1) :
+lemma exists_measure_rpow_eq_integral_rpowIntegrand₀₁ (hp : p ∈ Ioo 0 1) :
     ∃ μ : Measure ℝ, ∀ x ∈ Ici 0,
       (IntegrableOn (fun t => rpowIntegrand₀₁ p t x) (Ioi 0) μ)
       ∧ x ^ p = ∫ t in Ioi 0, rpowIntegrand₀₁ p t x ∂μ := by
@@ -340,6 +351,90 @@ lemma exists_measure_rpow_eq_integral (hp : p ∈ Ioo 0 1) :
   · simp_rw [Measure.restrict_smul, integral_smul_nnreal_measure, rpow_eq_const_mul_integral hp hx,
       NNReal.smul_def, C, NNReal.coe_mk, smul_eq_mul]
 
+@[deprecated (since := "2026-04-03")]
+alias exists_measure_rpow_eq_integral := exists_measure_rpow_eq_integral_rpowIntegrand₀₁
+
+end ZeroOne
+
+section OneTwo
+/-
+## `p ∈ (1,2)`
+-/
+variable {p t x : ℝ}
+
+lemma rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ (hx : 0 ≤ x) (ht : 0 < t) :
+    rpowIntegrand₁₂ p t x = x * rpowIntegrand₀₁ (p - 1) t x := by
+  grind [rpowIntegrand₁₂, rpowIntegrand₀₁]
+
+lemma rpowIntegrand₁₂_nonneg (hp : 1 < p) (ht : 0 ≤ t) (hx : 0 ≤ x) :
+    0 ≤ rpowIntegrand₁₂ p t x := by
+  by_cases ht' : 0 < t
+  · rw [rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ hx ht']
+    refine mul_nonneg hx ?_
+    exact rpowIntegrand₀₁_nonneg (by grind) (by grind) hx
+  · have ht' : t = 0 := by grind
+    simp [rpowIntegrand₁₂, ht', zero_rpow (by grind : p - 1 ≠ 0)]
+
+lemma rpowIntegrand₁₂_zero (ht : 0 < t) :
+    rpowIntegrand₁₂ p t 0 = 0 := by grind [rpowIntegrand₁₂]
+
+@[fun_prop]
+lemma continuousOn_rpowIntegrand₁₂_uncurry (hp : p ∈ Ioi 1) (s : Set ℝ) (hs : s ⊆ Ici 0) :
+    ContinuousOn (rpowIntegrand₁₂ p).uncurry (Ioi 0 ×ˢ s) := by
+  unfold rpowIntegrand₁₂
+  fun_prop (disch := grind)
+
+lemma monotoneOn_rpowIntegrand₁₂ (hp : p ∈ Ioo 1 2) (ht : 0 < t) :
+    MonotoneOn (rpowIntegrand₁₂ p t) (Ici 0) := by
+  refine MonotoneOn.congr ?_ fun x hx ↦ (rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ hx ht).symm
+  apply monotoneOn_id.mul <;> grind [rpowIntegrand₀₁_monotoneOn, rpowIntegrand₀₁_nonneg]
+
+lemma integrableOn_rpowIntegrand₁₂ (hp : p ∈ Ioo 1 2) (hx : 0 ≤ x) :
+    IntegrableOn (rpowIntegrand₁₂ p · x) (Ioi 0) := by
+  have hmain : (rpowIntegrand₁₂ p · x)
+      =ᵐ[volume.restrict (Ioi 0)] (x * rpowIntegrand₀₁ (p-1) · x) := by
+    filter_upwards [ae_restrict_mem measurableSet_Ioi] with a ha
+    rw [rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ hx ha]
+  rw [integrableOn_congr_fun_ae hmain]
+  refine Integrable.const_mul ?_ _
+  exact integrableOn_rpowIntegrand₀₁_Ioi (by grind) hx
+
+/-- The integral representation of the function `x ↦ x^p` (where `p ∈ (1, 2)`) . -/
+lemma rpow_eq_const_mul_integral_rpowIntegrand₁₂ (hp : p ∈ Ioo 1 2) (hx : 0 ≤ x) :
+    x ^ p
+      = (∫ t in Ioi 0, rpowIntegrand₀₁ (p - 1) t 1)⁻¹ * ∫ t in Ioi 0, rpowIntegrand₁₂ p t x := by
+  have hmain : (rpowIntegrand₁₂ p · x)
+      =ᵐ[volume.restrict (Ioi 0)] (x * rpowIntegrand₀₁ (p-1) · x) := by
+    filter_upwards [ae_restrict_mem measurableSet_Ioi] with a ha
+    rw [rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ hx ha]
+  rw [integral_congr_ae hmain, integral_const_mul_of_integrable
+      (integrableOn_rpowIntegrand₀₁_Ioi (by grind) hx)]
+  have h₁ : x ^ p = x * x ^ (p - 1) := by
+    rw [mul_comm, ← rpow_add_one' hx (by grind)]
+    simp
+  rw [h₁, rpow_eq_const_mul_integral (by grind) hx]
+  grind
+
+/-- The integral representation of the function `x ↦ x^p` (where `p ∈ (1, 2)`) . -/
+lemma exists_measure_rpow_eq_integral_rpowIntegrand₁₂ (hp : p ∈ Ioo 1 2) :
+    ∃ μ : Measure ℝ, ∀ x ∈ Ici 0,
+      (IntegrableOn (fun t => rpowIntegrand₁₂ p t x) (Ioi 0) μ)
+      ∧ x ^ p = ∫ t in Ioi 0, rpowIntegrand₁₂ p t x ∂μ := by
+  let C : ℝ≥0 := .mk
+    (∫ t in Ioi 0, rpowIntegrand₀₁ (p - 1) t 1)⁻¹ <| by
+      rw [inv_nonneg]
+      exact le_of_lt <| integral_rpowIntegrand₀₁_one_pos (by grind)
+  let μ : Measure ℝ := C • volume
+  refine ⟨μ, fun x hx => ⟨?_, ?_⟩⟩
+  · unfold μ IntegrableOn
+    rw [Measure.restrict_smul]
+    exact Integrable.smul_measure_nnreal <| integrableOn_rpowIntegrand₁₂ hp hx
+  · rw [Measure.restrict_smul, integral_smul_nnreal_measure,
+      rpow_eq_const_mul_integral_rpowIntegrand₁₂ hp hx]
+    simp [C, NNReal.smul_def]
+
+end OneTwo
+
 end Real
 
 namespace CFC
@@ -380,7 +475,7 @@ lemma exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁ [CompleteSpac
     ∃ μ : Measure ℝ, ∀ a ∈ Ici (0 : A),
       (IntegrableOn (fun t => cfcₙ (rpowIntegrand₀₁ p t) a) (Ioi 0) μ)
       ∧ a ^ p = ∫ t in Ioi 0, cfcₙ (rpowIntegrand₀₁ p t) a ∂μ := by
-  obtain ⟨μ, hμ⟩ := exists_measure_rpow_eq_integral hp
+  obtain ⟨μ, hμ⟩ := exists_measure_rpow_eq_integral_rpowIntegrand₀₁ hp
   refine ⟨μ, fun a (ha : 0 ≤ a) => ?_⟩
   nontriviality A
   have p_pos : 0 < (p : ℝ) := by exact_mod_cast hp.1
@@ -417,6 +512,54 @@ lemma exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁ [CompleteSpac
     _ = _ := cfcₙ_setIntegral measurableSet_Ioi _ bound a hf hmapzero hbound
                 hbound_finite_integral ha.isSelfAdjoint
 
+variable (A) in
+/-- The integral representation of the function `x ↦ x ^ p` (where `p ∈ (1, 2)`). -/
+lemma exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₁₂ [CompleteSpace A] {p : ℝ≥0}
+    (hp : p ∈ Ioo 1 2) :
+    ∃ μ : Measure ℝ, ∀ a ∈ Ici (0 : A),
+      (IntegrableOn (fun t => cfcₙ (rpowIntegrand₁₂ p t) a) (Ioi 0) μ)
+      ∧ a ^ p = ∫ t in Ioi 0, cfcₙ (rpowIntegrand₁₂ p t) a ∂μ := by
+  obtain ⟨μ, hμ⟩ := exists_measure_rpow_eq_integral_rpowIntegrand₁₂ hp
+  refine ⟨μ, fun a (ha : 0 ≤ a) => ?_⟩
+  have hpcoe : (p : ℝ) ∈ Ioo 1 2 := by exact_mod_cast hp
+  let f t := rpowIntegrand₁₂ p t
+  let maxr := sSup (quasispectrum ℝ a)
+  have maxr_nonneg : 0 ≤ maxr :=
+    le_csSup_of_le (b := 0) (IsCompact.bddAbove (quasispectrum.isCompact _)) (by simp) le_rfl
+  let bound (t : ℝ) := ‖f t maxr‖
+  have hf : ContinuousOn (Function.uncurry f) (Ioi (0 : ℝ) ×ˢ quasispectrum ℝ a) :=
+    continuousOn_rpowIntegrand₁₂_uncurry hpcoe.1 (quasispectrum ℝ a) (by grind)
+  have hbound : ∀ᵐ t ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t := by
+    filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht
+    intro z hz
+    have hz' : 0 ≤ z := by grind
+    unfold bound f
+    rw [Real.norm_of_nonneg (rpowIntegrand₁₂_nonneg (by grind) (by grind) hz'),
+        Real.norm_of_nonneg (rpowIntegrand₁₂_nonneg (by grind) (by grind) maxr_nonneg)]
+    refine monotoneOn_rpowIntegrand₁₂ (by grind) (by grind) hz' maxr_nonneg ?_
+    exact le_csSup (IsCompact.bddAbove (quasispectrum.isCompact _)) hz
+  have hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0)) := by
+    rw [hasFiniteIntegral_norm_iff]
+    exact (hμ maxr maxr_nonneg).1.2
+  have hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), rpowIntegrand₁₂ p x 0 = 0 := by
+    filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht
+    simp [rpowIntegrand₁₂_zero ht]
+  refine ⟨?integrable, ?integral⟩
+  case integrable =>
+    exact integrableOn_cfcₙ measurableSet_Ioi _ bound a hf hmapzero hbound hbound_finite_integral
+  case integral => calc
+      a ^ p = cfcₙ (fun x => NNReal.nnrpow x p) a := by
+        rw [CFC.nnrpow_def]
+      _ = cfcₙ (fun r => ∫ t in Ioi 0, rpowIntegrand₁₂ p t r ∂μ) a := by
+        rw [cfcₙ_nnreal_eq_real ..]
+        refine cfcₙ_congr fun r hr => ?_
+        have hr' : 0 ≤ r := by grind
+        simp only [sup_of_le_left hr', NNReal.nnrpow_def, NNReal.coe_rpow, coe_toNNReal']
+        exact (hμ r hr').2
+      _ = ∫ t in Ioi 0, cfcₙ (rpowIntegrand₁₂ p t) a ∂μ :=
+        cfcₙ_setIntegral measurableSet_Ioi _ bound a hf hmapzero hbound
+          hbound_finite_integral ha.isSelfAdjoint
+
 end NonUnitalCFC
 
 section NonUnitalCStarAlgebra