PositiveLocalAverages.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Positive local averaging preserves every topological boundary band. The statement allows arbitrary probability kernels; no regularity or exceptional boundary set is assumed for the kernel.

theorem OAI.CircleDomainRigidity.integral_mem_Icc_of_ae line 21

Source documentation

A probability average respects almost-everywhere interval bounds.

theorem integral_mem_Icc_of_ae
    (μ : Measure X) [IsProbabilityMeasure μ] (u : X → ℝ)
    (hu : Integrable u μ) {a b : ℝ} (hab : ∀ᵐ y ∂μ, u y ∈ Icc a b) :
    (∫y, u y ∂μ) ∈ Icc a b := by
…

def OAI.CircleDomainRigidity.LocalAverageSupport line 36
Source documentation
All averaging samples eventually lie in each relative neighborhood of this particular boundary point. This is an almost-everywhere support condition, so it also applies after choosing Borel representatives.
```
def LocalAverageSupport (G : Set X) (μ : X → Measure X) (s : X) : Prop :=
…
```
theorem OAI.CircleDomainRigidity.local_average_eventual_bounds line 39

theorem OAI.CircleDomainRigidity.local_average_tendsto line 50

Source documentation

The value of each existing limiting trace is retained by averaging.

theorem local_average_tendsto
    (G : Set X) (μ : X → Measure X) [∀x, IsProbabilityMeasure (μ x)]
    (u : X → ℝ) (hu : ∀x, Integrable u (μ x)) {s : X} {c : ℝ}
    (hs : LocalAverageSupport G μ s) (hc : Tendsto u (𝓝[G] s) (𝓝 c)) :
    Tendsto (fun x => ∫y, u y ∂μ x) (𝓝[G] s) (𝓝 c) := by
…

Mentions: OAI.CircleDomainRigidity.LocalAverageSupport

theorem OAI.CircleDomainRigidity.local_average_band_inclusion line 68

Source documentation

Positive averages with shrinking support can only contract the original pointwise band. No almost-everywhere qualification on s is needed.

theorem local_average_band_inclusion
    (G : Set X) (μ : X → Measure X) [∀x, IsProbabilityMeasure (μ x)]
    (u : X → ℝ) (hu : ∀x, Integrable u (μ x))
    (hb : ∀x, u x ∈ Icc 0 1) {s : X} (hGs : s ∈ closure G)
    (hs : LocalAverageSupport G μ s) :
    liminf u (𝓝[G] s) ≤ liminf (fun x => ∫y, u y ∂μ x) (𝓝[G] s) ∧
    limsup (fun x => ∫y, u y ∂μ x) (𝓝[G] s) ≤ limsup u (𝓝[G] s) := by
…

Mentions: OAI.CircleDomainRigidity.LocalAverageSupport

theorem OAI.CircleDomainRigidity.local_average_band_bound line 101