OAI/Combinatorics/PlanarL1/Interpolation.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

The deterministic clamping core of thin-band interpolation

No probabilistic or geometric claim is assumed by these lemmas; they establish the scalar inequalities used at each actual node.

  1. def OAI.PlanarL1.Interpolation.nodeValue line 16

    Source documentation

    The exact parent/tentative clamp in the source: U=max parent A, L=min parent B, and F=min U (max L T).

    def nodeValue (parent upper lower tentative : ℝ) : ℝ :=
…
  2. theorem OAI.PlanarL1.Interpolation.nodeValue_collar line 21

    Source documentation

    Whenever both barrier cones exclude movement, an equality collar preserves the parent value exactly.

    theorem nodeValue_collar {parent upper lower tentative : ℝ}
    (hu : upper ≤ parent) (hl : parent ≤ lower) :
    nodeValue parent upper lower tentative = parent := by
…

    Mentions: OAI.PlanarL1.Interpolation.nodeValue

  3. theorem OAI.PlanarL1.Interpolation.nodeValue_bounds line 29

    Source documentation

    Clamping into an interval whose upper end is not too small and whose lower end is not too large preserves the claimed accuracy window.

    theorem nodeValue_bounds {parent upper lower tentative lo hi : ℝ}
    (hlo : lo ≤ upper) (hhi : lower ≤ hi)
    (htlo : lo ≤ tentative) (hthi : tentative ≤ hi) :
    lo ≤ nodeValue parent upper lower tentative ∧
      nodeValue parent upper lower tentative ≤ hi := by
…

    Mentions: OAI.PlanarL1.Interpolation.nodeValue

  4. theorem OAI.PlanarL1.Interpolation.distant_node_overwrites line 40

    Source documentation

    The obstruction in int:depth: a distant node cannot pass an accurate parent value unchanged. The constants 6, 7 and 13 are the source's constants.

    theorem distant_node_overwrites {parent upper lower tentative p δ : ℝ}
    (hδ : 0 < δ) (hp : |parent - p| ≤ 6 * δ)
    (hu : p + 7 * δ < upper) (hl : lower < p - 7 * δ)
    (ht : p + 13 * δ < tentative) :
    p + 7 * δ < nodeValue parent upper lower tentative ∧
      nodeValue parent upper lower tentative ≠ parent := by
…

    Mentions: OAI.PlanarL1.Interpolation.nodeValue

  5. structure OAI.PlanarL1.Interpolation.NamedValue line 59

    Source documentation

    An atom evaluation together with its deterministic priority/inheritance name. Its value may depend on all the already sampled ancestor noises.

    structure NamedValue where
…
  6. def OAI.PlanarL1.Interpolation.minNamed line 64

    Source documentation

    Minima and maxima both resolve ties toward the earliest atom name.

    noncomputable def minNamed (a b : NamedValue) : NamedValue :=
…

    Mentions: OAI.PlanarL1.Interpolation.NamedValue

  7. def OAI.PlanarL1.Interpolation.maxNamed line 67
  8. lemma OAI.PlanarL1.Interpolation.minNamed_mem line 70
  9. lemma OAI.PlanarL1.Interpolation.maxNamed_mem line 74
  10. lemma OAI.PlanarL1.Interpolation.minNamed_value line 79
  11. lemma OAI.PlanarL1.Interpolation.maxNamed_value line 89
  12. def OAI.PlanarL1.Interpolation.nodeNamed line 99

    Source documentation

    The clamp with the manuscript's consistent atom-name tie rule.

    noncomputable def nodeNamed (parent upper lower tentative : NamedValue) : NamedValue :=
…

    Mentions: OAI.PlanarL1.Interpolation.NamedValue

  13. lemma OAI.PlanarL1.Interpolation.nodeNamed_value line 103
  14. lemma OAI.PlanarL1.Interpolation.nodeNamed_mem line 108
  15. lemma OAI.PlanarL1.Interpolation.nodeNamed_old line 126

    Source documentation

    A name from before the current node can only be selected by literally inheriting the parent's atom. In particular its scalar value is inherited too.

    lemma nodeNamed_old {parent upper lower tentative : NamedValue} {cutoff : ℕ}
    (hu : cutoff ≤ upper.name) (hl : cutoff ≤ lower.name)
    (ht : cutoff ≤ tentative.name)
    (h : (nodeNamed parent upper lower tentative).name < cutoff) :
    nodeNamed parent upper lower tentative = parent := by
…

    Mentions: OAI.PlanarL1.Interpolation.NamedValue, OAI.PlanarL1.Interpolation.nodeNamed

  16. lemma OAI.PlanarL1.Interpolation.nodeNamed_collar line 137

    Source documentation

    The complete equality collar, including exact retention of the parent atom's name .

    lemma nodeNamed_collar {parent upper lower tentative : NamedValue}
    (hu : upper.value < parent.value) (hl : parent.value < lower.value)
    (ht : parent.name ≤ tentative.name) :
    nodeNamed parent upper lower tentative = parent := by
…

    Mentions: OAI.PlanarL1.Interpolation.NamedValue, OAI.PlanarL1.Interpolation.nodeNamed

  17. lemma OAI.PlanarL1.Interpolation.chain_inherits line 162

    Source documentation

    Iterated inheritance along a fixed ancestor chain. This does not make any independence assumption on the already computed scalar intercepts.

    lemma chain_inherits {F U L T : ℕ → NamedValue} {k n cutoff : ℕ}
    (hkn : k ≤ n)
    (hrec : ∀ j, F (j + 1) = nodeNamed (F j) (U (j + 1)) (L (j + 1)) (T (j + 1)))
    (hnew : ∀ j, k ≤ j → j < n →
      cutoff ≤ (U (j + 1)).name ∧ cutoff ≤ (L (j + 1)).name ∧
        cutoff ≤ (T (j + 1)).name)
    (hout : (F n).name < cutoff) : F n = F k := by
…

    Mentions: OAI.PlanarL1.Interpolation.NamedValue, OAI.PlanarL1.Interpolation.nodeNamed

  18. theorem OAI.PlanarL1.Interpolation.bounded_ancestry line 183

    Source documentation

    Quantitative bounded ancestry. At a distant node k, the source's 7δ/13δ barriers prevent an accurate final value from retaining a name originating strictly before k. All actual new atoms of stage j have names ≥ 6*j. This is the substantive inheritance argument of lemma int:depth.

    theorem bounded_ancestry {F U L T : ℕ → NamedValue} {k n : ℕ} {p δ : ℝ}
    (hk : 1 ≤ k) (hkn : k ≤ n) (hδ : 0 < δ)
    (hrec : ∀ j, F (j + 1) = nodeNamed (F j) (U (j + 1)) (L (j + 1)) (T (j + 1)))
    (hnew : ∀ j, 6 * j ≤ (U j).name ∧ 6 * j ≤ (L j).name ∧ 6 * j ≤ (T j).name)
    (haccuracy : |(F n).value - p| ≤ 6 * δ)
    (hu : p + 7 * δ < (U k).value) (hl : (L k).value < p - 7 * δ)
    (ht : p + 13 * δ < (T k).value) : 6 * k ≤ (F n).name := by
…

    Mentions: OAI.PlanarL1.Interpolation.NamedValue, OAI.PlanarL1.Interpolation.nodeNamed

  19. lemma OAI.PlanarL1.Interpolation.recent_name_count line 213

    Source documentation

    There are at most 6*(M+1) names in the last M+1 levels, independently of the total depth. This is the exact deterministic list-size bound N.

    lemma recent_name_count (n M : ℕ) :
    (Finset.Ico (6 * (n - M)) (6 * (n + 1))).card ≤ 6 * (M + 1) := by
…
  20. lemma OAI.PlanarL1.Interpolation.distance_cone_lipschitz line 219

    Source documentation

    Both signed distance cones have their exact unit Lipschitz constant.

    lemma distance_cone_lipschitz {X : Type*} [PseudoMetricSpace X] (x : X) (c : ℝ) :
    LipschitzWith 1 (fun v => c + dist x v) ∧
      LipschitzWith 1 (fun v => c - dist x v) := by
…
  21. lemma OAI.PlanarL1.Interpolation.nodeValue_lipschitz line 230
  22. lemma OAI.PlanarL1.Interpolation.selection_near_tie line 253

    Source documentation

    A continuous finite selection cannot change its recorded branch on a ball without a near tie at the center. This includes the old-field branch of a clipping, even though that branch has no fresh offset of its own.

    lemma selection_near_tie {X : Type*} [PseudoMetricSpace X] {K : ℝ≥0}
    (F : X → NamedValue) (atom : ℕ → X → ℝ) (S : Finset ℕ)
    (hF : LipschitzWith K (fun z => (F z).value))
    (hA : ∀ i ∈ S, LipschitzWith K (atom i)) (x : X) {ρ : ℝ}
    (hρ : 0 ≤ ρ)
    (hlist : ∀ z, dist x z ≤ ρ → (F z).name ∈ S ∧ (F z).value = atom (F z).name z)
    (hbad : ∃ z, dist x z ≤ ρ ∧ (F z).name ≠ (F x).name) :
    ∃ i ∈ S, ∃ j ∈ S, i ≠ j ∧ |atom i x-atom j x| ≤ 2*K*ρ := by
…

    Mentions: OAI.PlanarL1.Interpolation.NamedValue

  23. lemma OAI.PlanarL1.Interpolation.selection_probability line 274
  24. def OAI.PlanarL1.Interpolation.clippedNamed line 299
  25. lemma OAI.PlanarL1.Interpolation.clippedNamed_mem line 302
  26. lemma OAI.PlanarL1.Interpolation.clippedNamed_value line 310
  27. def OAI.PlanarL1.Interpolation.clipNames line 314
  28. lemma OAI.PlanarL1.Interpolation.clipNames_card line 317
  29. lemma OAI.PlanarL1.Interpolation.mem_clipNames line 323
  30. def OAI.PlanarL1.Interpolation.namedClip line 339

    Source documentation

    The old field has priority zero; the shield has priority one, and actual inherited atom identities are shifted by two. Thus a retaining tie keeps the old identifier, just as required by the source chart update.

    noncomputable def namedClip {X : Type*} (F : X → NamedValue) (old shield : X → ℝ)
    (x : X) : NamedValue :=
…

    Mentions: OAI.PlanarL1.Interpolation.NamedValue

  31. def OAI.PlanarL1.Interpolation.clipAtom line 343
  32. lemma OAI.PlanarL1.Interpolation.namedClip_list line 346
  33. lemma OAI.PlanarL1.Interpolation.clipAtom_lipschitz line 367
  34. lemma OAI.PlanarL1.Interpolation.clippedNamed_retains line 384
  35. def OAI.PlanarL1.Interpolation.secondaryNames line 400
  36. lemma OAI.PlanarL1.Interpolation.secondaryNames_card line 403
  37. lemma OAI.PlanarL1.Interpolation.mem_secondaryNames line 412
  38. def OAI.PlanarL1.Interpolation.secondaryNamed line 430
  39. def OAI.PlanarL1.Interpolation.secondaryAtom line 436
  40. lemma OAI.PlanarL1.Interpolation.secondaryNamed_value line 440
  41. lemma OAI.PlanarL1.Interpolation.secondaryNamed_mem line 447
  42. lemma OAI.PlanarL1.Interpolation.secondaryNamed_list line 466
  43. lemma OAI.PlanarL1.Interpolation.secondaryAtom_lipschitz line 485
  44. def OAI.PlanarL1.Interpolation.familyName line 511

    Source documentation

    Retained old branches are shared (name zero). Every genuinely new group branch receives a distinct name including its group, not merely its formula.

    def familyName {k : ℕ} (g : Fin k) (i : ℕ) : ℕ :=
…
  45. lemma OAI.PlanarL1.Interpolation.familyName_zero line 514
  46. lemma OAI.PlanarL1.Interpolation.familyName_ne_zero line 517
  47. lemma OAI.PlanarL1.Interpolation.familyName_inj line 520
  48. def OAI.PlanarL1.Interpolation.familyNames line 528
  49. lemma OAI.PlanarL1.Interpolation.mem_familyNames line 531
  50. lemma OAI.PlanarL1.Interpolation.familyNames_card line 536
  51. def OAI.PlanarL1.Interpolation.familyAtom line 547
  52. lemma OAI.PlanarL1.Interpolation.familyAtom_zero line 552
  53. lemma OAI.PlanarL1.Interpolation.familyAtom_name line 556
  54. lemma OAI.PlanarL1.Interpolation.familyAtom_lipschitz line 562
  55. lemma OAI.PlanarL1.Interpolation.familyAtomPair_probability line 574

    Source documentation

    Comparisons in one group use the local fresh-offset estimate. Comparisons between groups condition on all other samples and then use a constant test.

    lemma familyAtomPair_probability {X Ω : Type*} {k : ℕ} [Fintype Ω] [Nonempty Ω]
    (old : X → ℝ) (A : Fin k → Ω → ℕ → X → ℝ) (S : Fin k → Finset ℕ)
    (x : X) {t b : ℝ}
    (hpair : ∀ g i, i ∈ S g → ∀ j, j ∈ S g → i ≠ j →
      FiniteRandom.prob (fun ω => |A g ω i x-A g ω j x| ≤ t) ≤ b)
    (hconst : ∀ g i, i ∈ S g → i ≠ 0 → ∀ c : ℝ,
      FiniteRandom.prob (fun ω => |A g ω i x-c| ≤ t) ≤ b)
    (i j : ℕ) (hi : i ∈ familyNames S) (hj : j ∈ familyNames S) (hne : i ≠ j) :
    FiniteRandom.prob (fun ω : Fin k → Ω =>
      |familyAtom old (fun g => A g (ω g)) i x-familyAtom old (fun g => A g (ω g)) j x| ≤ t) ≤ b := by
…

    Mentions: OAI.PlanarL1.FiniteRandom.prob, OAI.PlanarL1.Interpolation.familyNames, OAI.PlanarL1.Interpolation.familyAtom

  56. def OAI.PlanarL1.Interpolation.maxSelection line 625
  57. lemma OAI.PlanarL1.Interpolation.maxSelection_mem line 630
  58. lemma OAI.PlanarL1.Interpolation.maxSelection_lipschitz line 643
  59. def OAI.PlanarL1.Interpolation.familySelection line 654
  60. lemma OAI.PlanarL1.Interpolation.familySelection_list line 659
  61. lemma OAI.PlanarL1.Interpolation.familySelection_lipschitz line 681
  62. lemma OAI.PlanarL1.Interpolation.familySelection_probability line 692

    Source documentation

    The literal deterministic finite maximum has a single identifier throughout one small ball except for the finite pair-comparison events.

    lemma familySelection_probability {X Ω : Type*} [PseudoMetricSpace X]
    [Fintype Ω] [Nonempty Ω] {k N : ℕ} {K : ℝ≥0}
    (old : X → ℝ) (F : Fin k → Ω → X → NamedValue)
    (A : Fin k → Ω → ℕ → X → ℝ) (S : Fin k → Finset ℕ)
    (ho : LipschitzWith K old)
    (hF : ∀ g ω, LipschitzWith K (fun z => (F g ω z).value))
    (hA : ∀ g ω i, LipschitzWith K (A g ω i))
    (hzero : ∀ g ω z, A g ω 0 z=old z) (hcard : ∀ g, (S g).card ≤ N)
    (x : X) {ρ b : ℝ} (hρ : 0 ≤ ρ) (hb : 0 ≤ b)
    (hlist : ∀ g ω z, dist x z ≤ ρ → (F g ω z).name ∈ S g ∧
      (F g ω z).value = A g ω (F g ω z).name z)
    (hpair : ∀ g i, i ∈ S g → ∀ j, j ∈ S g → i ≠ j →
…

    Mentions: OAI.PlanarL1.Interpolation.NamedValue

  63. lemma OAI.PlanarL1.Interpolation.clippedNamed_eq_old_of_value line 733
  64. lemma OAI.PlanarL1.Interpolation.namedClip_eq_old_iff line 745