GridCompatibility.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Transferring almost-everywhere compatibility to actual grid choices

Independent shifts for distinct labels have the required finite product law. Each shifted grid level has a law absolutely continuous with respect to Haar measure on the circle. Consequently every completed-product null failure set remains null for actual grid tuples. Repeated levels of one label are not treated as independent; the tuple map explicitly requires distinct labels.

theorem OAI.CircleDomainRigidity.FiniteTransfer.absolutelyContinuous_pi_fin line 21

Source documentation

Absolute continuity passes to the finite products needed for level laws.

theorem absolutelyContinuous_pi_fin {T : Type*} [MeasurableSpace T] :
    ∀ (n : ℕ) (μ ν : Fin n → Measure T) [∀ i, SigmaFinite (μ i)] [∀ i, SigmaFinite (ν i)],
      (∀ i, μ i ≪ ν i) → Measure.pi μ ≪ Measure.pi ν := by
…

theorem OAI.CircleDomainRigidity.FiniteTransfer.quasiMeasurePreserving_translated_grid_level line 46
Source documentation
A uniform shift on a subinterval of a period, followed by any circle translation, has a Haar-absolutely-continuous law.
```
theorem quasiMeasurePreserving_translated_grid_level {h : ℝ}
    (_hh : 0 < h) (hsmall : h ≤ 1) (c : ℝ) :
    Measure.QuasiMeasurePreserving (fun θ : ℝ => ((θ + c : ℝ) : UnitAddCircle))
      (shiftLaw h) volume := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.shiftLaw

theorem OAI.CircleDomainRigidity.FiniteTransfer.quasiMeasurePreserving_grid_levels line 64

Source documentation

Finite products of the translated grid levels remain absolutely continuous with respect to independent Haar measure.

theorem quasiMeasurePreserving_grid_levels {n : ℕ} {h : ℝ}
    (hh : 0 < h) (hsmall : h ≤ 1) (c : Fin n → ℝ) :
    Measure.QuasiMeasurePreserving
      (fun θ : Fin n → ℝ => fun i => ((θ i + c i : ℝ) : UnitAddCircle))
      (Measure.pi (fun _ : Fin n => shiftLaw h))
      (Measure.pi (fun _ : Fin n => volume)) := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.shiftLaw

theorem OAI.CircleDomainRigidity.FiniteTransfer.measurePreserving_distinct_grid_labels line 78

Source documentation

Selecting distinct labels from an independent finite shift family preserves their product law.

theorem measurePreserving_distinct_grid_labels {m n : ℕ} {h : ℝ}
    (hh : 0 < h) (labels : Fin n → Fin m) (hinj : Injective labels) :
    MeasurePreserving (fun θ : Fin m → ℝ => fun j => θ (labels j))
      (Measure.pi (fun _ : Fin m => shiftLaw h))
      (Measure.pi (fun _ : Fin n => shiftLaw h)) := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.shiftLaw

theorem OAI.CircleDomainRigidity.FiniteTransfer.ae_grid_tuple_avoids_null_event line 93

Source documentation

Every completed-product null event is avoided almost surely by a chosen tuple of actual grid levels on distinct labels. Offsets may be any lattice offsets, since the proof allows every real translation.

theorem ae_grid_tuple_avoids_null_event {m d : ℕ} {h : ℝ}
    (hh : 0 < h) (hsmall : h ≤ 1) (labels : Fin (d + 1) → Fin m)
    (hinj : Injective labels) (c : Fin (d + 1) → ℝ)
    (E : Set (UnitAddCircle × (Fin d → UnitAddCircle)))
    (hE : (volume.prod (Measure.pi (fun _ : Fin d => volume))) E = 0) :
    ∀ᵐ θ ∂Measure.pi (fun _ : Fin m => shiftLaw h),
      (((θ (labels 0) + c 0 : ℝ) : UnitAddCircle),
        fun i : Fin d => ((θ (labels i.succ) + c i.succ : ℝ) : UnitAddCircle)) ∉ E := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.shiftLaw