Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
Samplinglib mathematical lesson

Ideal PBPS half-turn returned-position probability kernel

AutoSamplingTheory.ExampleCases.ProximalBPS.IdealHalfTurnKernel.ideal_half_turn_returned_position_kernel · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be any finite-dimensional real inner-product space, including dimension zero, with its Borel measurable structure. Let V:E→ℝ be C². Let α,β be nonnegative reals and η a real number satisfying α>0, α≤β, α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v∈E, η>0, and βη≤1. Allow arbitrary parameters y,xRef∈E and initial phase z0=(x0,p0)∈E×E. Set c=y−η∇V(xRef). For z=(x,p), define the actual harmonic flow Φ_t(z)=(c+cos(t)(x−c)+√η sin(t)p, −sin(t)(x−c)/√η+cos(t)p), reflection S(z)=(x,p−[2〈p,g(x)〉/‖g(x)‖²]g(x)), residual g(x)=∇V(x)−∇V(xRef), and rate λ(z)=√η max{0,〈p,g(x)〉}. The reflection uses total real division, hence is the identity when g(x)=0. Define Λ(z,t)=∫_0^t λ(Φ_s(z)) ds for finite t≥0 and τ(z,e)=inf{t≥0:Λ(z,t)≥e}, with inf empty=∞. Let P be the actual countable product of rate-one exponential Borel measures on Ω=ℝ^ℕ; let ε_k(sample)=max{sample_k,0} viewed as a nonnegative real. Define active records (T,z) and an absorbing stopped record carrying no phase. Initialize record0=(0,z0). At index k, a stopped record stays stopped; an active record (T,z) becomes stopped if τ(z,ε_k)=∞ and otherwise becomes (T+τ(z,ε_k), S(Φ_{τ(z,ε_k)}(z))). Its event time T_k is the finite time component if active and ∞ if stopped. There exists a total phase map Z:E×E×(E×E)×[0,∞)×Ω→E×E jointly Borel measurable in all displayed parameters, finite physical time t and sample, while V,α,β,η remain fixed. For every parameter triple, every sample, every finite t and any actual covering index n with T_n≤t<T_(n+1), if record_n=inl(a) with a=(s,z), then Z(y,xRef,z0,t,sample)=Φ_(t−s)(z), where subtraction is the NNReal nonnegative subtraction. If no such actual covering index exists, Z(y,xRef,z0,t,sample)=z0. This uncovered value is an explicitly chosen ASTIS total representative convention, not a source state supplied on exceptional inputs. Furthermore, for each fixed deterministic y,xRef,z0, for P-almost every sample simultaneously: for every finite nonnegative t there exist n and an actual finite live record a=(s,z) with T_n≤t<T_(n+1), record_n=inl(a), s≤t, t−s<τ(z,ε_n) and Z(y,xRef,z0,t,sample)=Φ_(t−s)(z); and Z(y,xRef,z0,0,sample)=z0. A stopped record never provides the source phase. An infinite next wait retains the last live harmonic arc for all later finite t and does not trigger the uncovered fallback. The AE event may depend on the fixed parameter triple; no uniform event over all parameters is asserted. Joint measurability permits later measurable parameter evaluation, but per-parameter AE agreement cannot be substituted at arbitrary parameters correlated with sample without a separate law/independence/conditional-kernel argument. Define the exact conditional reference law q_y=volume.tilted(r↦−V(r)−‖r−y‖²/(2η)); tilted denotes the normalized exponential tilt with its literal totalized Mathlib definition. Let γ=N(0,I) be the standard Gaussian momentum law on E, and M_y=(q_y⊗γ)⊗P on ((reference,momentum),clock sample). Let tπ=π as a nonnegative finite time. The same jointly measurable phase witness Z additionally has the following properties. There exists a probability kernel R:E→Measure(E), jointly measurable in its parameter y, with R(y)=q_y for every y. There exists a probability kernel H:(E×E)→Measure(E), jointly measurable in the input (y,x), such that for every deterministic y,x, H(y,x) is exactly the pushforward of M_y by w↦firstCoordinate(Z(y,w.reference,(x,w.momentum),π,w.clock)). Thus H is the ideal exact-reference Algorithm1 returned-position kernel; q_y normalization and kernel measurability are conclusions, not assumptions. The phase pushforward at time zero is δ_x⊗γ. Moreover, for each fixed y,x, M_y-almost every w simultaneously satisfies Z(y,w.reference,(x,w.momentum),0,w.clock)=(x,w.momentum) and admits an actual finite live record a=(s,z) and index n at π with T_n≤π<T_(n+1), record_n=inl(a), s≤π, π−s<τ(z,ε_n), and Z(y,w.reference,(x,w.momentum),π,w.clock)=Φ_(π−s)(z). The reference is independent of momentum and clocks under precisely the displayed product law and stays fixed along each run. This bounded ASTIS completion of source AppendixA.1 ideal H_y supplies a mathematical probability kernel and physical initialization/terminal agreement. It does not supply an implementable exact reference sampler, approximate reference comparison, expected cost, a phase Markov process or semigroup, invariance, reversibility, hypocoercivity, a random all-time path-law theorem, or a separately proved version-uniqueness theorem. There is no new hypothesis, correlated random-parameter substitution, uniform AE event over parameters or main/composition completion.

\[H(y,x)=\bigl[w\mapsto\operatorname{pr}_1 Z(y,w_r,(x,w_p),\pi,w_\omega)\bigr]_\#M_y.\]
Lean statement · ideal_half_turn_returned_position_kernel

Let E be any finite-dimensional real inner-product space, including dimension zero, with its Borel measurable structure. Let V:E→ℝ be C². Let α,β be nonnegative reals and η a real number satisfying α>0, α≤β, α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v∈E, η>0, and βη≤1. Allow arbitrary parameters y,xRef∈E and initial phase z0=(x0,p0)∈E×E. Set c=y−η∇V(xRef). For z=(x,p), define the actual harmonic flow Φ_t(z)=(c+cos(t)(x−c)+√η sin(t)p, −sin(t)(x−c)/√η+cos(t)p), reflection S(z)=(x,p−[2〈p,g(x)〉/‖g(x)‖²]g(x)), residual g(x)=∇V(x)−∇V(xRef), and rate λ(z)=√η max{0,〈p,g(x)〉}. The reflection uses total real division, hence is the identity when g(x)=0. Define Λ(z,t)=∫_0^t λ(Φ_s(z)) ds for finite t≥0 and τ(z,e)=inf{t≥0:Λ(z,t)≥e}, with inf empty=∞. Let P be the actual countable product of rate-one exponential Borel measures on Ω=ℝ^ℕ; let ε_k(sample)=max{sample_k,0} viewed as a nonnegative real. Define active records (T,z) and an absorbing stopped record carrying no phase. Initialize record0=(0,z0). At index k, a stopped record stays stopped; an active record (T,z) becomes stopped if τ(z,ε_k)=∞ and otherwise becomes (T+τ(z,ε_k), S(Φ_{τ(z,ε_k)}(z))). Its event time T_k is the finite time component if active and ∞ if stopped. There exists a total phase map Z:E×E×(E×E)×[0,∞)×Ω→E×E jointly Borel measurable in all displayed parameters, finite physical time t and sample, while V,α,β,η remain fixed. For every parameter triple, every sample, every finite t and any actual covering index n with T_n≤t<T_(n+1), if record_n=inl(a) with a=(s,z), then Z(y,xRef,z0,t,sample)=Φ_(t−s)(z), where subtraction is the NNReal nonnegative subtraction. If no such actual covering index exists, Z(y,xRef,z0,t,sample)=z0. This uncovered value is an explicitly chosen ASTIS total representative convention, not a source state supplied on exceptional inputs. Furthermore, for each fixed deterministic y,xRef,z0, for P-almost every sample simultaneously: for every finite nonnegative t there exist n and an actual finite live record a=(s,z) with T_n≤t<T_(n+1), record_n=inl(a), s≤t, t−s<τ(z,ε_n) and Z(y,xRef,z0,t,sample)=Φ_(t−s)(z); and Z(y,xRef,z0,0,sample)=z0. A stopped record never provides the source phase. An infinite next wait retains the last live harmonic arc for all later finite t and does not trigger the uncovered fallback. The AE event may depend on the fixed parameter triple; no uniform event over all parameters is asserted. Joint measurability permits later measurable parameter evaluation, but per-parameter AE agreement cannot be substituted at arbitrary parameters correlated with sample without a separate law/independence/conditional-kernel argument. Define the exact conditional reference law q_y=volume.tilted(r↦−V(r)−‖r−y‖²/(2η)); tilted denotes the normalized exponential tilt with its literal totalized Mathlib definition. Let γ=N(0,I) be the standard Gaussian momentum law on E, and M_y=(q_y⊗γ)⊗P on ((reference,momentum),clock sample). Let tπ=π as a nonnegative finite time. The same jointly measurable phase witness Z additionally has the following properties. There exists a probability kernel R:E→Measure(E), jointly measurable in its parameter y, with R(y)=q_y for every y. There exists a probability kernel H:(E×E)→Measure(E), jointly measurable in the input (y,x), such that for every deterministic y,x, H(y,x) is exactly the pushforward of M_y by w↦firstCoordinate(Z(y,w.reference,(x,w.momentum),π,w.clock)). Thus H is the ideal exact-reference Algorithm1 returned-position kernel; q_y normalization and kernel measurability are conclusions, not assumptions. The phase pushforward at time zero is δ_x⊗γ. Moreover, for each fixed y,x, M_y-almost every w simultaneously satisfies Z(y,w.reference,(x,w.momentum),0,w.clock)=(x,w.momentum) and admits an actual finite live record a=(s,z) and index n at π with T_n≤π<T_(n+1), record_n=inl(a), s≤π, π−s<τ(z,ε_n), and Z(y,w.reference,(x,w.momentum),π,w.clock)=Φ_(π−s)(z). The reference is independent of momentum and clocks under precisely the displayed product law and stays fixed along each run. This bounded ASTIS completion of source AppendixA.1 ideal H_y supplies a mathematical probability kernel and physical initialization/terminal agreement. It does not supply an implementable exact reference sampler, approximate reference comparison, expected cost, a phase Markov process or semigroup, invariance, reversibility, hypocoercivity, a random all-time path-law theorem, or a separately proved version-uniqueness theorem. There is no new hypothesis, correlated random-parameter substitution, uniform AE event over parameters or main/composition completion.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)
theorem ideal_half_turn_returned_position_kernel
    {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) :
    ideal_half_turn_returned_position_kernel_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · ideal_half_turn_returned_position_kernel_statement

This literal definition stores the complete proposition asserted above. It supplies no mathematical proof or additional hypothesis; the theorem proof must establish its value.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)
private def ideal_half_turn_returned_position_kernel_statement
    {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) : Prop :=
    let P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
    let ε : (ℕ → ℝ) → ℕ → ℝ≥0 := fun sample k => Real.toNNReal (sample k)
    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 eventTime : E → E → (E × E) → (ℕ → ℝ≥0) → ℕ → WithTop ℝ≥0 :=
      fun y xRef z₀ e n => (record y xRef z₀ e n).elim
        (fun a => (a.1 : WithTop ℝ≥0)) (fun _ => ⊤)
    let q : E → Measure E := fun y =>
      (volume : Measure E).tilted (fun x => -V x - ‖x - y‖ ^ 2 / (2 * η))
    let γ : Measure E := stdGaussian E
    let M : E → Measure ((E × E) × (ℕ → ℝ)) := fun y => ((q y).prod γ).prod P
    let tπ : ℝ≥0 := ⟨Real.pi, Real.pi_pos.le⟩
    ∃ Z : E → E → (E × E) → ℝ≥0 → (ℕ → ℝ) → (E × E),
      Measurable (fun a : ((E × E) × (E × E)) × ℝ≥0 × (ℕ → ℝ) =>
        Z a.1.1.1 a.1.1.2 a.1.2 a.2.1 a.2.2) ∧
      (∀ y xRef : E, ∀ z₀ : E × E, ∀ sample : ℕ → ℝ, ∀ t : ℝ≥0,
        ∀ n : ℕ, ∀ a : ℝ≥0 × (E × E),
          eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0) →
          (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1) →
          record y xRef z₀ (ε sample) n = Sum.inl a →
          Z y xRef z₀ t sample = Φ y xRef ((t - a.1 : ℝ≥0) : ℝ) a.2) ∧
      (∀ y xRef : E, ∀ z₀ : E × E, ∀ sample : ℕ → ℝ, ∀ t : ℝ≥0,
        (¬ ∃ n : ℕ, eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0) ∧
          (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1)) →
          Z y xRef z₀ t sample = z₀) ∧
      (∀ y xRef : E, ∀ z₀ : E × E, ∀ᵐ sample ∂P,
        (∀ t : ℝ≥0, ∃ n : ℕ, ∃ a : ℝ≥0 × (E × E),
          eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0) ∧
          (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1) ∧
          record y xRef z₀ (ε sample) n = Sum.inl a ∧ a.1 ≤ t ∧
          ((t - a.1 : ℝ≥0) : WithTop ℝ≥0) < τ y xRef a.2 (ε sample n) ∧
          Z y xRef z₀ t sample = Φ y xRef ((t - a.1 : ℝ≥0) : ℝ) a.2) ∧
        Z y xRef z₀ 0 sample = z₀) ∧
      ∃ R : Kernel E E, IsMarkovKernel R ∧ (∀ y : E, R y = q y) ∧
      ∃ H : Kernel (E × E) E, IsMarkovKernel H ∧
      (∀ y x : E, H (y, x) = Measure.map
        (fun w : (E × E) × (ℕ → ℝ) => (Z y w.1.1 (x, w.1.2) tπ w.2).1)
        (M y)) ∧
      (∀ y x : E, Measure.map
        (fun w : (E × E) × (ℕ → ℝ) => Z y w.1.1 (x, w.1.2) 0 w.2)
        (M y) = (Measure.dirac x).prod γ) ∧
      (∀ y x : E, ∀ᵐ w ∂M y,
        Z y w.1.1 (x, w.1.2) 0 w.2 = (x, w.1.2) ∧
        ∃ n : ℕ, ∃ a : ℝ≥0 × (E × E),
          eventTime y w.1.1 (x, w.1.2) (ε w.2) n ≤ (tπ : WithTop ℝ≥0) ∧
          (tπ : WithTop ℝ≥0) < eventTime y w.1.1 (x, w.1.2) (ε w.2) (n + 1) ∧
          record y w.1.1 (x, w.1.2) (ε w.2) n = Sum.inl a ∧ a.1 ≤ tπ ∧
          ((tπ - a.1 : ℝ≥0) : WithTop ℝ≥0) < τ y w.1.1 a.2 (ε w.2 n) ∧
          Z y w.1.1 (x, w.1.2) tπ w.2 = Φ y w.1.1 ((tπ - a.1 : ℝ≥0) : ℝ) a.2)


set_option maxHeartbeats 1600000 in

Exact module and namespace context

Proof roadmap

  1. 1Retain actual dynamics and specify independent source inputs

    Keep the literal actual harmonic flow, residual reflection/rate, integrated hazard, hitting time and stopped finite recurrence. Set q_y to the normalized source conditional tilt, γ to standard Gaussian, and M_y to the actual independent reference/momentum/clock product. No path or law provider is a premise.

  2. 2Consume the actual joint phase and derive the Gibbs normalization

    The verified actual phase supplies joint Borel measurability and actual deterministic/per-parameter AE properties. The existing Gibbs augmentation gives a positive integral of exp(−V). A nonzero Bochner integral implies integrability, so its normalized exponential tilt is a probability measure. No minimizer, moment or normalizer certificate is supplied.

  3. 3Identify the exact everywhere-defined conditional reference kernel

    Apply the canonical Gaussian conditional-kernel theorem to the derived Gibbs probability. The pinned successive-tilt identity identifies its quadratic tilt with literal q_y. Kernel fiber probability forces the totalized tilt to be a genuine probability for every y.

  4. 4Build the actual parameter-dependent independent product kernel

    Pull R back by the y coordinate; multiply it by constant Gaussian and actual exponential product kernels. The resulting Q has precisely the source input law M_y at every (y,x). Standard kernel product instances give probability, without an independence assumption hidden in a binder.

  5. 5Push the actual terminal position through a measurable probability kernel

    Joint measurability of Z proves that terminal first-coordinate evaluation F is Borel in input and all random inputs. Retain (y,x) with the identity kernel, multiply by Q and map F. Pinned kernel-map probability gives H mass one, and the Dirac-product/map identities give exactly its source fiber formula.

  6. 6Retrieve measurable actual records, clocks, waits and flow

    Use the verified finite recursion, harmonic flow and integrated hazard clock as genuine dependencies. Coordinate clamping is measurable. These inputs will prove measurability of the full finite-time arc predicate before any product-AE lifting.

  7. 7Eliminate the apparent uncountable record witness

    Fix y,x. Pull back actual records/clocks to W=((reference,momentum),sample). The total Sum projection L_n chooses the live record and has a dummy branch only to make it Borel everywhere. Include record_n=inl(L_n) explicitly, so a stopped record cannot supply a source phase. Composing with Z, τ and Φ gives measurable origin/wait/branch maps.

  8. 8Prove that actual origin and terminal agreement form a Borel event

    Each D_n includes both half-open clock bounds, a live-record equality, stored time≤π, elapsed strictly below the next wait, and actual Z-to-flow equality. Borel order/equality and countable union give G={Z0=(x,p)}∩⋃D_n measurable. This avoids asserting measurability of an uncountable all-time intersection.

  9. 9Lift verified fixed-input good sections by product Fubini

    For each fixed reference/momentum, actual80 supplies a P-AE all-time arc and origin event. At π its live record equals L_n. Since the full finite-time event G is measurable, product Fubini lifts these sections to M_y-AE G. Expanding G returns the actual live witness and both origin/terminal conclusions.

  10. 10Derive the physical initialization law from the actual Gaussian marginal

    Return the constructed Z,R,H and proven actual product-AE terminal statement. AE map congruence replaces Z0 by (x,p); the independent product marginal of p is exactly γ because q_y and P have mass one. Its pushforward by p↦(x,p) is δ_x⊗γ.

Full assumptions and notation

All objects and hypotheses

  • E is any finite-dimensional real inner-product space with its Borel measurable structure, including dimension zero. V is real-valued and C²; α,β are nonnegative reals.
  • Exactly six analytic source hypotheses: α>0; α≤β; V∈C²; for all x,v, α‖v‖²≤D²V(x)[v,v]≤β‖v‖²; η>0; βη≤1. No third or higher derivative bound.
  • Standing E,V,α,β,η are fixed. y,xRef,z0,t,sample are arguments of one jointly Borel map. P and ε are literal canonical definitions; measurability, positive support, recurrence, cover and nonaccumulation are produced dependencies.
  • Standing parameters are fixed. Actual80 deterministic covered-arc/fallback and per-fixedparams common-AE all-time phase properties are retained. The new origin/terminal assertions use the exact independent product M_y=(q_y⊗γ)⊗P, for each fixed y,x; no arbitrary correlated input or uniform event is inferred.
  • A stopped record has no phase and infinite event time; every covering interval has a live finite record. The last infinite-wait live arc remains covered. The initial-phase fallback is an explicitly labelled ASTIS measurable extension only on the uncovered complement; zero-time exceptional bounces need not have source index0 at t0.
  • q_y and R are constructed from the original six conditions, not extra measure, normalization, kernel or sampler premises. The standard Gaussian momentum is unscaled; η appears in the literal dynamics. Kernel input order is (y,x), corresponding to source fixed parameter y and starting position x.

Mathematical proof

1. Retain actual dynamics and specify independent source inputs

Keep the literal actual harmonic flow, residual reflection/rate, integrated hazard, hitting time and stopped finite recurrence. Set q_y to the normalized source conditional tilt, γ to standard Gaussian, and M_y to the actual independent reference/momentum/clock product. No path or law provider is a premise.

\[q_y(dr)=\frac{\exp[-V(r)-\|r-y\|^2/(2\eta)]\,dr}{\int\exp[-V(u)-\|u-y\|^2/(2\eta)]\,du},\quad\gamma=N(0,I),\quad M_y=(q_y\otimes\gamma)\otimes P.\]
Corresponding Lean step
  classical
  let P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
  let ε : (ℕ → ℝ) → ℕ → ℝ≥0 := fun sample k => Real.toNNReal (sample k)
  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 eventTime : E → E → (E × E) → (ℕ → ℝ≥0) → ℕ → WithTop ℝ≥0 :=
    fun y xRef z₀ e n => (record y xRef z₀ e n).elim
      (fun a => (a.1 : WithTop ℝ≥0)) (fun _ => ⊤)
  let q : E → Measure E := fun y =>
    (volume : Measure E).tilted (fun x => -V x - ‖x - y‖ ^ 2 / (2 * η))
  let γ : Measure E := stdGaussian E
  let M : E → Measure ((E × E) × (ℕ → ℝ)) := fun y => ((q y).prod γ).prod P
  let tπ : ℝ≥0 := ⟨Real.pi, Real.pi_pos.le⟩

Exact contiguous compiled proof region; earlier local definitions and facts remain in scope.

2. Consume the actual joint phase and derive the Gibbs normalization

The verified actual phase supplies joint Borel measurability and actual deterministic/per-parameter AE properties. The existing Gibbs augmentation gives a positive integral of exp(−V). A nonzero Bochner integral implies integrability, so its normalized exponential tilt is a probability measure. No minimizer, moment or normalizer certificate is supplied.

\[0<\int e^{-V}\Longrightarrow e^{-V}\in L^1,\quad\mu=\operatorname{tilt}_{-V}(dr)\in\mathcal P(E).\]
Corresponding Lean step
  have h80 := ActualPhysicalTimeMeasurability.actual_physical_time_measurable_phase
    hα hαβ hV hH hη hβη
  obtain ⟨Z, hZM, hcovered, hfallback, hAE⟩ := h80
  have hZV := (GibbsAugmentation.normalized_augmentation_density
    hα hV (fun x v => (hH x v).1) hη).1
  have hi : Integrable (fun x : E => Real.exp (-V x)) (volume : Measure E) :=
    Integrable.of_integral_ne_zero hZV.ne'
  let μ : Measure E := (volume : Measure E).tilted (fun x => -V x)
  letI : IsProbabilityMeasure μ := isProbabilityMeasure_tilted hi

Exact contiguous compiled proof region; earlier local definitions and facts remain in scope.

3. Identify the exact everywhere-defined conditional reference kernel

Apply the canonical Gaussian conditional-kernel theorem to the derived Gibbs probability. The pinned successive-tilt identity identifies its quadratic tilt with literal q_y. Kernel fiber probability forces the totalized tilt to be a genuine probability for every y.

\[R_y=\operatorname{tilt}_{-\|\cdot-y\|^2/(2\eta)}(\mu)=q_y,\qquad q_y(E)=1.\]
Corresponding Lean step
  obtain ⟨R, hR, hRy, _⟩ :=
    AutoSamplingTheory.TechnicalLemmas.Probability.GaussianConditionalKernel.exists_tilted_isCondKernel μ hη
  letI : IsMarkovKernel R := hR
  have hRq (y : E) : R y = q y := by
    rw [hRy y, show μ = (volume : Measure E).tilted (fun x => -V x) from rfl,
      tilted_tilted hi]
    congr 1
    funext z
    dsimp only [Pi.add_apply]
    ring
  have hqprob (y : E) : IsProbabilityMeasure (q y) := by
    rw [← hRq y]
    infer_instance
  letI : IsProbabilityMeasure P :=
    AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws.1
  letI : IsProbabilityMeasure γ := inferInstanceAs (IsProbabilityMeasure (stdGaussian E))

Exact contiguous compiled proof region; earlier local definitions and facts remain in scope.

4. Build the actual parameter-dependent independent product kernel

Pull R back by the y coordinate; multiply it by constant Gaussian and actual exponential product kernels. The resulting Q has precisely the source input law M_y at every (y,x). Standard kernel product instances give probability, without an independence assumption hidden in a binder.

\[Q(y,x)=R_y\otimes\gamma\otimes P=M_y.\]
Corresponding Lean step
  let Q : Kernel (E × E) ((E × E) × (ℕ → ℝ)) :=
    ((R.comap Prod.fst measurable_fst) ×ₖ Kernel.const (E × E) γ) ×ₖ
      Kernel.const (E × E) P
  have hQ (y x : E) : Q (y, x) = M y := by
    simp only [Q, Kernel.prod_apply, Kernel.comap_apply, Kernel.const_apply, hRq, M]

Exact contiguous compiled proof region; earlier local definitions and facts remain in scope.

5. Push the actual terminal position through a measurable probability kernel

Joint measurability of Z proves that terminal first-coordinate evaluation F is Borel in input and all random inputs. Retain (y,x) with the identity kernel, multiply by Q and map F. Pinned kernel-map probability gives H mass one, and the Dirac-product/map identities give exactly its source fiber formula.

\[H(y,x)=\bigl[w\mapsto\operatorname{pr}_1 Z(y,w_r,(x,w_p),\pi,w_\omega)\bigr]_\#M_y.\]
Corresponding Lean step
  let F : (E × E) × ((E × E) × (ℕ → ℝ)) → E :=
    fun a => (Z a.1.1 a.2.1.1 (a.1.2, a.2.1.2) tπ a.2.2).1
  have hFM : Measurable F :=
    (hZM.comp ((measurable_fst.fst.prodMk measurable_snd.fst.fst).prodMk
      (measurable_fst.snd.prodMk measurable_snd.fst.snd) |>.prodMk
        (measurable_const.prodMk measurable_snd.snd))).fst
  let H : Kernel (E × E) E := (Kernel.id ×ₖ Q).map F
  have hHkernel : IsMarkovKernel H := Kernel.IsMarkovKernel.map _ hFM
  have hHlaw (y x : E) : H (y, x) = Measure.map
      (fun w : (E × E) × (ℕ → ℝ) => (Z y w.1.1 (x, w.1.2) tπ w.2).1) (M y) := by
    dsimp only [H]
    rw [Kernel.map_apply _ hFM, Kernel.prod_apply, Kernel.id_apply, hQ,
      Measure.dirac_prod, Measure.map_map hFM (by fun_prop)]
    rfl

Exact contiguous compiled proof region; earlier local definitions and facts remain in scope.

6. Retrieve measurable actual records, clocks, waits and flow

Use the verified finite recursion, harmonic flow and integrated hazard clock as genuine dependencies. Coordinate clamping is measurable. These inputs will prove measurability of the full finite-time arc predicate before any product-AE lifting.

\[\operatorname{record}_n,T_n,\tau,\Phi,\varepsilon\text{ are jointly Borel}.\]
Corresponding Lean step
  have h76 := ActualFiniteJumpRecursion.actual_fixed_reference_finite_jump_recursion
    hα hαβ hV hH hη hβη
  rcases h76 with ⟨_, _, _, hrecordM, htimeM, _, _, _, _, _⟩
  have hΦM : Measurable (fun a : (E × E) × ℝ × (E × E) =>
      Φ a.1.1 a.1.2 a.2.1 a.2.2) :=
    (ActualHarmonicFlow.actual_harmonic_flow_laws hα hαβ hV hH hη hβη).2.1
  have hτM : Measurable (fun a : (E × E) × (E × E) × ℝ≥0 =>
      τ a.1.1 a.1.2 a.2.1 a.2.2) := (ActualHazardClock.actual_integrated_hazard_clock_laws
    hα hαβ hV hH hη hβη).2.2.2.2.2.2.1
  have hεM : Measurable ε := measurable_pi_lambda _ fun n =>
    measurable_real_toNNReal.comp (measurable_pi_apply n)
  let W := (E × E) × (ℕ → ℝ)

Exact contiguous compiled proof region; earlier local definitions and facts remain in scope.

7. Eliminate the apparent uncountable record witness

Fix y,x. Pull back actual records/clocks to W=((reference,momentum),sample). The total Sum projection L_n chooses the live record and has a dummy branch only to make it Borel everywhere. Include record_n=inl(L_n) explicitly, so a stopped record cannot supply a source phase. Composing with Z, τ and Φ gives measurable origin/wait/branch maps.

\[\operatorname{record}_n=\mathrm{inl}(a)\Longrightarrow L_n=a;\quad\text{only }\exists n\in\mathbb N\text{ remains}.\]
Corresponding Lean step
  have hgood (y x : E) : ∀ᵐ w ∂M y,
      Z y w.1.1 (x, w.1.2) 0 w.2 = (x, w.1.2) ∧
      ∃ n : ℕ, ∃ a : ℝ≥0 × (E × E),
        eventTime y w.1.1 (x, w.1.2) (ε w.2) n ≤ (tπ : WithTop ℝ≥0) ∧
        (tπ : WithTop ℝ≥0) < eventTime y w.1.1 (x, w.1.2) (ε w.2) (n + 1) ∧
        record y w.1.1 (x, w.1.2) (ε w.2) n = Sum.inl a ∧ a.1 ≤ tπ ∧
        ((tπ - a.1 : ℝ≥0) : WithTop ℝ≥0) < τ y w.1.1 a.2 (ε w.2 n) ∧
        Z y w.1.1 (x, w.1.2) tπ w.2 = Φ y w.1.1 ((tπ - a.1 : ℝ≥0) : ℝ) a.2 := by
    letI : IsProbabilityMeasure (q y) := hqprob y
    let args : W → (E × E) × (E × E) × (ℕ → ℝ≥0) :=
      fun w => ((y, w.1.1), (x, w.1.2), ε w.2)
    have hargs : Measurable args := (measurable_const.prodMk measurable_fst.fst).prodMk
      ((measurable_const.prodMk measurable_fst.snd).prodMk (hεM.comp measurable_snd))
    have hrM (n : ℕ) : Measurable (fun w : W => record y w.1.1 (x, w.1.2) (ε w.2) n) :=
      (hrecordM n).comp hargs
    have htM (n : ℕ) : Measurable (fun w : W => eventTime y w.1.1 (x, w.1.2) (ε w.2) n) :=
      (htimeM n).comp hargs
    let L : ℕ → W → ℝ≥0 × (E × E) := fun n w =>
      (record y w.1.1 (x, w.1.2) (ε w.2) n).elim id (fun _ => (0, (0, 0)))
    have hLM (n : ℕ) : Measurable (L n) :=
      (measurable_id.sumElim measurable_const).comp (hrM n)
    have hzM (t : ℝ≥0) : Measurable (fun w : W => Z y w.1.1 (x, w.1.2) t w.2) :=
      hZM.comp (((measurable_const.prodMk measurable_fst.fst).prodMk
        (measurable_const.prodMk measurable_fst.snd)).prodMk
          (measurable_const.prodMk measurable_snd))
    have hwaitM (n : ℕ) : Measurable (fun w : W => τ y w.1.1 (L n w).2 (ε w.2 n)) := by
      have heM : Measurable (fun w : W => ε w.2 n) :=
        measurable_real_toNNReal.comp ((measurable_pi_apply n).comp measurable_snd)
      have haM : Measurable (fun w : W => ((y, w.1.1), (L n w).2, ε w.2 n)) :=
        (measurable_const.prodMk measurable_fst.fst).prodMk ((hLM n).snd.prodMk heM)
      have hcomp := hτM.comp haM
      exact hcomp
    have hbranchM (n : ℕ) : Measurable (fun w : W =>
        Φ y w.1.1 ((tπ - (L n w).1 : ℝ≥0) : ℝ) (L n w).2) :=
      hΦM.comp ((measurable_const.prodMk measurable_fst.fst).prodMk
        ((measurable_coe_nnreal_real.comp (measurable_const.sub (hLM n).fst)).prodMk
          (hLM n).snd))
    have hLiveM (n : ℕ) : MeasurableSet {w : W |
        record y w.1.1 (x, w.1.2) (ε w.2) n = Sum.inl (L n w)} := by
      have heq : {w : W | record y w.1.1 (x, w.1.2) (ε w.2) n = Sum.inl (L n w)} =
          (fun w : W => record y w.1.1 (x, w.1.2) (ε w.2) n) ⁻¹'
            Set.range (Sum.inl : (ℝ≥0 × (E × E)) → ((ℝ≥0 × (E × E)) ⊕ Unit)) := by
        ext w
        change _ ↔ ∃ a, Sum.inl a = record y w.1.1 (x, w.1.2) (ε w.2) n
        constructor
        · intro hw
          exact ⟨L n w, hw.symm⟩
        · rintro ⟨a, ha⟩
          have hLa : L n w = a := by
            change (record y w.1.1 (x, w.1.2) (ε w.2) n).elim id (fun _ => (0, (0, 0))) = a
            rw [← ha]
            rfl
          change record y w.1.1 (x, w.1.2) (ε w.2) n = Sum.inl (L n w)
          rw [hLa]
          exact ha.symm
      rw [heq]
      exact measurableSet_range_inl.preimage (hrM n)

Exact contiguous compiled proof region; earlier local definitions and facts remain in scope.

8. Prove that actual origin and terminal agreement form a Borel event

Each D_n includes both half-open clock bounds, a live-record equality, stored time≤π, elapsed strictly below the next wait, and actual Z-to-flow equality. Borel order/equality and countable union give G={Z0=(x,p)}∩⋃D_n measurable. This avoids asserting measurability of an uncountable all-time intersection.

\[G=\{Z_0=(x,p)\}\cap\bigcup_{n\in\mathbb N}D_n\quad\text{is Borel}.\]
Corresponding Lean step
    let D : ℕ → Set W := fun n => {w |
      eventTime y w.1.1 (x, w.1.2) (ε w.2) n ≤ (tπ : WithTop ℝ≥0) ∧
      (tπ : WithTop ℝ≥0) < eventTime y w.1.1 (x, w.1.2) (ε w.2) (n + 1) ∧
      record y w.1.1 (x, w.1.2) (ε w.2) n = Sum.inl (L n w) ∧ (L n w).1 ≤ tπ ∧
      ((tπ - (L n w).1 : ℝ≥0) : WithTop ℝ≥0) < τ y w.1.1 (L n w).2 (ε w.2 n) ∧
      Z y w.1.1 (x, w.1.2) tπ w.2 = Φ y w.1.1 ((tπ - (L n w).1 : ℝ≥0) : ℝ) (L n w).2}
    have hDM (n : ℕ) : MeasurableSet (D n) :=
      (measurableSet_le (htM n) measurable_const).inter
        ((measurableSet_lt measurable_const (htM (n + 1))).inter
          ((hLiveM n).inter
            ((measurableSet_le (hLM n).fst measurable_const).inter
              ((measurableSet_lt
                (WithTop.measurable_coe.comp (measurable_const.sub (hLM n).fst))
                (hwaitM n)).inter (measurableSet_eq_fun (hzM tπ) (hbranchM n))))))
    let G : Set W := {w | Z y w.1.1 (x, w.1.2) 0 w.2 = (x, w.1.2)} ∩ ⋃ n, D n
    have hGM : MeasurableSet G :=
      (measurableSet_eq_fun (hzM 0) (measurable_const.prodMk measurable_fst.snd)).inter
        (MeasurableSet.iUnion hDM)

Exact contiguous compiled proof region; earlier local definitions and facts remain in scope.

9. Lift verified fixed-input good sections by product Fubini

For each fixed reference/momentum, actual80 supplies a P-AE all-time arc and origin event. At π its live record equals L_n. Since the full finite-time event G is measurable, product Fubini lifts these sections to M_y-AE G. Expanding G returns the actual live witness and both origin/terminal conclusions.

\[\forall(r,p),\ P\text{-a.s. }G(r,p,\omega)\Longrightarrow((q_y\otimes\gamma)\otimes P)(G)=1.\]
Corresponding Lean step
    have hGAE : ∀ᵐ w ∂M y, w ∈ G := by
      apply (Measure.ae_prod_iff_ae_ae hGM).mpr
      filter_upwards with u
      filter_upwards [hAE y u.1 (x, u.2)] with sample hs
      refine ⟨hs.2, Set.mem_iUnion.mpr ?_⟩
      obtain ⟨n, a, hl, hu, hr, ha, hw, hz⟩ := hs.1 tπ
      have hr' : record y u.1 (x, u.2) (ε sample) n = Sum.inl a := hr
      have hLa : L n (u, sample) = a := by
        change (record y u.1 (x, u.2) (ε sample) n).elim id (fun _ => (0, (0, 0))) = a
        rw [hr']
        rfl
      refine ⟨n, ?_⟩
      change _ ∧ _ ∧ _ ∧ _ ∧ _ ∧ _
      rw [hLa]
      exact ⟨hl, hu, hr, ha, hw, hz⟩
    filter_upwards [hGAE] with w hw
    obtain ⟨n, hn⟩ := Set.mem_iUnion.mp hw.2
    exact ⟨hw.1, n, L n w, hn⟩

Exact contiguous compiled proof region; earlier local definitions and facts remain in scope.

10. Derive the physical initialization law from the actual Gaussian marginal

Return the constructed Z,R,H and proven actual product-AE terminal statement. AE map congruence replaces Z0 by (x,p); the independent product marginal of p is exactly γ because q_y and P have mass one. Its pushforward by p↦(x,p) is δ_x⊗γ.

\[\bigl[w\mapsto Z(y,w_r,(x,w_p),0,w_\omega)\bigr]_\#M_y=\delta_x\otimes\gamma.\]
Corresponding Lean step
  refine ⟨Z, hZM, hcovered, hfallback, hAE, R, hR, hRq, H, hHkernel, hHlaw, ?_, hgood⟩
  intro y x
  letI : IsProbabilityMeasure (q y) := hqprob y
  rw [Measure.map_congr ((hgood y x).mono (fun w hw => hw.1)), Measure.dirac_prod]
  have hmarg : Measure.map (fun w : W => w.1.2) (M y) = γ := by
    change Measure.map (Prod.snd ∘ Prod.fst) (((q y).prod γ).prod P) = γ
    rw [← Measure.map_map measurable_snd measurable_fst]
    simp
  calc
    Measure.map (fun w : W => (x, w.1.2)) (M y) =
        Measure.map (Prod.mk x) (Measure.map (fun w : W => w.1.2) (M y)) :=
      (Measure.map_map (by fun_prop) (by fun_prop)).symm
    _ = Measure.map (Prod.mk x) γ := by rw [hmarg]

Exact contiguous compiled proof region; earlier local definitions and facts remain in scope.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · ideal_half_turn_returned_position_kernel

Retain actual dynamics and specify independent source inputs; Consume the actual joint phase and derive the Gibbs normalization; Identify the exact everywhere-defined conditional reference kernel; Build the actual parameter-dependent independent product kernel; Push the actual terminal position through a measurable probability kernel; Retrieve measurable actual records, clocks, waits and flow; Eliminate the apparent uncountable record witness; Prove that actual origin and terminal agreement form a Borel event; Lift verified fixed-input good sections by product Fubini; Derive the physical initialization law from the actual Gaussian marginal

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)
theorem ideal_half_turn_returned_position_kernel
    {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) :
    ideal_half_turn_returned_position_kernel_statement hα hαβ hV hH hη hβη := by
  classical
  let P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
  let ε : (ℕ → ℝ) → ℕ → ℝ≥0 := fun sample k => Real.toNNReal (sample k)
  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 eventTime : E → E → (E × E) → (ℕ → ℝ≥0) → ℕ → WithTop ℝ≥0 :=
    fun y xRef z₀ e n => (record y xRef z₀ e n).elim
      (fun a => (a.1 : WithTop ℝ≥0)) (fun _ => ⊤)
  let q : E → Measure E := fun y =>
    (volume : Measure E).tilted (fun x => -V x - ‖x - y‖ ^ 2 / (2 * η))
  let γ : Measure E := stdGaussian E
  let M : E → Measure ((E × E) × (ℕ → ℝ)) := fun y => ((q y).prod γ).prod P
  let tπ : ℝ≥0 := ⟨Real.pi, Real.pi_pos.le⟩
  have h80 := ActualPhysicalTimeMeasurability.actual_physical_time_measurable_phase
    hα hαβ hV hH hη hβη
  obtain ⟨Z, hZM, hcovered, hfallback, hAE⟩ := h80
  have hZV := (GibbsAugmentation.normalized_augmentation_density
    hα hV (fun x v => (hH x v).1) hη).1
  have hi : Integrable (fun x : E => Real.exp (-V x)) (volume : Measure E) :=
    Integrable.of_integral_ne_zero hZV.ne'
  let μ : Measure E := (volume : Measure E).tilted (fun x => -V x)
  letI : IsProbabilityMeasure μ := isProbabilityMeasure_tilted hi
  obtain ⟨R, hR, hRy, _⟩ :=
    AutoSamplingTheory.TechnicalLemmas.Probability.GaussianConditionalKernel.exists_tilted_isCondKernel μ hη
  letI : IsMarkovKernel R := hR
  have hRq (y : E) : R y = q y := by
    rw [hRy y, show μ = (volume : Measure E).tilted (fun x => -V x) from rfl,
      tilted_tilted hi]
    congr 1
    funext z
    dsimp only [Pi.add_apply]
    ring
  have hqprob (y : E) : IsProbabilityMeasure (q y) := by
    rw [← hRq y]
    infer_instance
  letI : IsProbabilityMeasure P :=
    AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws.1
  letI : IsProbabilityMeasure γ := inferInstanceAs (IsProbabilityMeasure (stdGaussian E))
  let Q : Kernel (E × E) ((E × E) × (ℕ → ℝ)) :=
    ((R.comap Prod.fst measurable_fst) ×ₖ Kernel.const (E × E) γ) ×ₖ
      Kernel.const (E × E) P
  have hQ (y x : E) : Q (y, x) = M y := by
    simp only [Q, Kernel.prod_apply, Kernel.comap_apply, Kernel.const_apply, hRq, M]
  let F : (E × E) × ((E × E) × (ℕ → ℝ)) → E :=
    fun a => (Z a.1.1 a.2.1.1 (a.1.2, a.2.1.2) tπ a.2.2).1
  have hFM : Measurable F :=
    (hZM.comp ((measurable_fst.fst.prodMk measurable_snd.fst.fst).prodMk
      (measurable_fst.snd.prodMk measurable_snd.fst.snd) |>.prodMk
        (measurable_const.prodMk measurable_snd.snd))).fst
  let H : Kernel (E × E) E := (Kernel.id ×ₖ Q).map F
  have hHkernel : IsMarkovKernel H := Kernel.IsMarkovKernel.map _ hFM
  have hHlaw (y x : E) : H (y, x) = Measure.map
      (fun w : (E × E) × (ℕ → ℝ) => (Z y w.1.1 (x, w.1.2) tπ w.2).1) (M y) := by
    dsimp only [H]
    rw [Kernel.map_apply _ hFM, Kernel.prod_apply, Kernel.id_apply, hQ,
      Measure.dirac_prod, Measure.map_map hFM (by fun_prop)]
    rfl
  have h76 := ActualFiniteJumpRecursion.actual_fixed_reference_finite_jump_recursion
    hα hαβ hV hH hη hβη
  rcases h76 with ⟨_, _, _, hrecordM, htimeM, _, _, _, _, _⟩
  have hΦM : Measurable (fun a : (E × E) × ℝ × (E × E) =>
      Φ a.1.1 a.1.2 a.2.1 a.2.2) :=
    (ActualHarmonicFlow.actual_harmonic_flow_laws hα hαβ hV hH hη hβη).2.1
  have hτM : Measurable (fun a : (E × E) × (E × E) × ℝ≥0 =>
      τ a.1.1 a.1.2 a.2.1 a.2.2) := (ActualHazardClock.actual_integrated_hazard_clock_laws
    hα hαβ hV hH hη hβη).2.2.2.2.2.2.1
  have hεM : Measurable ε := measurable_pi_lambda _ fun n =>
    measurable_real_toNNReal.comp (measurable_pi_apply n)
  let W := (E × E) × (ℕ → ℝ)
  have hgood (y x : E) : ∀ᵐ w ∂M y,
      Z y w.1.1 (x, w.1.2) 0 w.2 = (x, w.1.2) ∧
      ∃ n : ℕ, ∃ a : ℝ≥0 × (E × E),
        eventTime y w.1.1 (x, w.1.2) (ε w.2) n ≤ (tπ : WithTop ℝ≥0) ∧
        (tπ : WithTop ℝ≥0) < eventTime y w.1.1 (x, w.1.2) (ε w.2) (n + 1) ∧
        record y w.1.1 (x, w.1.2) (ε w.2) n = Sum.inl a ∧ a.1 ≤ tπ ∧
        ((tπ - a.1 : ℝ≥0) : WithTop ℝ≥0) < τ y w.1.1 a.2 (ε w.2 n) ∧
        Z y w.1.1 (x, w.1.2) tπ w.2 = Φ y w.1.1 ((tπ - a.1 : ℝ≥0) : ℝ) a.2 := by
    letI : IsProbabilityMeasure (q y) := hqprob y
    let args : W → (E × E) × (E × E) × (ℕ → ℝ≥0) :=
      fun w => ((y, w.1.1), (x, w.1.2), ε w.2)
    have hargs : Measurable args := (measurable_const.prodMk measurable_fst.fst).prodMk
      ((measurable_const.prodMk measurable_fst.snd).prodMk (hεM.comp measurable_snd))
    have hrM (n : ℕ) : Measurable (fun w : W => record y w.1.1 (x, w.1.2) (ε w.2) n) :=
      (hrecordM n).comp hargs
    have htM (n : ℕ) : Measurable (fun w : W => eventTime y w.1.1 (x, w.1.2) (ε w.2) n) :=
      (htimeM n).comp hargs
    let L : ℕ → W → ℝ≥0 × (E × E) := fun n w =>
      (record y w.1.1 (x, w.1.2) (ε w.2) n).elim id (fun _ => (0, (0, 0)))
    have hLM (n : ℕ) : Measurable (L n) :=
      (measurable_id.sumElim measurable_const).comp (hrM n)
    have hzM (t : ℝ≥0) : Measurable (fun w : W => Z y w.1.1 (x, w.1.2) t w.2) :=
      hZM.comp (((measurable_const.prodMk measurable_fst.fst).prodMk
        (measurable_const.prodMk measurable_fst.snd)).prodMk
          (measurable_const.prodMk measurable_snd))
    have hwaitM (n : ℕ) : Measurable (fun w : W => τ y w.1.1 (L n w).2 (ε w.2 n)) := by
      have heM : Measurable (fun w : W => ε w.2 n) :=
        measurable_real_toNNReal.comp ((measurable_pi_apply n).comp measurable_snd)
      have haM : Measurable (fun w : W => ((y, w.1.1), (L n w).2, ε w.2 n)) :=
        (measurable_const.prodMk measurable_fst.fst).prodMk ((hLM n).snd.prodMk heM)
      have hcomp := hτM.comp haM
      exact hcomp
    have hbranchM (n : ℕ) : Measurable (fun w : W =>
        Φ y w.1.1 ((tπ - (L n w).1 : ℝ≥0) : ℝ) (L n w).2) :=
      hΦM.comp ((measurable_const.prodMk measurable_fst.fst).prodMk
        ((measurable_coe_nnreal_real.comp (measurable_const.sub (hLM n).fst)).prodMk
          (hLM n).snd))
    have hLiveM (n : ℕ) : MeasurableSet {w : W |
        record y w.1.1 (x, w.1.2) (ε w.2) n = Sum.inl (L n w)} := by
      have heq : {w : W | record y w.1.1 (x, w.1.2) (ε w.2) n = Sum.inl (L n w)} =
          (fun w : W => record y w.1.1 (x, w.1.2) (ε w.2) n) ⁻¹'
            Set.range (Sum.inl : (ℝ≥0 × (E × E)) → ((ℝ≥0 × (E × E)) ⊕ Unit)) := by
        ext w
        change _ ↔ ∃ a, Sum.inl a = record y w.1.1 (x, w.1.2) (ε w.2) n
        constructor
        · intro hw
          exact ⟨L n w, hw.symm⟩
        · rintro ⟨a, ha⟩
          have hLa : L n w = a := by
            change (record y w.1.1 (x, w.1.2) (ε w.2) n).elim id (fun _ => (0, (0, 0))) = a
            rw [← ha]
            rfl
          change record y w.1.1 (x, w.1.2) (ε w.2) n = Sum.inl (L n w)
          rw [hLa]
          exact ha.symm
      rw [heq]
      exact measurableSet_range_inl.preimage (hrM n)
    let D : ℕ → Set W := fun n => {w |
      eventTime y w.1.1 (x, w.1.2) (ε w.2) n ≤ (tπ : WithTop ℝ≥0) ∧
      (tπ : WithTop ℝ≥0) < eventTime y w.1.1 (x, w.1.2) (ε w.2) (n + 1) ∧
      record y w.1.1 (x, w.1.2) (ε w.2) n = Sum.inl (L n w) ∧ (L n w).1 ≤ tπ ∧
      ((tπ - (L n w).1 : ℝ≥0) : WithTop ℝ≥0) < τ y w.1.1 (L n w).2 (ε w.2 n) ∧
      Z y w.1.1 (x, w.1.2) tπ w.2 = Φ y w.1.1 ((tπ - (L n w).1 : ℝ≥0) : ℝ) (L n w).2}
    have hDM (n : ℕ) : MeasurableSet (D n) :=
      (measurableSet_le (htM n) measurable_const).inter
        ((measurableSet_lt measurable_const (htM (n + 1))).inter
          ((hLiveM n).inter
            ((measurableSet_le (hLM n).fst measurable_const).inter
              ((measurableSet_lt
                (WithTop.measurable_coe.comp (measurable_const.sub (hLM n).fst))
                (hwaitM n)).inter (measurableSet_eq_fun (hzM tπ) (hbranchM n))))))
    let G : Set W := {w | Z y w.1.1 (x, w.1.2) 0 w.2 = (x, w.1.2)} ∩ ⋃ n, D n
    have hGM : MeasurableSet G :=
      (measurableSet_eq_fun (hzM 0) (measurable_const.prodMk measurable_fst.snd)).inter
        (MeasurableSet.iUnion hDM)
    have hGAE : ∀ᵐ w ∂M y, w ∈ G := by
      apply (Measure.ae_prod_iff_ae_ae hGM).mpr
      filter_upwards with u
      filter_upwards [hAE y u.1 (x, u.2)] with sample hs
      refine ⟨hs.2, Set.mem_iUnion.mpr ?_⟩
      obtain ⟨n, a, hl, hu, hr, ha, hw, hz⟩ := hs.1 tπ
      have hr' : record y u.1 (x, u.2) (ε sample) n = Sum.inl a := hr
      have hLa : L n (u, sample) = a := by
        change (record y u.1 (x, u.2) (ε sample) n).elim id (fun _ => (0, (0, 0))) = a
        rw [hr']
        rfl
      refine ⟨n, ?_⟩
      change _ ∧ _ ∧ _ ∧ _ ∧ _ ∧ _
      rw [hLa]
      exact ⟨hl, hu, hr, ha, hw, hz⟩
    filter_upwards [hGAE] with w hw
    obtain ⟨n, hn⟩ := Set.mem_iUnion.mp hw.2
    exact ⟨hw.1, n, L n w, hn⟩
  refine ⟨Z, hZM, hcovered, hfallback, hAE, R, hR, hRq, H, hHkernel, hHlaw, ?_, hgood⟩
  intro y x
  letI : IsProbabilityMeasure (q y) := hqprob y
  rw [Measure.map_congr ((hgood y x).mono (fun w hw => hw.1)), Measure.dirac_prod]
  have hmarg : Measure.map (fun w : W => w.1.2) (M y) = γ := by
    change Measure.map (Prod.snd ∘ Prod.fst) (((q y).prod γ).prod P) = γ
    rw [← Measure.map_map measurable_snd measurable_fst]
    simp
  calc
    Measure.map (fun w : W => (x, w.1.2)) (M y) =
        Measure.map (Prod.mk x) (Measure.map (fun w : W => w.1.2) (M y)) :=
      (Measure.map_map (by fun_prop) (by fun_prop)).symm
    _ = Measure.map (Prod.mk x) γ := by rw [hmarg]

end
end AutoSamplingTheory.ExampleCases.ProximalBPS.IdealHalfTurnKernel

Exact module and namespace context

Scope and omitted-condition boundaries
  • Ideal exact-reference probability kernel at pi and product-input AE actual origin/terminal arc only. Fixed V/alpha/beta/eta; no arbitrary correlated input substitution. Full random all-time path law/version uniqueness, implementation/reference approximation/oracle costs, phase Markov/semigroup/invariance/reversibility/hypocoercivity/main/composition and reader visual/main/PURIFIED/live remain OPEN.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • tilted_tilted
  • Integrable.of_integral_ne_zero
  • isProbabilityMeasure_tilted
  • Kernel.comap
  • Kernel.prod
  • Kernel.prod_apply
  • Kernel.map_apply
  • Kernel.IsMarkovKernel.map
  • Measure.dirac_prod
  • Measure.map_map
  • Measure.map_congr
  • Measure.map_fst_prod
  • Measure.map_snd_prod
  • Measure.ae_prod_iff_ae_ae
  • measurableSet_range_inl
  • measurableSet_eq_fun
  • MeasurableSet.iUnion
  • Measurable.sumElim

Mathematical sources

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.