SymbolCores.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SmoothObstruction.SymbolCores.compact_core line 16

Source documentation

A finite measurable observation is uniformly stable at nearby points of one compact core, losing arbitrarily little of the original probability.

theorem compact_core (μ : Measure M) [IsFiniteMeasure μ]
    (f : M → A) (hf : Measurable f) {κ : ℝ} (hκ : 0<κ) :
    ∃ (C : Set M) (δ : ℝ≥0), IsCompact C ∧ μ Cᶜ≤ENNReal.ofReal κ ∧
      0<δ ∧ ∀ x∈C,∀ y∈C,edist x y<(δ : ℝ≥0∞) → f x=f y := by
…

theorem OAI.SmoothObstruction.SymbolMass.mismatch_mass line 83

Source documentation

The per-time mismatch estimate in the original, unnormalized retained law. Only its actual dominated marginals are used.

theorem mismatch_mass (σ : Measure Ω) (μ : Measure M)
    (f : M → A) (C : Set M) (hC : IsClosed C) {δ : ℝ≥0}
    (hcore : ∀ x∈C,∀ y∈C,edist x y<(δ : ℝ≥0∞) → f x=f y)
    (u v : Ω → M) (hu : Measurable u) (hv : Measurable v)
    (a b : ℝ≥0∞) (hU : σ.map u≤a•μ) (hV : σ.map v≤b•μ)
    (hdist : ∀ᵐ ω ∂σ,edist (u ω) (v ω)<(δ : ℝ≥0∞)) :
    σ {ω | f (u ω)≠f (v ω)}≤(a+b)*μ Cᶜ := by
…

theorem OAI.SmoothObstruction.SymbolMass.transported_domination line 109

Source documentation

Invariance transports output domination to every observation time.

theorem transported_domination (σ : Measure Ω) (μ : Measure M)
    (z : Ω → M) (hz : Measurable z) (S : M → M)
    (hS : MeasurePreserving S μ μ) (a : ℝ≥0∞) (hzle : σ.map z≤a•μ) :
    σ.map (S ∘ z)≤a•μ := by
…

def OAI.SmoothObstruction.SymbolMass.errors line 125
Source documentation
Counted mismatches, before any normalization of the retained law.
```
noncomputable def errors (N : ℕ) (bad : Fin N → Set Ω) (ω : Ω) : ℝ≥0∞ :=
…
```
lemma OAI.SmoothObstruction.SymbolMass.measurable_errors line 128

theorem OAI.SmoothObstruction.SymbolMass.fraction_bad line 134

Source documentation

The finite-time Markov bound. The factor N cancels; no mixing in time and no renormalized law is required.

theorem fraction_bad (σ : Measure Ω) (N : ℕ) (hN : 0<N)
    (bad : Fin N → Set Ω) (hb : ∀ t,MeasurableSet (bad t))
    (ε θ : ℝ≥0∞) (hθ : θ≠0) (hθt : θ≠∞)
    (hm : ∀ t,σ (bad t)≤ε) :
    σ {ω | (N:ℝ≥0∞)*θ≤errors N bad ω}≤ε/θ := by
…

Mentions: OAI.SmoothObstruction.SymbolMass.errors

theorem OAI.SmoothObstruction.SymbolMass.two_halves_bad line 157

Source documentation

Both half-names lose at most twice the one-half Markov bound.

theorem two_halves_bad (σ : Measure Ω) (N : ℕ) (hN : 0<N)
    (bad₁ bad₂ : Fin N → Set Ω)
    (hb₁ : ∀ t,MeasurableSet (bad₁ t)) (hb₂ : ∀ t,MeasurableSet (bad₂ t))
    (ε θ : ℝ≥0∞) (hθ : θ≠0) (hθt : θ≠∞)
    (hm₁ : ∀ t,σ (bad₁ t)≤ε) (hm₂ : ∀ t,σ (bad₂ t)≤ε) :
    σ ({ω | (N:ℝ≥0∞)*θ≤errors N bad₁ ω} ∪
      {ω | (N:ℝ≥0∞)*θ≤errors N bad₂ ω})≤2*(ε/θ) := by
…

Mentions: OAI.SmoothObstruction.SymbolMass.errors

lemma OAI.SmoothObstruction.SymbolMass.errors_eq_mismatches line 180

theorem OAI.SmoothObstruction.SymbolMass.symbol_success line 193

Source documentation

Compact symbol cores give simultaneous full-half-name recovery with original (not conditionally normalized) mass at least .98.

theorem symbol_success (μ : Measure M) [IsProbabilityMeasure μ]
    (S Sinv : M → M) (hS : MeasurePreserving S μ μ) (hSi : MeasurePreserving Sinv μ μ)
    (f : M → A) (hf : Measurable f) :
    ∃ δ : ℝ,0<δ ∧ ∀ (D : SwitchData μ) (n : ℕ),0<n →
      (99/100:ℝ)≤D.law.real D.carrier → D.retained.map D.point≤(2:ℝ≥0∞) • μ →
      (∀ p∈D.carrier,∀ t v : Fin (n+1),
        dist (S^[t.val] (D.point p)) (S^[t.val] p.1)+
        dist (Sinv^[v.val] (D.point p)) (Sinv^[v.val] p.2)<δ) →
      ∃ H : Set (M×M),MeasurableSet H ∧ H⊆D.carrier ∧ (98/100:ℝ)≤D.law.real H ∧
        ∀ p∈H,
          (mismatches (fun t : Fin n => f (S^[t.val] p.1))
            (fun t : Fin n => f (S^[t.val] (D.point p))):ℝ)<(3/400:ℝ)*n ∧
…

Mentions: OAI.SmoothObstruction.SwitchData