circleAverage_congr_codiscreteWithin

English

If two functions agree outside a codiscreteWithin sphere, their circle averages coincide.

Русский

Если две функции согласуются за пределами кодискретной области сферы, их окружные средние совпадают.

LaTeX

$$$circleAverage\ f_1\ c\ R = circleAverage\ f_2\ c\ R$ при условии\ f_1 =_{{codiscreteWithin(sphere\ c\ |R|)}}\ f_2$$

Lean4

/-- If two functions agree outside of a discrete set in the circle, then their averages agree. -/
theorem circleAverage_congr_codiscreteWithin (hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂) (hR : R ≠ 0) :
    circleAverage f₁ c R = circleAverage f₂ c R :=
  by
  unfold circleAverage
  congr 1
  apply intervalIntegral.integral_congr_ae_restrict
  apply ae_restrict_le_codiscreteWithin measurableSet_uIoc
  apply codiscreteWithin.mono (by tauto) (circleMap_preimage_codiscrete hR hf)

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