actual_finite_history_tail_law

Plain-English statement

Independent science ada2d073d04a78493555b2ac35344b9c5a264bfc. Same six source analytic hypotheses and literal actual76 stopped recursion driven by actual77 iidExp1. For every deterministic n, actual history R0..Rn consumes raw coordinates k<n: derive ambient and F_n measurability, pointwise prefix causality, unchanged full infinite raw tail starting n, history-tail independence/product law and unnormalized restricted-tail pushforward, including n0/stopped/null A. Truncation is only a measurable proof factorization. Closes only probability substrate of G86-11/S87I1-I3; conditional random-hazard next-wait survival/density/final survival/iteration S87I4-I5/fullA7, random stopping/physical-time residual memorylessness/restart/Markov/invariance/allL2/main/error/unboundedcost/composition/wholepaper/Goal remain OPEN.

Scope guard. This card records a compiled local declaration. Its mathematical scope is exactly the Lean statement below; the Registry note and source correspondence may describe motivation but do not strengthen it.

Lean learning studio · mathematics → formal proof

Read the mathematics first, then descend into Lean

You do not need to know Lean before opening this panel. The page keeps the paper-level theorem, rigorous proof obligations, exact Lean declaration, and proof dependencies as separate layers so a first-time reader can move down one layer at a time.

BeginnerWhy this theorem exists → intuition → statement → one hand calculation. Hide proof-engineering detail.

RigorousExpose assumptions, hidden measure/limit/domain issues, proof route, and rigorous references.

Lean learnerOpen the exact declaration, proof tree/network, syntax glossary, and line-by-line explanation.

Proof architecture

Start with the tree when learning: prerequisites sit below the theorem and downstream results sit above it. Switch to the network when you want to understand where this declaration lives in the local formal library. Every mapped node is clickable.

Loading source-derived dependency evidence…

Graph rule: only dependencies found by the ASTIS source scan are drawn. Missing tactic indirection is treated as an under-approximation; the site never invents an edge just to make a prettier graph.

How to read the exact Lean declaration

Read a Lean theorem left-to-right exactly as you would unpack a mathematical sentence: name → ambient types → automatically inferred structures → explicit hypotheses → conclusion → proof. Then read the proof top-to-bottom as transformations of the current goal.

NameWhat reusable mathematical fact is being created?
ParametersWhich symbols are arbitrary, and which structures are inferred by typeclass search?
PropositionAfter the colon, translate the Lean expression back into a paper statement.
Proof actionsAfter by, ask what each tactic does to the mathematical goal—not only what syntax it uses.

Syntax used on this page

This glossary is filtered to syntax that actually occurs in the declaration above. Open a symbol only when you meet it, rather than memorizing Lean grammar in advance.

Source voice and ASTIS voice stay separate

When Samplinglib shows a short quotation from Chewi, it is labeled as a source excerpt and linked to the canonical book page. Intuition, expanded proof steps, hidden regularity assumptions, and Lean explanations are ASTIS-authored commentary. A quotation never substitutes for a formal proof, and an ASTIS explanation is never attributed to the textbook author.

Lean statement

theorem actual_finite_history_tail_law
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ) * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ) * ‖v‖ ^ 2)
    (hη : 0 < η) (hβη : (β : ℝ) * η ≤ 1) :
    actual_finite_history_tail_law_statement hα hαβ hV hH hη hβη := by
  classical
  let c : E → E → E := fun y xRef => y - η • gradient V xRef
  let Φ : E → E → ℝ → (E × E) → (E × E) := fun y xRef t z =>
    (c y xRef + Real.cos t • (z.1 - c y xRef) +
        (Real.sqrt η * Real.sin t) • z.2,
     (-Real.sin t / Real.sqrt η) • (z.1 - c y xRef) + Real.cos t • z.2)
  let S : E → (E × E) → (E × E) := fun xRef z =>
    (z.1, z.2 - (2 * inner ℝ z.2 (gradient V z.1 - gradient V xRef) /
      ‖gradient V z.1 - gradient V xRef‖ ^ 2) • (gradient V z.1 - gradient V xRef))
  let rate : E → (E × E) → ℝ := fun xRef z =>
    Real.sqrt η * max 0 (inner ℝ z.2 (gradient V z.1 - gradient V xRef))
  let Λ : E → E → (E × E) → ℝ≥0 → ℝ := fun y xRef z t =>
    ∫ s in (0 : ℝ)..(t : ℝ), rate xRef (Φ y xRef s z)
  let τ : E → E → (E × E) → ℝ≥0 → WithTop ℝ≥0 := fun y xRef z e =>
    MeasureTheory.hittingAfter
      (fun t : ℝ≥0 => fun a : (E × E) × (E × E) × ℝ≥0 =>
        Λ a.1.1 a.1.2 a.2.1 t - (a.2.2 : ℝ))
      (Set.Ici (0 : ℝ)) 0 ((y, xRef), z, e)
  let next : E → E → ℝ≥0 → ((ℝ≥0 × (E × E)) ⊕ Unit) →
      ((ℝ≥0 × (E × E)) ⊕ Unit) := fun y xRef e r =>
    match r with
    | Sum.inr _ => Sum.inr ()
    | Sum.inl a =>
      if τ y xRef a.2 e = ⊤ then Sum.inr () else
        Sum.inl (a.1 + (τ y xRef a.2 e).untopD 0,
          S xRef (Φ y xRef (((τ y xRef a.2 e).untopD 0 : ℝ≥0) : ℝ) a.2))
  let record : E → E → (E × E) → (ℕ → ℝ≥0) → ℕ →
      ((ℝ≥0 × (E × E)) ⊕ Unit) := fun y xRef z₀ e n =>
    Nat.rec (Sum.inl (0, z₀)) (fun k r => next y xRef (e k) r) n
  let P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
  let ε : (ℕ → ℝ) → ℕ → ℝ≥0 := fun w k => Real.toNNReal (w k)
  let history : E → E → (E × E) → (n : ℕ) → (ℕ → ℝ) →
      (Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit)) :=
    fun y xRef z₀ n w j => record y xRef z₀ (ε w) j.val
  let tail : ℕ → (ℕ → ℝ) → (ℕ → ℝ) := fun n w k => w (n + k)
  let past : ℕ → MeasurableSpace (ℕ → ℝ) := fun n =>
    ⨆ k ∈ Set.Iio n, MeasurableSpace.comap (fun w : ℕ → ℝ => w k) inferInstance
  change
  ∀ y xRef : E, ∀ z₀ : E × E, ∀ n : ℕ,
      Measurable (history y xRef z₀ n) ∧ Measurable (tail n) ∧
      (∀ (w w' : ℕ → ℝ), (∀ k < n, w k = w' k) →
        history y xRef z₀ n w = history y xRef z₀ n w') ∧
      Measurable[past n] (history y xRef z₀ n) ∧
      Measure.map (tail n) P = P ∧
      IndepFun (history y xRef z₀ n) (tail n) P ∧
      Measure.map (fun w => (history y xRef z₀ n w, tail n w)) P =
        (Measure.map (history y xRef z₀ n) P).prod P ∧
      (∀ A : Set (Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit)), MeasurableSet A →
        Measure.map (tail n) (P.restrict (history y xRef z₀ n ⁻¹' A)) =
          (P (history y xRef z₀ n ⁻¹' A)) • P)

  have hrec := ActualFiniteJumpRecursion.actual_fixed_reference_finite_jump_recursion
    hα hαβ hV hH hη hβη
  have hR (j : ℕ) : Measurable (fun a : (E × E) × (E × E) × (ℕ → ℝ≥0) =>
      record a.1.1 a.1.2 a.2.1 a.2.2 j) := hrec.2.2.2.1 j
  have hinput := AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws
  letI : IsProbabilityMeasure P := hinput.1
  letI : IsProbabilityMeasure (expMeasure (1 : ℝ)) :=
    isProbabilityMeasure_expMeasure zero_lt_one
  have hclock : iIndepFun (fun k (w : ℕ → ℝ) => w k) P := hinput.2.2.1
  intro y xRef z₀ n
  -- Deterministic causality: the mth record consumes exactly coordinates below m.
  have hcausal (e e' : ℕ → ℝ≥0) (m : ℕ)
      (he : ∀ k < m, e k = e' k) :
      record y xRef z₀ e m = record y xRef z₀ e' m := by
    induction m with
    | zero => rfl
    | succ m ih =>
      change next y xRef (e m) (record y xRef z₀ e m) =
        next y xRef (e' m) (record y xRef z₀ e' m)
      rw [he m (Nat.lt_succ_self m), ih (fun k hk => he k (Nat.lt_succ_of_lt hk))]
  have hprefix (w w' : ℕ → ℝ) (hw : ∀ k < n, w k = w' k) :
      history y xRef z₀ n w = history y xRef z₀ n w' := by
    funext j
    exact hcausal (ε w) (ε w') j.val (fun k hk =>
      congrArg Real.toNNReal (hw k (lt_of_lt_of_le hk (Nat.le_of_lt_succ j.isLt))))
  have hε : Measurable ε := measurable_pi_lambda _ (fun k =>
    measurable_real_toNNReal.comp (measurable_pi_apply k :
      Measurable (fun w : ℕ → ℝ => w k)))
  have hHmeas : Measurable (history y xRef z₀ n) :=
    measurable_pi_lambda _ (fun j => (hR j.val).comp
      ((measurable_const : Measurable (fun _ : ℕ → ℝ => (y, xRef))).prodMk
        ((measurable_const : Measurable (fun _ : ℕ → ℝ => z₀)).prodMk hε)))
  have hTmeas : Measurable (tail n) :=
    measurable_pi_lambda _ (fun k => measurable_pi_apply (n + k))
  -- Truncation is a proof factorization, never a replacement algorithm/input law.
  let truncated : (ℕ → ℝ) → ℕ → ℝ≥0 :=
    fun w k => if k < n then ε w k else 0
  have htruncated : Measurable[past n] truncated := by
    letI : MeasurableSpace (ℕ → ℝ) := past n
    apply measurable_pi_lambda
    intro k
    by_cases hk : k < n
    · have hx : Measurable[past n] (fun w : ℕ → ℝ => w k) := by
        apply measurable_iff_comap_le.mpr
        exact le_iSup_of_le k (le_iSup_of_le hk le_rfl)
      simpa only [truncated, hk, if_true, ε, Function.comp_def] using
        measurable_real_toNNReal.comp hx
    · simpa only [truncated, hk, if_false] using
        (measurable_const : Measurable[past n] (fun _ : ℕ → ℝ => (0 : ℝ≥0)))
  have hHp : Measurable[past n] (history y xRef z₀ n) := by
    letI : MeasurableSpace (ℕ → ℝ) := past n
    apply measurable_pi_lambda
    intro j
    have hm := (hR j.val).comp
      ((measurable_const : Measurable (fun _ : ℕ → ℝ => (y, xRef))).prodMk
        ((measurable_const : Measurable (fun _ : ℕ → ℝ => z₀)).prodMk htruncated))
    have heq : (fun w => record y xRef z₀ (truncated w) j.val) =
        (fun w => history y xRef z₀ n w j) := by
      funext w
      exact hcausal (truncated w) (ε w) j.val (fun k hk =>
        if_pos (lt_of_lt_of_le hk (Nat.le_of_lt_succ j.isLt)))
    rw [← heq]
    exact hm
  let future : ℕ → MeasurableSpace (ℕ → ℝ) := fun m =>
    ⨆ k ∈ Set.Ici m, MeasurableSpace.comap (fun w : ℕ → ℝ => w k) inferInstance
  have hTf : Measurable[future n] (tail n) := by
    letI : MeasurableSpace (ℕ → ℝ) := future n
    apply measurable_pi_lambda
    intro k
    apply measurable_iff_comap_le.mpr
    exact le_iSup_of_le (n + k) (le_iSup_of_le (Nat.le_add_right n k) le_rfl)
  have hdis : Disjoint (Set.Iio n) (Set.Ici n) := by
    rw [Set.disjoint_left]
    intro k hk hn
    exact (not_lt_of_ge (show n ≤ k from hn)) (show k < n from hk)
  have hblocks : Indep (past n) (future n) P :=
    indep_iSup_of_disjoint (fun k => (measurable_pi_apply k).comap_le)
      ((iIndepFun_iff_iIndep (fun _ : ℕ => inferInstance)
        (fun k (w : ℕ → ℝ) => w k) P).mp hclock) hdis
  have hindep : IndepFun (history y xRef z₀ n) (tail n) P :=
    indep_of_indep_of_le hblocks hHp.comap_le hTf.comap_le
  have htailLaw : Measure.map (tail n) P = P := by
    exact Measure.map_infinitePi_infinitePi_of_inj
      (P := fun _ : ℕ => expMeasure (1 : ℝ)) (f := fun k => n + k)
      (fun _ _ h => Nat.add_left_cancel h)
  have hjoint : Measure.map (fun w => (history y xRef z₀ n w, tail n w)) P =
      (Measure.map (history y xRef z₀ n) P).prod P := by
    rw [hindep.map_prod_eq_prod_map_map hHmeas.aemeasurable hTmeas.aemeasurable,
      htailLaw]
  refine ⟨hHmeas, hTmeas, hprefix, hHp, htailLaw, hindep, hjoint, ?_⟩
  intro A hA
  apply Measure.ext
  intro B hB
  rw [Measure.map_apply hTmeas hB, Measure.restrict_apply (hB.preimage hTmeas),
    Measure.smul_apply, Set.inter_comm,
    hindep.measure_inter_preimage_eq_mul A B hA hB]
  have hBtail : P (tail n ⁻¹' B) = P B := by
    rw [← Measure.map_apply hTmeas hB, htailLaw]
  rw [hBtail]
  rfl

end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteHistoryTailLaw

Open AutoSamplingTheory/ExampleCases/ProximalBPS/ActualFiniteHistoryTailLaw.lean:77published source at ed709a7f320d

Proof architecture

Actual PBPS conditional-iteration substrate; no SALD claim

Lean proof walkthrough

Read the quantified variables and typeclass brackets as part of the mathematical statement; inferred arguments are not missing assumptions.
`intro` introduces quantified hypotheses into the local proof context.
`have` creates a named intermediate mathematical fact.
`rw` rewrites by an established identity.
`apply` reduces the goal to the hypotheses of a reusable theorem.
`refine` instantiates a reusable theorem while leaving explicit subgoals.
`exact` closes the current goal with an already typed term.
`simpa` closes the goal after a controlled simplification of a typed result.

Why the statement has this shape

The declaration is kept at the reusable level recorded by its Registry tags and direct consumers. Explicit measures, spaces, wrappers, and regularity hypotheses expose interfaces that paper notation often infers. A theorem card explains those interfaces but never widens the compiled statement.

Hidden assumptions and non-claims

Measurability is represented explicitly or must be supplied by a dependency.
Totalized `fderiv` values must not be read as a differentiability theorem.
Almost-everywhere hypotheses depend on the stated measure and representative.
Density statements retain normalization and absolute-continuity prerequisites.