InvariantMean.lean`

132 declarations, 0 contain sorry, 0 declared as axioms

A discrete abelian invariant mean, constructed from weighted cube averages. Repeated group elements keep their multiplicities.

def OAI.PlaneFiveColor.InvariantMean.shift line 21
Source documentation
Translation acts on all bounded functions because the domain is discrete.
```
def shift (g : G) (f : G →ᵇ ℝ) : G →ᵇ ℝ :=
…
```
lemma OAI.PlaneFiveColor.InvariantMean.shift_apply line 24
lemma OAI.PlaneFiveColor.InvariantMean.shift_comm line 26
lemma OAI.PlaneFiveColor.InvariantMean.shift_add line 30
lemma OAI.PlaneFiveColor.InvariantMean.shift_sub line 34
lemma OAI.PlaneFiveColor.InvariantMean.shift_smul line 38
lemma OAI.PlaneFiveColor.InvariantMean.shift_norm_le line 42
def OAI.PlaneFiveColor.InvariantMean.single line 46
Source documentation
A single cyclic Cesàro average, always with a positive denominator.
```
def single (g : G) (n : ℕ) (f : G →ᵇ ℝ) : G →ᵇ ℝ :=
…
```
lemma OAI.PlaneFiveColor.InvariantMean.single_apply line 49
lemma OAI.PlaneFiveColor.InvariantMean.single_norm_le line 53
lemma OAI.PlaneFiveColor.InvariantMean.single_add line 65
lemma OAI.PlaneFiveColor.InvariantMean.single_sub line 69
lemma OAI.PlaneFiveColor.InvariantMean.single_smul line 73
lemma OAI.PlaneFiveColor.InvariantMean.single_shift line 78
lemma OAI.PlaneFiveColor.InvariantMean.single_const line 88
lemma OAI.PlaneFiveColor.InvariantMean.single_nonneg line 95
lemma OAI.PlaneFiveColor.InvariantMean.single_telescope line 102
lemma OAI.PlaneFiveColor.InvariantMean.single_coboundary_norm line 113
def OAI.PlaneFiveColor.InvariantMean.cube line 128
Source documentation
Multiplicities in the cube are explicitly retained through composition.
```
def cube : List G → ℕ → (G →ᵇ ℝ) → (G →ᵇ ℝ)
  | [], _, f => f
  | g::L, n, f => single g n (cube L n f)
```
Mentions: OAI.PlaneFiveColor.InvariantMean.single
lemma OAI.PlaneFiveColor.InvariantMean.cube_norm_le line 132
lemma OAI.PlaneFiveColor.InvariantMean.cube_shift line 137
lemma OAI.PlaneFiveColor.InvariantMean.cube_add line 143
lemma OAI.PlaneFiveColor.InvariantMean.cube_sub line 149
lemma OAI.PlaneFiveColor.InvariantMean.cube_smul line 155
lemma OAI.PlaneFiveColor.InvariantMean.cube_const line 161
lemma OAI.PlaneFiveColor.InvariantMean.cube_nonneg line 167
lemma OAI.PlaneFiveColor.InvariantMean.cube_coboundary_norm line 175
Source documentation
Each listed generator has the same boundary bound, independently of the length of the list and without an injective image assumption.
```
lemma cube_coboundary_norm (L : List G) (g : G) (hg : g ∈ L) (n : ℕ) (f : G →ᵇ ℝ) :
    ‖cube L n (shift g f-f)‖ ≤ 2 * ‖f‖ / (n+1 : ℕ) := by
…
```
Mentions: OAI.PlaneFiveColor.InvariantMean.cube, OAI.PlaneFiveColor.InvariantMean.shift
def OAI.PlaneFiveColor.InvariantMean.approx line 188
Source documentation
The directed weighted-cube averages.
```
def approx (i : Finset G × ℕ) (f : G →ᵇ ℝ) : ℝ :=
…
```
lemma OAI.PlaneFiveColor.InvariantMean.approx_norm_le line 191
def OAI.PlaneFiveColor.InvariantMean.averagingUF line 195
Source documentation
One fixed ultrafilter is used for all functions.
```
def averagingUF (G : Type*) [AddCommGroup G] : Ultrafilter (Finset G × ℕ) :=
…
```
lemma OAI.PlaneFiveColor.InvariantMean.averagingUF_le line 199
lemma OAI.PlaneFiveColor.InvariantMean.approx_has_limit line 202
def OAI.PlaneFiveColor.InvariantMean.mean line 215
Source documentation
The invariant mean, as the limit of the multiplicity-preserving averages.
```
def mean (f : G →ᵇ ℝ) : ℝ :=
…
```
lemma OAI.PlaneFiveColor.InvariantMean.tendsto_approx line 218
lemma OAI.PlaneFiveColor.InvariantMean.mean_add line 222
lemma OAI.PlaneFiveColor.InvariantMean.mean_smul line 227
lemma OAI.PlaneFiveColor.InvariantMean.mean_const line 232
lemma OAI.PlaneFiveColor.InvariantMean.mean_nonneg line 238
lemma OAI.PlaneFiveColor.InvariantMean.mean_norm_le line 242
lemma OAI.PlaneFiveColor.InvariantMean.eventually_mem line 247
lemma OAI.PlaneFiveColor.InvariantMean.tendsto_index line 255
lemma OAI.PlaneFiveColor.InvariantMean.tendsto_boundary line 264
lemma OAI.PlaneFiveColor.InvariantMean.mean_shift line 273
def OAI.PlaneFiveColor.InvariantMean.meanCLM line 284
Source documentation
A normalized positive shift-invariant continuous real linear functional.
```
def meanCLM : (G →ᵇ ℝ) →L[ℝ] ℝ :=
…
```
lemma OAI.PlaneFiveColor.InvariantMean.meanCLM_apply line 289
def OAI.PlaneFiveColor.InvariantMean.realPart line 291
def OAI.PlaneFiveColor.InvariantMean.imagPart line 293
lemma OAI.PlaneFiveColor.InvariantMean.realPart_apply line 296
lemma OAI.PlaneFiveColor.InvariantMean.imagPart_apply line 298
def OAI.PlaneFiveColor.InvariantMean.cmean line 301
Source documentation
Complexification of the same (not a separately chosen) real mean.
```
def cmean (f : G →ᵇ ℂ) : ℂ := (mean (realPart f) : ℂ) + (mean (imagPart f) : ℂ) * Complex.I
```
Mentions: OAI.PlaneFiveColor.InvariantMean.mean, OAI.PlaneFiveColor.InvariantMean.realPart, OAI.PlaneFiveColor.InvariantMean.imagPart
lemma OAI.PlaneFiveColor.InvariantMean.cmean_add line 303
lemma OAI.PlaneFiveColor.InvariantMean.cmean_smul line 309
lemma OAI.PlaneFiveColor.InvariantMean.realPart_norm_le line 319
lemma OAI.PlaneFiveColor.InvariantMean.imagPart_norm_le line 325
lemma OAI.PlaneFiveColor.InvariantMean.cmean_norm_le line 330
def OAI.PlaneFiveColor.InvariantMean.cmeanCLM line 338
lemma OAI.PlaneFiveColor.InvariantMean.cmeanCLM_apply line 343
lemma OAI.PlaneFiveColor.InvariantMean.cmean_const line 345
def OAI.PlaneFiveColor.InvariantMean.cshift line 351
Source documentation
Complex translation; no ordinary measurability is asserted or needed.
```
def cshift (g : G) (f : G →ᵇ ℂ) : G →ᵇ ℂ :=
…
```
lemma OAI.PlaneFiveColor.InvariantMean.cshift_apply line 354
lemma OAI.PlaneFiveColor.InvariantMean.cmean_shift line 356
def OAI.PlaneFiveColor.InvariantMean.circlePull line 364
Source documentation
Pullback along the dense algebraic circle embedding.
```
def circlePull (ρ : G →+ UnitAddCircle) (f : C(UnitAddCircle, ℂ)) : G →ᵇ ℂ :=
…
```
lemma OAI.PlaneFiveColor.InvariantMean.circlePull_apply line 368
lemma OAI.PlaneFiveColor.InvariantMean.circlePull_norm_le line 371
def OAI.PlaneFiveColor.InvariantMean.circleMean line 376
lemma OAI.PlaneFiveColor.InvariantMean.circleMean_apply line 384
def OAI.PlaneFiveColor.InvariantMean.circleIntegral line 388
Source documentation
Normalized Haar integral on the ordinary circle.
```
def circleIntegral : C(UnitAddCircle, ℂ) →L[ℂ] ℂ :=
…
```
lemma OAI.PlaneFiveColor.InvariantMean.circleIntegral_apply line 402
lemma OAI.PlaneFiveColor.InvariantMean.circleMean_fourier_nonzero line 407
Source documentation
An ordinary nonconstant Fourier monomial has zero mean as soon as its half-period is represented in the discrete group.
```
lemma circleMean_fourier_nonzero (ρ : G →+ UnitAddCircle) {n : ℤ} (hn : n ≠ 0)
    (hρ : ∃ g, ρ g = ((1 / 2 / n : ℝ) : UnitAddCircle)) : circleMean ρ (fourier n) = 0 := by
…
```
Mentions: OAI.PlaneFiveColor.InvariantMean.circleMean
theorem OAI.PlaneFiveColor.InvariantMean.circleMean_eq_integral line 422
abbrev OAI.PlaneFiveColor.InvariantMean.AF line 441
Source documentation
The real algebraic field and the literal discrete quotient F/Z.
```
abbrev AF := algebraicClosure ℚ ℝ
```
def OAI.PlaneFiveColor.InvariantMean.PeriodGroup line 443
instance OAI.PlaneFiveColor.InvariantMean.(instance at line 444) line 444
instance OAI.PlaneFiveColor.InvariantMean.(instance at line 445) line 445
def OAI.PlaneFiveColor.InvariantMean.periodMk line 447
def OAI.PlaneFiveColor.InvariantMean.fieldCircle line 450
Source documentation
The ordinary circle quotient map, before passage to F/Z.
```
def fieldCircle : AF →+ UnitAddCircle :=
…
```
Mentions: OAI.PlaneFiveColor.InvariantMean.AF
lemma OAI.PlaneFiveColor.InvariantMean.fieldCircle_apply line 454
def OAI.PlaneFiveColor.InvariantMean.periodMap line 457
Source documentation
F/Z embeds in the ordinary circle; no ordinary topology is imposed on its source.
```
def periodMap : PeriodGroup →+ UnitAddCircle :=
…
```
Mentions: OAI.PlaneFiveColor.InvariantMean.PeriodGroup
lemma OAI.PlaneFiveColor.InvariantMean.periodMap_apply line 463
lemma OAI.PlaneFiveColor.InvariantMean.periodMap_half_period line 466
theorem OAI.PlaneFiveColor.InvariantMean.ordinary_mean_integral line 473
Source documentation
The exact identification of the chosen mean on ordinary continuous periodic functions asserted in spectral.tex113–123.
```
theorem ordinary_mean_integral (f : C(UnitAddCircle, ℂ)) :
    cmean (circlePull periodMap f) = ∫ x, f x ∂haarAddCircle :=
…
```
Mentions: OAI.PlaneFiveColor.InvariantMean.cmean, OAI.PlaneFiveColor.InvariantMean.circlePull, OAI.PlaneFiveColor.InvariantMean.periodMap
lemma OAI.PlaneFiveColor.InvariantMean.mean_mono line 477
lemma OAI.PlaneFiveColor.InvariantMean.mean_abs_le line 483
def OAI.PlaneFiveColor.InvariantMean.normFn line 496
Source documentation
Norm of a bounded vector field, still an arbitrary bounded function on this discrete domain.
```
def normFn (V : G →ᵇ H) : G →ᵇ ℝ :=
…
```
lemma OAI.PlaneFiveColor.InvariantMean.normFn_apply line 501
def OAI.PlaneFiveColor.InvariantMean.pairing line 503
lemma OAI.PlaneFiveColor.InvariantMean.pairing_apply line 507
lemma OAI.PlaneFiveColor.InvariantMean.pairing_mean_bound line 510
def OAI.PlaneFiveColor.InvariantMean.pairingMean line 517
def OAI.PlaneFiveColor.InvariantMean.weakMean line 538
Source documentation
Hilbert-space weak mean; it exists by the proved scalar mean and Riesz, without any real-variable measurability assumption on V.
```
def weakMean (V : G →ᵇ H) : H := (InnerProductSpace.toDual ℝ H).symm (pairingMean V)
```
Mentions: OAI.PlaneFiveColor.InvariantMean.pairingMean
lemma OAI.PlaneFiveColor.InvariantMean.weakMean_pair line 540
lemma OAI.PlaneFiveColor.InvariantMean.weakMean_norm_bound line 544
lemma OAI.PlaneFiveColor.InvariantMean.weakMean_add line 551
lemma OAI.PlaneFiveColor.InvariantMean.weakMean_sub line 559
lemma OAI.PlaneFiveColor.InvariantMean.weakMean_shift line 568
lemma OAI.PlaneFiveColor.InvariantMean.weakMean_map line 575
def OAI.PlaneFiveColor.InvariantMean.periodSum line 592
Source documentation
Periodization is defined for all functions; bounded support below ensures that these sums are finite and uniformly bounded.
```
def periodSum (h : AF → H) (t : AF) : H := ∑' k : ℤ, h (t + k)
```
Mentions: OAI.PlaneFiveColor.InvariantMean.AF
lemma OAI.PlaneFiveColor.InvariantMean.periodSum_periodic line 594
def OAI.PlaneFiveColor.InvariantMean.periodLift line 607
Source documentation
Literal quotient-valued periodization.
```
def periodLift (h : AF → H) : PeriodGroup → H := (periodSum_periodic h).lift
```
Mentions: OAI.PlaneFiveColor.InvariantMean.AF, OAI.PlaneFiveColor.InvariantMean.PeriodGroup, OAI.PlaneFiveColor.InvariantMean.periodSum_periodic
lemma OAI.PlaneFiveColor.InvariantMean.periodLift_mk line 609

lemma OAI.PlaneFiveColor.InvariantMean.period_term_zero line 614

Source documentation

A uniform finite interval of integers contains all summands after the argument has been moved to [0,1).

lemma period_term_zero {h : AF → H} {N : ℕ}
    (hs : ∀ t : AF, (N : ℝ) < |(t : ℝ)| → h t = 0)
    {t : AF} (ht0 : 0 ≤ (t : ℝ)) (ht1 : (t : ℝ) < 1) (k : ℤ)
    (hk : k ∉ Finset.Icc (-(N : ℤ)-2) ((N : ℤ)+2)) : h (t+k) = 0 := by
…

Mentions: OAI.PlaneFiveColor.InvariantMean.AF

lemma OAI.PlaneFiveColor.InvariantMean.periodSum_norm_le line 627
def OAI.PlaneFiveColor.InvariantMean.periodBCF line 646
Source documentation
Every bounded, boundedly supported vector function has a bounded periodization on the discrete quotient F/Z.
```
def periodBCF (h : AF → H) {N : ℕ} {B : ℝ}
    (hs : ∀ t : AF, (N : ℝ) < |(t : ℝ)| → h t = 0)
    (hb : ∀ t, ‖h t‖ ≤ B) : PeriodGroup →ᵇ H :=
…
```
Mentions: OAI.PlaneFiveColor.InvariantMean.AF, OAI.PlaneFiveColor.InvariantMean.PeriodGroup

lemma OAI.PlaneFiveColor.InvariantMean.period_summable line 655

Source documentation

Absolute finiteness of each period sum.

lemma period_summable {h : AF → H} {N : ℕ}
    (hs : ∀ t : AF, (N : ℝ) < |(t : ℝ)| → h t = 0) (t : AF) :
    Summable (fun k : ℤ => h (t+k)) := by
…

Mentions: OAI.PlaneFiveColor.InvariantMean.AF

lemma OAI.PlaneFiveColor.InvariantMean.periodSum_add line 676
lemma OAI.PlaneFiveColor.InvariantMean.periodSum_shift line 682
lemma OAI.PlaneFiveColor.InvariantMean.periodBCF_mk line 689
lemma OAI.PlaneFiveColor.InvariantMean.periodBCF_norm_le line 694
def OAI.PlaneFiveColor.InvariantMean.integralReal line 705
Source documentation
The scalar invariant integral in the manuscript, literally the invariant mean of the period sum on F/Z.
```
def integralReal (h : AF → ℝ) {N : ℕ} {B : ℝ}
    (hs : ∀ t : AF, (N : ℝ) < |(t : ℝ)| → h t = 0)
    (hb : ∀ t, ‖h t‖ ≤ B) : ℝ := mean (periodBCF h hs hb)
```
Mentions: OAI.PlaneFiveColor.InvariantMean.AF, OAI.PlaneFiveColor.InvariantMean.mean, OAI.PlaneFiveColor.InvariantMean.periodBCF
def OAI.PlaneFiveColor.InvariantMean.integralComplex line 709
lemma OAI.PlaneFiveColor.InvariantMean.integralReal_nonneg line 713
lemma OAI.PlaneFiveColor.InvariantMean.integralReal_shift line 721
lemma OAI.PlaneFiveColor.InvariantMean.integralReal_mono line 735
def OAI.PlaneFiveColor.InvariantMean.weakIntegral line 750
Source documentation
Hilbert-space weak invariant integral of bounded, boundedly supported functions, with no ordinary real-variable measurability hypothesis.
```
def weakIntegral (h : AF → H) {N : ℕ} {B : ℝ}
    (hs : ∀ t : AF, (N : ℝ) < |(t : ℝ)| → h t = 0)
    (hb : ∀ t, ‖h t‖ ≤ B) : H := weakMean (periodBCF h hs hb)
```
Mentions: OAI.PlaneFiveColor.InvariantMean.AF, OAI.PlaneFiveColor.InvariantMean.weakMean, OAI.PlaneFiveColor.InvariantMean.periodBCF
lemma OAI.PlaneFiveColor.InvariantMean.weakIntegral_pair line 754
lemma OAI.PlaneFiveColor.InvariantMean.weakIntegral_norm_bound line 767
lemma OAI.PlaneFiveColor.InvariantMean.weakIntegral_shift line 777
lemma OAI.PlaneFiveColor.InvariantMean.weakIntegral_sub line 793
lemma OAI.PlaneFiveColor.InvariantMean.weakIntegral_map line 808

lemma OAI.PlaneFiveColor.InvariantMean.compact_local_summable line 829

Source documentation

Compact support makes all local norm sums finite, before any interchange of sums, evaluations or integrals.

lemma compact_local_summable (f : C(ℝ, ℂ)) {N : ℕ}
    (hs : ∀ t : ℝ, (N : ℝ) < |t| → f t = 0) (K : Compacts ℝ) :
    Summable (fun k : ℤ => ‖(f.comp (ContinuousMap.addRight k)).restrict K‖) := by
…

def OAI.PlaneFiveColor.InvariantMean.ordinaryPeriod line 856
Source documentation
The ordinary continuous periodic function associated with a test function. Continuous-map summation agrees pointwise by local finiteness.
```
def ordinaryPeriod (f : C(ℝ, ℂ)) : C(UnitAddCircle, ℂ) :=
…
```
lemma OAI.PlaneFiveColor.InvariantMean.ordinaryPeriod_apply line 860
theorem OAI.PlaneFiveColor.InvariantMean.integralComplex_ordinary line 870
Source documentation
Exact agreement of the manuscript's invariant integral with the usual Lebesgue integral on every continuous boundedly supported test function.
```
theorem integralComplex_ordinary (f : C(ℝ, ℂ)) {N : ℕ} {B : ℝ}
    (hs : ∀ t : ℝ, (N : ℝ) < |t| → f t = 0) (hb : ∀ t, ‖f t‖ ≤ B) :
    integralComplex (fun t : AF => f t) (fun t ht => hs t ht) (fun t => hb t) =
      ∫ t : ℝ, f t := by
…
```
Mentions: OAI.PlaneFiveColor.InvariantMean.integralComplex, OAI.PlaneFiveColor.InvariantMean.AF
lemma OAI.PlaneFiveColor.InvariantMean.integralComplex_re line 889
theorem OAI.PlaneFiveColor.InvariantMean.integralReal_ordinary line 903
lemma OAI.PlaneFiveColor.InvariantMean.weakIntegral_congr line 926
lemma OAI.PlaneFiveColor.InvariantMean.shifted_support line 938
lemma OAI.PlaneFiveColor.InvariantMean.smoothed_support line 953
lemma OAI.PlaneFiveColor.InvariantMean.smoothed_bound line 960
def OAI.PlaneFiveColor.InvariantMean.smoothedVector line 966

theorem OAI.PlaneFiveColor.InvariantMean.smoothed_translation_bound line 974

Source documentation

Translation continuity of smoothing rests only on regularity of the scalar window, not on any measurability of the discrete representation.

theorem smoothed_translation_bound
    (hu : ∀ s t v, U s (U t v) = U (s+t) v)
    (φ : AF → ℝ) {N : ℕ} {B C : ℝ}
    (hφ : ∀ t : AF, (N : ℝ) < |(t : ℝ)| → φ t = 0)
    (hb : ∀ t, |φ t| ≤ B) (v : H) (s : AF) (hs : |(s : ℝ)| ≤ 1)
    (hC : 0 ≤ C) (hd : ∀ t, |φ (t-s)-φ t| ≤ C) :
    ‖U s (smoothedVector U φ hφ hb v) - smoothedVector U φ hφ hb v‖ ≤
      (Finset.Icc (-((N+1 : ℕ) : ℤ)-2) (((N+1 : ℕ) : ℤ)+2)).card * (C * ‖v‖) := by
…

Mentions: OAI.PlaneFiveColor.InvariantMean.AF, OAI.PlaneFiveColor.InvariantMean.smoothedVector

theorem OAI.PlaneFiveColor.InvariantMean.smoothed_tendsto line 1033

Source documentation

Every uniformly continuous compact window produces a strongly continuous vector even for a completely discontinuous representation of the discrete F.

theorem smoothed_tendsto
    (hu : ∀ s t v, U s (U t v) = U (s+t) v)
    (φ : ℝ → ℝ) (hc : UniformContinuous φ) {N : ℕ} {B : ℝ}
    (hφ : ∀ t : ℝ, (N : ℝ) < |t| → φ t = 0)
    (hb : ∀ t, |φ t| ≤ B) (v : H) :
    Tendsto (fun s : AF => U s
      (smoothedVector U (fun t => φ t) (fun t ht => hφ t ht) (fun t => hb t) v))
      (𝓝 0) (𝓝 (smoothedVector U (fun t => φ t)
        (fun t ht => hφ t ht) (fun t => hb t) v)) := by
…

Mentions: OAI.PlaneFiveColor.InvariantMean.AF, OAI.PlaneFiveColor.InvariantMean.smoothedVector