GridCells.lean`

31 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SmoothObstruction.GridMargin.street line 19
Source documentation
The deleted street for one of N translated grids of the same mesh Nδ.
```
def street (δ : ℝ) (N : ℕ) (k : Fin N) : Set ℝ :=
…
```
lemma OAI.SmoothObstruction.GridMargin.street_measurable line 22
lemma OAI.SmoothObstruction.GridMargin.centers_lt_eq line 28
lemma OAI.SmoothObstruction.GridMargin.street_disjoint line 39
theorem OAI.SmoothObstruction.GridMargin.exists_small_street line 62
Source documentation
A translated regular grid with a quantitative margin for an arbitrary probability law; no replacement of the law by a conditioned one.
```
theorem exists_small_street (μ : Measure ℝ) [IsProbabilityMeasure μ]
    {δ : ℝ} (hδ : 0<δ) {N : ℕ} (hN : 0<N) :
    ∃ k : Fin N,μ.real (street δ N k)≤(N:ℝ)⁻¹ := by
…
```
Mentions: OAI.SmoothObstruction.GridMargin.street
lemma OAI.SmoothObstruction.GridMargin.floor_stable line 82
Source documentation
Within a retained scalar cell, a perturbation less than the full margin cannot change the integer cell index.
```
lemma floor_stable {r a x y ε : ℝ} (hr : 0<r)
    (hx : ∀ j : ℤ,ε < |x-(a+r*j)|) (hxy : |y-x|≤ε) :
    ⌊(y-a)/r⌋=⌊(x-a)/r⌋ := by
…
```

theorem OAI.SmoothObstruction.GridMargin.exists_product_margins line 112

Source documentation

Simultaneous product-coordinate margins for the original probability, with no conditioning on a good set. Each coordinate gets one translation.

theorem exists_product_margins (μ : Measure X) [IsProbabilityMeasure μ]
    (c : X → ι → ℝ) (hc : ∀ i,Measurable (fun x =>  c x i))
    {δ : ℝ} (hδ : 0 < δ) {N : ℕ} (hN : 0 < N) :
    ∃ k : ι → Fin N,
      μ.real (⋃ i,(fun x =>  c x i) ⁻¹' street δ N (k i)) ≤ (Fintype.card ι:ℝ)/N := by
…

Mentions: OAI.SmoothObstruction.GridMargin.street

def OAI.SmoothObstruction.GridMargin.gridIndex line 132
Source documentation
The precise regular translated-grid label.
```
noncomputable def gridIndex (δ : ℝ) (N : ℕ) (k : Fin N) (x : ℝ) : ℤ :=
…
```
lemma OAI.SmoothObstruction.GridMargin.measurable_gridIndex line 135
lemma OAI.SmoothObstruction.GridMargin.gridIndex_stable line 138
def OAI.SmoothObstruction.GridMargin.boundedLabel line 149
Source documentation
Bounded integer labels are encoded without enlarging the physical cells.
```
def boundedLabel (m : ℕ) (j : ℤ) : Fin (2*m+1) :=
…
```
lemma OAI.SmoothObstruction.GridMargin.boundedLabel_inj line 152
lemma OAI.SmoothObstruction.GridMargin.floor_bounds line 159
def OAI.SmoothObstruction.GridMargin.productLabel line 169
Source documentation
Arbitrary bounded coordinates give a genuine finite measurable partition, with exactly this finite alphabet, rather than an assumed cardinal bound.
```
noncomputable def productLabel (m : ℕ) (δ : ℝ) (N : ℕ) (k : ι → Fin N)
    (c : X → ι → ℝ) (x : X) : ι → Fin (2*m+1) :=
…
```
lemma OAI.SmoothObstruction.GridMargin.measurable_productLabel line 174
lemma OAI.SmoothObstruction.GridMargin.productLabel_stable line 182
lemma OAI.SmoothObstruction.GridMargin.same_cell_coord line 192
lemma OAI.SmoothObstruction.GridMargin.productLabel_diameter line 204
lemma OAI.SmoothObstruction.GridMargin.productLabel_card line 215
theorem OAI.SmoothObstruction.GridMargin.exists_small_street_finite line 227
Source documentation
Each finite original measure admits the same translated-street estimate, scaled by its original total mass. This is used on partition fibres without changing the final pair law.
```
theorem exists_small_street_finite (μ : Measure ℝ) [IsFiniteMeasure μ]
    {δ : ℝ} (hδ : 0<δ) {N : ℕ} (hN : 0<N) :
    ∃ k : Fin N,μ.real (street δ N k)≤μ.real univ/(N:ℝ) := by
…
```
Mentions: OAI.SmoothObstruction.GridMargin.street

theorem OAI.SmoothObstruction.GridMargin.exists_product_margins_finite line 249

Source documentation

Simultaneous margins for a finite, not necessarily probability, law.

theorem exists_product_margins_finite (μ : Measure X) [IsFiniteMeasure μ]
    (c : X → ι → ℝ) (hc : ∀ i,Measurable (fun x => c x i))
    {δ : ℝ} (hδ : 0<δ) {N : ℕ} (hN : 0<N) :
    ∃ k : ι → Fin N,
      μ.real (⋃ i,(fun x => c x i) ⁻¹' street δ N (k i)) ≤
        (Fintype.card ι:ℝ)*μ.real univ/N := by
…

Mentions: OAI.SmoothObstruction.GridMargin.street

theorem OAI.SmoothObstruction.GridMargin.fibrewise_margins line 273

Source documentation

Independently translated grids in each fibre of a finite measurable partition retain the same original total-mass budget. The number of fibres does not multiply the loss.

theorem fibrewise_margins (μ : Measure X) [IsProbabilityMeasure μ]
    (P : X → C) (hP : Measurable P) (c : C → X → ι → ℝ)
    (hc : ∀ a i,Measurable (fun x => c a x i))
    {δ : ℝ} (hδ : 0<δ) {N : ℕ} (hN : 0<N) :
    ∃ k : C → ι → Fin N,
      μ.real (⋃ a,(P ⁻¹' {a}) ∩ ⋃ i,(fun x => c a x i) ⁻¹' street δ N (k a i)) ≤
        (Fintype.card ι:ℝ)/N := by
…

Mentions: OAI.SmoothObstruction.GridMargin.street

def OAI.SmoothObstruction.GridRefinement.label line 315
lemma OAI.SmoothObstruction.GridRefinement.measurable_label line 321

theorem OAI.SmoothObstruction.GridRefinement.exists_refinement line 335

Source documentation

A genuine finite coordinate-grid refinement, with original-measure loss independent of the number of base fibres. Stability is quantitative and the cardinality is the actual finite alphabet cardinality.

theorem exists_refinement (μ : Measure X) [IsProbabilityMeasure μ]
    (P : X → C) (hP : Measurable P) (c : C → X → ι → ℝ)
    (hc : ∀ a i,Measurable (fun x => c a x i))
    (m : ℕ) {δ : ℝ} (hδ : 0<δ) {N : ℕ} (hN : 0<N) :
    ∃ (k : C → ι → Fin N) (W : Set X),
      MeasurableSet W ∧ μ.real W≤(Fintype.card ι:ℝ)/N ∧
      Measurable (label P c m δ N k) ∧
      (∀ x y,x∉W → P y=P x →
        (∀ i,|c (P x) y i-c (P x) x i|≤δ/4) →
        label P c m δ N k y=label P c m δ N k x) ∧
      (∀ x y,label P c m δ N k x=label P c m δ N k y →
        (∀ i,|((c (P x) x i-δ*(k (P x) i).val)/(δ*N))|≤(m:ℝ)) →
…

Mentions: OAI.SmoothObstruction.GridRefinement.label

theorem OAI.SmoothObstruction.GridRefinement.exists_mixing_refinement line 387

Source documentation

The retained product margins survive a complementary coordinate mix. Each output coordinate may follow either retained input, so this applies simultaneously to both actual orbit joins. Mass is still the original law.

theorem exists_mixing_refinement (μ : Measure X) [IsProbabilityMeasure μ]
    (P : X → C) (hP : Measurable P) (c : C → X → ι → ℝ)
    (hc : ∀ a i,Measurable (fun x => c a x i))
    (m : ℕ) {δ : ℝ} (hδ : 0 < δ) {N : ℕ} (hN : 0 < N) :
    ∃ (k : C → ι → Fin N) (W : Set X),
      MeasurableSet W ∧ μ.real W ≤ (Fintype.card ι:ℝ)/N ∧
      Measurable (label P c m δ N k) ∧
      (∀ x y z,x∉W → y∉W →
        label P c m δ N k x=label P c m δ N k y → P z=P x →
        (∀ i,|c (P x) z i-c (P x) x i| ≤ δ/4 ∨
          |c (P x) z i-c (P x) y i| ≤ δ/4) →
        label P c m δ N k z=label P c m δ N k x) ∧
…

Mentions: OAI.SmoothObstruction.GridRefinement.label

lemma OAI.SmoothObstruction.ProductCells.norm_le_coords line 446
lemma OAI.SmoothObstruction.ProductCells.grid_range line 461

theorem OAI.SmoothObstruction.ProductCells.exists_cells line 481

Source documentation

Finite product cells for arbitrary measurable geometric coordinates. The original probability law loses at most d/N near product streets. The number of cells is exactly the finite grid alphabet; no rank or orbit code is counted. Stability is stated in the physical coordinates needed for joins.

theorem exists_cells (μ : Measure X) [IsProbabilityMeasure μ]
    (P : X → C) (hP : Measurable P) (φ : C → X → E)
    (hφ : ∀ c,Measurable (φ c)) (A : C → E ≃L[ℝ] E)
    {D H F δ : ℝ} (hD : 0≤D) (hH : 0≤H) (hF : 0≤F) (hδ : 0<δ)
    (hbound : ∀ x,‖φ (P x) x‖≤D)
    (hAi : ∀ c,‖(A c).symm.toContinuousLinearMap‖≤H)
    (hA : ∀ c,‖(A c).toContinuousLinearMap‖≤F)
    {N : ℕ} (hN : 0<N) :
    let m := ⌈H*D/(δ*N)+1⌉₊
…

theorem OAI.SmoothObstruction.ChartDensity.selected_coordinate_bound line 552
Source documentation
A uniform selected-coordinate bound follows from the compact atlas, without any regularity assumption on the selection itself.
```
theorem selected_coordinate_bound (a : ι → M) (K : ι → Set M)
    (hK : ∀ i,IsCompact (K i)) (hKU : ∀ i,K i⊆(chartAt H (a i)).source)
    (q : M → ι) (hqK : ∀ x,x∈K (q x)) :
    ∃ D : ℝ,1≤D ∧ ∀ x,‖coordinates I (a (q x)) x‖≤D := by
…
```
Mentions: OAI.SmoothObstruction.ChartDensity.coordinates

theorem OAI.SmoothObstruction.ChartDensity.exists_coarse_cells line 579

Source documentation

Genuine finite coarse bins in a compact atlas. Their translated margins are estimated using the ORIGINAL measure, with no assumptions about its interaction with the good gauge set. Only the selected starting chart is part of the finite alphabet.

theorem exists_coarse_cells [MeasurableSpace ι] [MeasurableSingletonClass ι]
    (μ : Measure M) [IsProbabilityMeasure μ]
    (a : ι → M) (K : ι → Set M)
    (hK : ∀ i,IsCompact (K i)) (hKU : ∀ i,K i⊆(chartAt H (a i)).source)
    (q : M → ι) (hq : Measurable q) (hqK : ∀ x,x∈K (q x)) :
    ∃ D : ℝ,1≤D ∧ ∀ {δ : ℝ},0<δ → ∀ {N : ℕ},0<N →
      let m := ⌈D/(δ*N)+1⌉₊
…