  37This is intentionally *time-slice* and abstract: it doesn't define what `A_t`/`F` are, only that
  38they exist and can be paired against `A r^2` on `[a,R]`.
  39-/
  40structure ProjectedPDEPairingHypothesisAt (P : RM2URadialProfile) (a : ℝ)
  41    (At F : ℝ → ℝ) : Prop where
  42  /-- Pointwise relation on `(1,∞)`: `rm2uOp = F - At`. -/
  43  hDecomp : ∀ r ∈ Set.Ioi (1 : ℝ), rm2uOp P r = F r - At r
  44  /-- Interval-integrability of the forcing pairing on `[a,R]` (needed for linearity). -/
  45  hForceInt :
  46    ∀ R : ℝ, a ≤ R → IntervalIntegrable (fun x : ℝ => (F x) * (P.A x) * (x ^ 2)) volume a R
  47  /-- Interval-integrability of the time-derivative pairing on `[a,R]` (needed for linearity). -/
  48  hTimeInt :
  49    ∀ R : ℝ, a ≤ R → IntervalIntegrable (fun x : ℝ => (At x) * (P.A x) * (x ^ 2)) volume a R
  50  /-- Uniform bound on the forcing pairing on `[a,R]`. -/
  51  hForcePair :
  52    ∃ CF : ℝ, ∀ R : ℝ, a ≤ R → |∫ x in a..R, (F x) * (P.A x) * (x ^ 2)| ≤ CF
  53  /-- Uniform bound on the time-derivative pairing on `[a,R]`. -/
  54  hTimePair :
  55    ∃ CT : ℝ, ∀ R : ℝ, a ≤ R → |∫ x in a..R, (At x) * (P.A x) * (x ^ 2)| ≤ CT
  56
  57/-- Build the `TailFluxVanishImpliesCoerciveHypothesisAt` interface from a projected PDE pairing
  58decomposition plus the remaining local/interval hypotheses.
  59
  60This isolates the *single* extra analytic step that the TeX manuscript is implicitly using:
  61bounding `∫ (F - A_t) A r^2` by bounding the two pairings separately.
  62-/
  63theorem TailFluxVanishImpliesCoerciveHypothesisAt.of_projectedPDEPairing
  64    (P : RM2URadialProfile) (a : ℝ)
  65    (hbase : TailFluxVanishImpliesCoerciveHypothesisAt P a)
  66    {At F : ℝ → ℝ} (hpde : ProjectedPDEPairingHypothesisAt P a At F) :
  67    TailFluxVanishImpliesCoerciveHypothesisAt P a := by
  68  classical
  69  refine
  70    { ha1 := hbase.ha1

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.