OAI/Dynamics/SmoothObstruction/Obstruction.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SmoothObstruction.PairUpper.statistic_nonneg line 19
  2. lemma OAI.SmoothObstruction.PairUpper.statistic_le_one line 25
  3. theorem OAI.SmoothObstruction.PairUpper.integral_upper line 35

    Source documentation

    The upper bound is genuinely an integral in the original same-cell law. Entropies are the original input-observable entropies.

    theorem integral_upper (μ : Measure X) [IsProbabilityMeasure μ]
    (P : X → C) (hP : Measurable P)
    (U W : X → J → {v : V // v≠0}) (hU : Measurable U) (hW : Measurable W)
    (B : LinearMap.BilinForm (ZMod 2) V) (hB : B.Nondegenerate)
    (hentU : (249/250:ℝ)*Fintype.card J*Real.log (Fintype.card {v : V // v≠0})≤
      entropy (observed μ U hU))
    (hentW : (249/250:ℝ)*Fintype.card J*Real.log (Fintype.card {v : V // v≠0})≤
      entropy (observed μ W hW))
    (hC : Real.log (Fintype.card C)≤
      (3/500:ℝ)*Fintype.card J*Real.log (Fintype.card {v : V // v≠0}))
    (hlog : 1000*Real.log 2≤ Real.log (Fintype.card {v : V // v≠0})) :
    (∫ z,statistic B (U z.1) (W z.2) ∂(PairLaw.law μ P))≤ 31/50 := by
…

    Mentions: OAI.SmoothObstruction.PairUpper.statistic, OAI.SmoothObstruction.PairLaw.law

  4. theorem OAI.SmoothObstruction.PairUpper.integral_success_lower line 54

    Source documentation

    The success set is measured in the unconditioned law.

    theorem integral_success_lower (μ : Measure X) [IsProbabilityMeasure μ]
    (P : X → C) (hP : Measurable P)
    (U W : X → J → {v : V // v≠0}) (hU : Measurable U) (hW : Measurable W)
    (B : LinearMap.BilinForm (ZMod 2) V)
    (G : Set (X × X)) (hG : MeasurableSet G)
    (hGm : (19/20:ℝ) ≤ (PairLaw.law μ P).real G)
    (hZG : ∀ z∈G,(24/25:ℝ) ≤ statistic B (U z.1) (W z.2)) :
    (114/125:ℝ) ≤ ∫ z,statistic B (U z.1) (W z.2) ∂(PairLaw.law μ P) := by
…

    Mentions: OAI.SmoothObstruction.PairLaw.law, OAI.SmoothObstruction.PairUpper.statistic

  5. theorem OAI.SmoothObstruction.PairUpper.no_success_event line 78

    Source documentation

    Section7's two conflicting bounds are checked on the SAME original probability. In particular an event of mass .95 with value≥ .96 is impossible; no assertion of independence is made on that event or its complement.

    theorem no_success_event (μ : Measure X) [IsProbabilityMeasure μ]
    (P : X → C) (hP : Measurable P)
    (U W : X → J → {v : V // v≠0}) (hU : Measurable U) (hW : Measurable W)
    (B : LinearMap.BilinForm (ZMod 2) V) (hB : B.Nondegenerate)
    (hentU : (249/250:ℝ)*Fintype.card J*Real.log (Fintype.card {v : V // v≠0})≤
      entropy (observed μ U hU))
    (hentW : (249/250:ℝ)*Fintype.card J*Real.log (Fintype.card {v : V // v≠0})≤
      entropy (observed μ W hW))
    (hC : Real.log (Fintype.card C)≤
      (3/500:ℝ)*Fintype.card J*Real.log (Fintype.card {v : V // v≠0}))
    (hlog : 1000*Real.log 2≤ Real.log (Fintype.card {v : V // v≠0}))
    (G : Set (X × X)) (hG : MeasurableSet G)
…
  6. lemma OAI.SmoothObstruction.FiniteLaw.observed_preserving line 101
  7. lemma OAI.SmoothObstruction.WordHierarchy.firstList_entropy line 115
  8. lemma OAI.SmoothObstruction.WordHierarchy.advance_block line 130
  9. lemma OAI.SmoothObstruction.WordHierarchy.graph_firstLists line 139
  10. lemma OAI.SmoothObstruction.WordHierarchy.actual_passing_lower line 151
  11. lemma OAI.SmoothObstruction.WordHierarchy.graph_bad_small line 161
  12. lemma OAI.SmoothObstruction.WordHierarchy.alphabet_log_large line 175
  13. lemma OAI.SmoothObstruction.SwitchData.real_preimage_le line 190
  14. theorem OAI.SmoothObstruction.SwitchData.retain_statistic line 201

    Source documentation

    Null transport guards and the rare graph exception are removed from an already successful set using the ORIGINAL, unnormalized retained law.

    theorem retain_statistic (D : SwitchData μ)
    (hdom : D.retained.map D.point≤(2:ℝ≥0∞) • μ)
    (H : Set (M×M)) (hH : MeasurableSet H) (hHG : H⊆D.carrier)
    (hHm : (98/100:ℝ)≤D.law.real H)
    (B E : Set M) (hB : MeasurableSet B) (hE : MeasurableSet E)
    (hBc : μ Bᶜ=0) (hEc : μ.real Eᶜ≤1/1000) :
    ∃ K : Set (M×M),MeasurableSet K ∧ K⊆H ∧ (19/20:ℝ)≤D.law.real K ∧
      ∀ p∈K,p.1∈B ∧ p.2∈B ∧ D.point p∈B ∧ D.point p∈E := by
…

    Mentions: OAI.SmoothObstruction.SwitchData

  15. lemma OAI.SmoothObstruction.WordHierarchy.cell_cost line 252
  16. lemma OAI.SmoothObstruction.WordHierarchy.cheap_index_tendsto line 287
  17. def OAI.SmoothObstruction.WordHierarchy.initialSymbol line 299
  18. lemma OAI.SmoothObstruction.WordHierarchy.measurable_initialSymbol line 300
  19. lemma OAI.SmoothObstruction.WordHierarchy.iterate_forward_inverse line 304
  20. lemma OAI.SmoothObstruction.WordHierarchy.statistic_symm line 311
  21. lemma OAI.SmoothObstruction.WordHierarchy.pull_symbol line 329
  22. lemma OAI.SmoothObstruction.WordHierarchy.pull_past_symbol line 336
  23. lemma OAI.SmoothObstruction.WordHierarchy.pull_past_advance line 344
  24. lemma OAI.SmoothObstruction.WordHierarchy.transported_graph_bad line 350
  25. theorem OAI.SmoothObstruction.WordHierarchy.transported_success line 371

    Source documentation

    Conull guards, both full-half original names, and the graph test are joined in the ORIGINAL cell-weighted law. The two entries keep their original order.

    theorem transported_success (hT : MeasurePreserving T μ μ)
    (hB : MeasurableSet B) (hBc : ν Bᶜ=0)
    (i k : ℕ) (hk : k ≤ K (S i)/8) (hQ : 2 ≤ 2^k)
    (D : SwitchData ν) (hdom : D.retained.map D.point≤(2:ℝ≥0∞) • ν)
    (H : Set (M×M)) (hH : MeasurableSet H) (hHG : H⊆D.carrier)
    (hHm : (98/100:ℝ)≤D.law.real H)
    (hgood : ∀ p∈H,
      (mismatches (fun t : Fin (2^k*length 40000 i) => initialSymbol (r ((R^[t.val]) p.1)))
        (fun t : Fin (2^k*length 40000 i) => initialSymbol (r ((R^[t.val]) (D.point p)))):ℝ)<
          (3/400:ℝ)*(2^k*length 40000 i) ∧
      (mismatches (fun t : Fin (2^k*length 40000 i) => initialSymbol (r ((R.symm^[2^k*length 40000 i-t.val]) p.2)))
        (fun t : Fin (2^k*length 40000 i) => initialSymbol (r ((R.symm^[2^k*length 40000 i-t.val]) (D.point p)))):ℝ)<
…

    Mentions: OAI.SmoothObstruction.WordHierarchy.T, OAI.SmoothObstruction.WordHierarchy.S, OAI.SmoothObstruction.SwitchData, OAI.SmoothObstruction.WordHierarchy.initialSymbol

  26. theorem OAI.SmoothObstruction.WordHierarchy.no_switching line 438

    Source documentation

    The obstruction for the genuine word extension, using the entire smooth switching property and exact invariant-conull transport, not a factor-only or globally defined conjugacy substitute.

    theorem no_switching {M : Type} [MetricSpace M] [CompactSpace M]
    [MeasurableSpace M] [BorelSpace M] [Nonempty M]
    (μ : Measure Extension) [IsProbabilityMeasure μ] (hT : MeasurePreserving T μ μ)
    (ν : Measure M) [IsProbabilityMeasure ν]
    (R : M ≃ M) (hR : MeasurePreserving R ν ν) (hRi : MeasurePreserving R.symm ν ν)
    (r : M → Extension) (hr : MeasurePreserving r ν μ)
    (B : Set M) (hB : MeasurableSet B) (hBc : ν Bᶜ=0) (hBinv : R.symm ⁻¹' B=B)
    (hforward : ∀ t,∀ x∈B,r ((R^[t]) x)=(T^[t]) (r x))
    (hswitch : SmoothSwitching ν R R.symm) : False := by
…

    Mentions: OAI.SmoothObstruction.WordHierarchy.Extension, OAI.SmoothObstruction.WordHierarchy.T, OAI.SmoothObstruction.SmoothSwitching