hasFiniteIntegral_on_iff — Mathlib

English

If hs and ht are fundamental domains and f is invariant under G, then HasFiniteIntegral on s equals HasFiniteIntegral on t for appropriate f.

Русский

Если s и t — фундаментальные области, и f инвариантна по G, то имеет смысл HasFiniteIntegral на s равняется HasFiniteIntegral на t.

LaTeX

$$$$\\text{HasFiniteIntegral}(f, \\mu|_s) \\iff \\text{HasFiniteIntegral}(f, \\mu|_t).$$$$

Lean4

@[to_additive]
protected theorem hasFiniteIntegral_on_iff (hs : IsFundamentalDomain G s μ) (ht : IsFundamentalDomain G t μ) {f : α → E}
    (hf : ∀ (g : G) (x), f (g • x) = f x) : HasFiniteIntegral f (μ.restrict s) ↔ HasFiniteIntegral f (μ.restrict t) :=
  by
  dsimp only [HasFiniteIntegral]
  rw [hs.setLIntegral_eq ht]
  intro g x; rw [hf]

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