StationaryGauge.lean`

29 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SmoothObstruction.GoodStationary.floorAt line 19
Source documentation
The literal geometric floor used throughout the source.
```
noncomputable def floorAt (k : ℕ) : ℝ := (2 : ℝ) ^ (-(k : ℝ) / 10)
```
lemma OAI.SmoothObstruction.GoodStationary.floorAt_pos line 21
lemma OAI.SmoothObstruction.GoodStationary.floorAt_sq line 23
lemma OAI.SmoothObstruction.GoodStationary.floorAt_square_summable line 30
def OAI.SmoothObstruction.GoodStationary.bAt line 39
Source documentation
Here a h is the sum over the diagonal coordinates of the dyadic squared chord errors. Its square root replaces the optional convolution upper bound in the manuscript's example of the choice of sequence.
```
noncomputable def bAt (η : ℝ) (a : ℕ → ℝ) (k : ℕ) : ℝ :=
…
```
lemma OAI.SmoothObstruction.GoodStationary.bAt_floor line 42
lemma OAI.SmoothObstruction.GoodStationary.bAt_pos line 47
lemma OAI.SmoothObstruction.GoodStationary.bAt_square_summable line 50
lemma OAI.SmoothObstruction.GoodStationary.error_ratio line 62
def OAI.SmoothObstruction.GoodStationary.jointEnergy line 83
lemma OAI.SmoothObstruction.GoodStationary.jointEnergy_nonneg line 87
lemma OAI.SmoothObstruction.GoodStationary.jointEnergy_summable line 90
def OAI.SmoothObstruction.GoodStationary.Good line 97
Source documentation
A finite set of forward chord inequalities. Centered integer intervals are precisely these sets pulled back by the negative iterate of a homeomorphism.
```
def Good {d : ℕ} (T : Ω → Ω) (f : Fin d → Ω → ℝ) (k : ℕ) (b : ℝ) : Set Ω :=
…
```
lemma OAI.SmoothObstruction.GoodStationary.good_iff_deviation line 101
theorem OAI.SmoothObstruction.GoodStationary.bad_measure line 121
Source documentation
Quantitative squared Markov bound for all coordinate chords together. The measure is UNNORMALIZED; no conditioning of the original law occurs.
```
theorem bad_measure {d : ℕ} {T : Ω → Ω} (hT : MeasurePreserving T μ μ)
    {f : Fin d → Ω → ℝ} (hf : ∀ j, MemLp (f j) 2 μ)
    {b : ℝ} (hb : 0 < b) (k : ℕ) :
    μ (Good T f k b)ᶜ ≤ ENNReal.ofReal (4 * jointEnergy T f μ (k + 1) / b^2) := by
…
```
Mentions: OAI.SmoothObstruction.GoodStationary.Good, OAI.SmoothObstruction.GoodStationary.jointEnergy

theorem OAI.SmoothObstruction.GoodStationary.good_segments line 157

Source documentation

The actual simultaneous good-segment sequence, not an assumed rate of convergence. No ergodicity or rate assumption is used.

theorem good_segments {d : ℕ} {T : Ω → Ω} (hT : MeasurePreserving T μ μ)
    {f : Fin d → Ω → ℝ} (hf : ∀ j, MemLp (f j) 2 μ) {η : ℝ} (hη : 0 < η) :
    ∃ b : ℕ → ℝ, (∀ k, 0 < b k) ∧ (∀ k, floorAt k ≤ b k) ∧
      Summable (fun k => (b k)^2) ∧
      ∀ k, μ (Good T f k (b k))ᶜ ≤ ENNReal.ofReal (η / 400) := by
…

Mentions: OAI.SmoothObstruction.GoodStationary.floorAt, OAI.SmoothObstruction.GoodStationary.Good

lemma OAI.SmoothObstruction.GoodStationary.chord_continuous line 173
lemma OAI.SmoothObstruction.GoodStationary.good_isClosed line 180

theorem OAI.SmoothObstruction.GoodStationary.compact_good_segments line 196

Source documentation

Compact good sets, with the source's 1−η/100 lower bound. The proof actually gives 1−η/400. The displayed natural-coordinate block has length 2^(k+1), corresponding to the source's centered block [-2^k,2^k).

theorem compact_good_segments {d : ℕ} {T : Ω → Ω} (hT : MeasurePreserving T μ μ)
    (hTc : Continuous T) {f : Fin d → Ω → ℝ} (hf : ∀ j, Continuous (f j))
    {η : ℝ} (hη : 0 < η) :
    ∃ b : ℕ → ℝ, (∀ k, 0 < b k) ∧ (∀ k, floorAt k ≤ b k) ∧
      Summable (fun k => (b k)^2) ∧ ∀ k,
      IsCompact (Good T f k (b k)) ∧ 1 - η / 100 ≤ μ.real (Good T f k (b k)) := by
…

Mentions: OAI.SmoothObstruction.GoodStationary.floorAt, OAI.SmoothObstruction.GoodStationary.Good

def OAI.SmoothObstruction.GoodStationary.CenteredGood line 214
Source documentation
The actual centered good set, with the left endpoint at time −2^k.
```
def CenteredGood {d : ℕ} (S : Ω ≃ₜ Ω) (f : Fin d → Ω → ℝ) (k : ℕ) (b : ℝ) : Set Ω :=
…
```
lemma OAI.SmoothObstruction.GoodStationary.centeredGood_isClosed line 218
lemma OAI.SmoothObstruction.GoodStationary.centeredGood_measure line 226
Source documentation
Centering does not alter the measure, since the inverse as well as the forward transformation preserves the original measure.
```
lemma centeredGood_measure {d : ℕ} {S : Ω ≃ₜ Ω} (hS : MeasurePreserving S μ μ)
    {f : Fin d → Ω → ℝ} (hf : ∀ j, Continuous (f j)) (k : ℕ) (b : ℝ) :
    μ.real (CenteredGood S f k b) = μ.real (Good S f k b) := by
…
```
Mentions: OAI.SmoothObstruction.GoodStationary.CenteredGood, OAI.SmoothObstruction.GoodStationary.Good
lemma OAI.SmoothObstruction.GoodStationary.subinterval_chord line 234

theorem OAI.SmoothObstruction.GoodStationary.compact_centered_good_segments line 254

Source documentation

The simultaneous compact centered good sets of the stationary part of Proposition good-frames. The geometric frame lift and its coordinate functions are not postulated here: this lemma takes any compact stationary system.

theorem compact_centered_good_segments {d : ℕ} {S : Ω ≃ₜ Ω}
    (hS : MeasurePreserving S μ μ) {f : Fin d → Ω → ℝ} (hf : ∀ j, Continuous (f j))
    {η : ℝ} (hη : 0 < η) :
    ∃ b : ℕ → ℝ, (∀ k, 0 < b k) ∧ (∀ k, floorAt k ≤ b k) ∧
      Summable (fun k => (b k)^2) ∧ ∀ k,
      IsCompact (CenteredGood S f k (b k)) ∧
      1 - η / 100 ≤ μ.real (CenteredGood S f k (b k)) := by
…

Mentions: OAI.SmoothObstruction.GoodStationary.floorAt, OAI.SmoothObstruction.GoodStationary.CenteredGood

theorem OAI.SmoothObstruction.GoodStationary.compact_projection_good line 270

Source documentation

Projection of a compact good set needs no measurable frame selection. The sole measure input is the genuine pushforward identity.

theorem compact_projection_good {Γ : Type*} [TopologicalSpace Ω] [CompactSpace Ω]
    [BorelSpace Ω] [IsProbabilityMeasure μ] [TopologicalSpace Γ] [T2Space Γ]
    [MeasurableSpace Γ] [BorelSpace Γ] {ν : Measure Γ} [IsProbabilityMeasure ν]
    {π : Ω → Γ} (hπ : Continuous π) (hpush : MeasurePreserving π μ ν)
    {G : Set Ω} (hG : IsCompact G) {a : ℝ} (ha : a ≤ μ.real G) :
    IsCompact (π '' G) ∧ a ≤ ν.real (π '' G) := by
…

def OAI.SmoothObstruction.OrbitCocycle.logDiagonal line 289
lemma OAI.SmoothObstruction.OrbitCocycle.continuous_logDiagonal line 293
theorem OAI.SmoothObstruction.OrbitCocycle.compact_actual_good line 302
Source documentation
The actual good-frame burden for a bounded coordinate cocycle is constructed from stationarity, with compactness restored inside the Borel full-measure genuine-code locus rather than asserted for a measurable graph. The projection uses the middle of each length-2n block.
```
theorem compact_actual_good (S : X ≃ₜ X) (A : X → CompactMatrix.Alphabet d K)
    (hA : Measurable A) (μ : ProbabilityMeasure X)
    (hS : MeasurePreserving S (μ : Measure X) (μ : Measure X))
    {η : ℝ} (hη : 0<η) :
    ∃ (ν : ProbabilityMeasure (Path (X:=X) (d:=d) (K:=K) × QR.Frame d))
…
```
Mentions: OAI.SmoothObstruction.CompactMatrix.Alphabet, OAI.SmoothObstruction.OrbitCocycle.Path, OAI.SmoothObstruction.QR.Frame

theorem OAI.SmoothObstruction.ManifoldCoordinates.manifold_good_frames line 376

Source documentation

Genuine manifold good frames, with no stationary-frame or bounded- cocycle assumption. The finite compact atlas, actual chart derivative, invariant QR lift, square-summable burden, and compact good base sets are all constructed. The model may have corners, in particular boundary.

theorem manifold_good_frames (S : Diffeomorph I I M M ∞)
    (μ : ProbabilityMeasure M) (hS : MeasurePreserving S (μ : Measure M) (μ : Measure M))
    {η : ℝ} (hη : 0<η) :
    ∃ (ι : Type u) (_ : Fintype ι) (_ : MeasurableSpace ι) (_ : MeasurableSingletonClass ι)
      (a : ι → M) (K : ι → Set M) (c : M → ι) (C : ℝ)
      (A : M → CompactMatrix.Alphabet d C),
      (∀ i,IsCompact (K i)) ∧ (∀ i,K i⊆(chartAt H (a i)).source) ∧
      Measurable c ∧ (∀ x,x∈K (c x)) ∧ 0<C ∧ Measurable A ∧
      (∀ x,(A x).val=coord I S (a (c x)) (a (c (S x))) x) ∧
      ∃ (ν : ProbabilityMeasure (OrbitCocycle.Path (X:=M) (d:=d) (K:=C) × QR.Frame d))
…

Mentions: OAI.SmoothObstruction.CompactMatrix.Alphabet, OAI.SmoothObstruction.ManifoldCoordinates.coord, OAI.SmoothObstruction.OrbitCocycle.Path, OAI.SmoothObstruction.QR.Frame