OAI/Combinatorics/PlanarL1/OrdinaryState.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarL1.Columns.Model.SetSystem.pullback line 17

    Source documentation

    Change label coordinates only: every individual set and component graph is pulled back, and the upper invariant is transported by the actual measure.

    noncomputable def pullback (A : SetSystem M Ω μ) {g : Ω' → Ω}
    (hg : MeasurePreserving g μ' μ) : SetSystem M Ω' μ' where
…

    Mentions: OAI.PlanarL1.Columns.Model.SetSystem

  2. def OAI.PlanarL1.Columns.Model.SetSystem.lift line 35
  3. lemma OAI.PlanarL1.Columns.Model.SetSystem.lift_active line 38
  4. def OAI.PlanarL1.Columns.Model.Field.constant line 45
  5. structure OAI.PlanarL1.Columns.Model.OrdinaryData line 54

    Source documentation

    The literal ordinary-chart scalar data. A nonconstant chart remembers its old band component and its one point source, rather than just a Lipschitz bound. The zero extension outside that component is never used on the chart's region.

    structure OrdinaryData {n : ℕ} (M : Model n) where
…

    Mentions: OAI.PlanarL1.Columns.Model

  6. def OAI.PlanarL1.Columns.Model.OrdinaryData.comparison line 66
  7. def OAI.PlanarL1.Columns.Model.OrdinaryData.value line 71
  8. lemma OAI.PlanarL1.Columns.Model.OrdinaryData.vertical line 74
  9. lemma OAI.PlanarL1.Columns.Model.OrdinaryData.switch line 86
  10. def OAI.PlanarL1.Columns.Model.OrdinaryData.field line 90
  11. def OAI.PlanarL1.Columns.Model.OrdinaryData.initial line 93
  12. lemma OAI.PlanarL1.Columns.Model.OrdinaryData.initial_value line 102
  13. def OAI.PlanarL1.Columns.Model.OrdinaryData.atom line 107

    Source documentation

    Conversion of an actual signed atom back to the old ordinary orientation.

    noncomputable def atom (D : OrdinaryData M) (J : Set ℝ) (hJ : IsClosed J)
    (hc : J.OrdConnected) {r : Fin n} (o : M.Point J r) (c η : ℝ) (hη : |η| = 1) :
    OrdinaryData M where
…

    Mentions: OAI.PlanarL1.Columns.Model.OrdinaryData

  14. lemma OAI.PlanarL1.Columns.Model.OrdinaryData.atom_value line 118
  15. structure OAI.PlanarL1.Columns.Model.OrdinaryState line 131

    Source documentation

    A finite ordinary chart partition for system A, with the actual globally nested sets and actual jointly distributed label variables. Chart regions may be disconnected; no artificial connected-component identifiers are introduced.

    structure OrdinaryState {n : ℕ} (M : Model n) (κ : ℝ) (Ω : Type*)
    [MeasurableSpace Ω] (μ : Measure Ω) where
…

    Mentions: OAI.PlanarL1.Columns.Model

  16. def OAI.PlanarL1.Columns.Model.OrdinaryState.initial line 149
  17. def OAI.PlanarL1.Columns.Model.OrdinaryState.lift line 164
  18. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.chart_distance line 178

    Source documentation

    Deterministic chart distance on a common identifier, with no independence assumed between different identifiers.

    lemma chart_distance (S : OrdinaryState M κ Ω μ) (i j : Fin n) (H T : ℝ)
    (he : S.name i H=S.name j T) :
    (∫ ω, |(S.sets.activity ω).indicator i H-(S.sets.activity ω).indicator j T| ∂μ) =
      max |H-T| |κ*(S.chart (S.name i H)).value i ⟨H,S.height_in i H⟩-
        κ*(S.chart (S.name j T)).value j ⟨T,S.height_in j T⟩| := by
…

    Mentions: OAI.PlanarL1.Columns.Model.OrdinaryState

  19. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.atomName_depth_eq line 201
  20. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.portalAt_mem line 214
  21. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.node_eq_of_portal_column line 220
  22. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.nodeAtom_eq_global line 228

    Source documentation

    A name is global to the whole interpolation tree, not only a chosen chain. Different node occurrences cannot silently give one identifier two fields.

    lemma nodeAtom_eq_global (p : M.Point J root → ℝ) (α : Noise (n := n))
…

    Mentions: OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

  23. structure OAI.PlanarL1.Columns.Model.Point.RadialTree.AtomSource line 240

    Source documentation

    The exact portal occurrence from which an atom identifier originates.

    structure AtomSource (a : ℕ) where
…
  24. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.pasted_has_source line 247
  25. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.pasted_name_lt line 253
  26. def OAI.PlanarL1.Columns.Model.Point.RadialTree.AtomSource.eval line 261
  27. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.AtomSource.eval_eq line 265
  28. def OAI.PlanarL1.Columns.Model.Point.RadialTree.AtomSource.center line 270
  29. def OAI.PlanarL1.Columns.Model.Point.RadialTree.AtomSource.intercept line 272
  30. def OAI.PlanarL1.Columns.Model.Point.RadialTree.AtomSource.sign line 277
  31. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.AtomSource.sign_unit line 279
  32. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.AtomSource.eval_formula line 283
  33. def OAI.PlanarL1.Columns.Model.Point.RadialTree.AtomSource.chart line 291

    Source documentation

    Convert back to the old ordinary orientation, as in /main-packing. The -4E proposal shift is part of the literal atom constant.

    noncomputable def chart (S : R.AtomSource a) (D : OrdinaryData M)
    (p : M.Point J root → ℝ) (α : Noise (n := n)) (E : ℝ) : OrdinaryData M :=
…

    Mentions: OAI.PlanarL1.Columns.Model.OrdinaryData, OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

  34. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.AtomSource.chart_value line 295
  35. def OAI.PlanarL1.Columns.Model.Point.RadialTree.atomChart line 307

    Source documentation

    A finite globally consistent chart table for every possible spatial atom. Unused identifiers get a constant chart and can never be selected by pasted.

    noncomputable def atomChart (D : OrdinaryData M) (p : M.Point J root → ℝ)
    (α : Noise (n := n)) (E : ℝ) (a : ℕ) : OrdinaryData M := by
…

    Mentions: OAI.PlanarL1.Columns.Model.OrdinaryData, OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

  36. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.source_eval_pasted line 312
  37. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.atomChart_value line 322
  38. def OAI.PlanarL1.Columns.Model.OrdinaryState.append line 347

    Source documentation

    Finite chart-table extension. Old identifiers are literally retained in the right summand; installing a fresh chart never refines the old regions.

    noncomputable def append (S : OrdinaryState M κ Ω μ) (B : SetSystem M Ω μ)
    (k : ℕ) (D : Fin k → OrdinaryData M) (Z : Fin k → Threshold.Variables Ω μ)
    (choose : Fin n → ℝ → Option (Fin k))
    (hin : ∀ i H a, choose i H = some a → H ∈ (D a).band)
    (hcomp : ∀ i H a (_hc : choose i H = some a) r o,
      (D a).origin = some ⟨r,o⟩ → (M.activeGraph (D a).band).Reachable r i)
    (hswitch : ∀ i j H, H ∈ M.heights i j → choose i H = choose j H)
    (hold : ∀ ω i H, choose i H = none →
      ((B.activity ω).active i H ↔ (S.sets.activity ω).active i H))
    (hnew : ∀ ω i H a (hc : choose i H = some a),
      ((B.activity ω).active i H ↔ Threshold.active (Z a) H
        (κ*(D a).value i ⟨H,hin i H a hc⟩) ω)) : OrdinaryState M κ Ω μ where
…

    Mentions: OAI.PlanarL1.Columns.Model.OrdinaryState, OAI.PlanarL1.Columns.Model.SetSystem, OAI.PlanarL1.Columns.Model.OrdinaryData, OAI.PlanarL1.Threshold.Variables, OAI.PlanarL1.Threshold.active

  39. def OAI.PlanarL1.Columns.Model.OrdinaryData.Contains line 427

    Source documentation

    The actual chart domain, with the connected-component requirement made explicit. Different copies of a quotient point satisfy the same condition.

    def Contains (D : OrdinaryData M) (i : Fin n) (H : ℝ) : Prop :=
…

    Mentions: OAI.PlanarL1.Columns.Model.OrdinaryData

  40. lemma OAI.PlanarL1.Columns.Model.OrdinaryData.initial_contains line 430
  41. lemma OAI.PlanarL1.Columns.Model.OrdinaryData.atom_contains line 435
  42. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.atomChart_contains line 452