toStrongFEPair — Mathlib

English

Various auxiliary lemmas establish that the strong FE-pair obtained from a weak one retains asymptotic and integrability properties and satisfies the defining relation with h_feq and hε.

Русский

Различные вспомогательные леммы доказывают, что сильная FE-пара, полученная из слабой, сохраняет асимптотические и интеграционные свойства и удовлетворяет определённому соотношению с h_feq и hε.

LaTeX

$$toStrongFEPair._proof_1, _proof_2, _proof_3, _proof_4$$

Lean4

/-- Given a weak FE-pair `(f, g)`, modify it into a strong FE-pair by subtracting suitable
correction terms from `f` and `g`. -/
def toStrongFEPair : StrongFEPair E where
  f := P.f_modif
  g := P.symm.f_modif
  k := P.k
  ε := P.ε
  f₀ := 0
  g₀ := 0
  hf_int := P.hf_modif_int
  hg_int := P.symm.hf_modif_int
  h_feq := P.hf_modif_FE
  hε := P.hε
  hk := P.hk
  hf₀ := rfl
  hg₀ := rfl
  hf_top
    r := by
    refine (P.hf_top r).congr' ?_ (by rfl)
    filter_upwards [eventually_gt_atTop 1] with x hx
    rw [f_modif, Pi.add_apply, indicator_of_mem (mem_Ioi.mpr hx), indicator_of_notMem (notMem_Ioo_of_ge hx.le),
      add_zero, sub_zero]
  hg_top
    r := by
    refine (P.hg_top r).congr' ?_ (by rfl)
    filter_upwards [eventually_gt_atTop 1] with x hx
    rw [f_modif, Pi.add_apply, indicator_of_mem (mem_Ioi.mpr hx), indicator_of_notMem (notMem_Ioo_of_ge hx.le),
      add_zero, sub_zero]
    rfl
      /- Alternative form for the difference between `f - f₀` and its modified term. -/

Похожие утверждения