tailFlux

formal source

  29
  30This matches `SkewHarmGate.Radial.zeroSkewAtInfinity_of_integrable`.
  31-/
  32noncomputable def tailFlux (A A' : ℝ → ℝ) (r : ℝ) : ℝ :=
  33  (-A r) * ((A' r) * (r ^ 2))
  34
  35/-- “Tail flux vanishes at infinity”: the boundary term tends to `0` as `r → ∞`. -/
  36def TailFluxVanish (A A' : ℝ → ℝ) : Prop :=
  37  Tendsto (fun r : ℝ => tailFlux A A' r) atTop (𝓝 0)
  38
  39/-- Abstract profile for a fixed time-slice RM2U coefficient, with derivative data. -/
  40structure RM2URadialProfile where
  41  A : ℝ → ℝ
  42  A' : ℝ → ℝ
  43  A'' : ℝ → ℝ
  44  hA : ∀ x ∈ Set.Ioi (1 : ℝ), HasDerivAt A (A' x) x
  45  hA' : ∀ x ∈ Set.Ioi (1 : ℝ), HasDerivAt A' (A'' x) x
  46
  47namespace RM2URadialProfile
  48
  49/-- The boundary term associated to a profile. -/
  50noncomputable def boundaryTerm (P : RM2URadialProfile) : ℝ → ℝ :=
  51  fun r => tailFlux P.A P.A' r
  52
  53/-- Convenience: `TailFluxVanish` for a profile. -/
  54def tailFluxVanish (P : RM2URadialProfile) : Prop :=
  55  TailFluxVanish P.A P.A'
  56
  57end RM2URadialProfile
  58
  59/-- A concrete analytic target implied by UEWE and used to close RM2U in the manuscript:
  60integrability of the \(\ell=2\) coefficient and its derivative with the `r^2` weight. -/
  61def CoerciveL2Bound (P : RM2URadialProfile) : Prop :=
  62  IntegrableOn (fun r : ℝ => (P.A r) ^ 2) (Set.Ioi (1 : ℝ)) volume