OAI/Geometry/EinsteinFour/ScalarPoissonKernelLocal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A local pairwise almost-everywhere constancy criterion on a compact connected space with a measure of full support.

  1. theorem OAI.PositiveEinsteinFour.Geometry.ae_constant_on_of_ae_pairwise line 23
  2. theorem OAI.PositiveEinsteinFour.Geometry.ae_constants_eq_of_open_overlap line 36
  3. theorem OAI.PositiveEinsteinFour.Geometry.ae_constant_of_local_ae_pairwise line 52

    Source documentation

    Pairwise a.e. equality on a neighborhood of every point forces one global a.e. constant on a connected compact full-support measure space.

    theorem ae_constant_of_local_ae_pairwise (f : X → ℝ)
    (hlocal : ∀ x, ∃ U : Set X, IsOpen U ∧ x ∈ U ∧
      ∀ᵐ p ∂(μ.restrict U).prod (μ.restrict U), f p.1 = f p.2) :
    ∃ c : ℝ, f =ᵐ[μ] fun _ => c := by
…
  4. theorem OAI.PositiveEinsteinFour.Geometry.actual_scalar_ae_constant_of_local_ae_pairwise line 92