ActualWeightedSector: mathematical reading route

Mathematical statement

Let E be a finite-dimensional real inner-product space equipped with its Borel sigma algebra; zero dimension is allowed. Let alpha,beta≥0, eta be real, V:E→R. Assume exactly alpha>0, alpha≤beta, V is C2, alpha||v||^2≤D2V(x)[v,v]≤beta||v||^2 for every x,v, eta>0 and beta*eta≤1. All conclusions hold for every y,r in E, initial phase z0=(x0,p0), integer n≥0 and finite T≥0. Set c=y-eta*grad V(r). For z=(x,p), define Phi_u(z)=(c+cos(u)(x-c)+sqrt(eta)sin(u)p, -sin(u)/sqrt(eta)(x-c)+cos(u)p). Define h_r(x)=grad V(x)-grad V(r), S_r(x,p)=(x,p-[2<p,h_r(x)>/||h_r(x)||^2]h_r(x)) with real division totalized by 0/0=0, lambda_r(x,p)=sqrt(eta)max(0,<p,h_r(x)>), and Lambda_z(u)=integral from0 to u of lambda_r(Phi_s(z)) ds for u≥0, using Lebesgue measure. A tagged record is either live(a,z), with a≥0, or stopped; Hist_n is the type of all n+1 records. Let Delta_n(T) be the strict simplex 0<t1<...<tn<T. Write a0=0, ai=ti (1≤i≤n), a_(n+1)=T. Given t in Delta_n(T), define z_i=S_r(Phi_(a_i-a_(i-1))(z_(i-1))) for1≤i≤n and K_n(t)_j=live(a_j,z_j). The literal Lean nonnegative conversions preserve these nonnegative times. Define qReal_n(t)=product_(i=1)^n [lambda_r(Phi_(a_i-a_(i-1))(z_(i-1))) exp(-Lambda_(z_(i-1))(a_i-a_(i-1)))], q_n=ofReal(qReal_n). For arbitrary histories let readTime(live(a,z))=a and readTime(stopped)=0; d_n(T,h)=max(T-readTime(h_n),0). Put W(live(a,z),u)=ofReal(exp(-Lambda_z(u))) and W(stopped,u)=0. Define rho_n(T,t)=q_n(t) W(K_n(t)_n,d_n(T,K_n(t))). Here ofReal(x) is max(x,0) embedded into extended nonnegative reals; no probability law or normalization is assumed in this deterministic identity. Define Path_T as all phase-valued functions on[0,T]. The total interpolation Psi_n(h)(s) starts at z0 and scans records j=0,...,n in order: a live(a,z) record with a≤s replaces the accumulator by Phi_(max(s-a,0))(z); otherwise it is unchanged. Set Gamma_n(t)=Psi_n(K_n(t)). Extend this particular prescribed path to all real times by gamma(s)=Gamma_n(t)(min(max(s,0),T)). This extension agrees with Gamma on[0,T]; no topology on an entire function space is asserted. Define R(x,p)=(x,-p), U_y(x,p)=V(x)+||x-y||^2/(2 eta)+||p||^2/2 and w_y(z)=exp(-U_y(z)). Let ell=(Lebesgue measure on E) times (Lebesgue measure on E), and m_n,T be the comap of Lebesgue measure on R^n by the inclusion of the strict simplex Prefix_n(T). Equip X_n,T=(E times E) times Prefix_n(T) with its Borel product/subtype sigma algebra and phase-first measure mu_n,T=ell times m_n,T, without normalization or a factorial factor. For every n≥0 and T≥0 there exists one map rho:Prefix_n(T)→Prefix_n(T), with (rho(t))_i=T-t_(n+1-i) in one-based coordinates, which serves all y,r and observables below. For q=(z,t) set A(q)=Gamma_(y,r,z,n,T,t)(T), Theta(q)=(R(A(q)),rho(t)), and W(q)=ofReal(w_y(z))*rho_(y,r,z,n,T)(t); the density rho remains the actual q_n times terminal survival defined above. For every measurable F:X_n,T→[0,infinity], integral W(q)*F(Theta(q)) dmu_n,T(q) = integral W(q)*F(q) dmu_n,T(q). Both integrals are nonnegative Lebesgue integrals and may be infinite, with 0*infinity=0. Measurability of F is the test-domain condition; the actual weight's joint measurability, map's measure preservation and weight matching are proved internally from the six analytic assumptions. No finite-mass, finite-integral, normalization or positivity-of-rate premise is added. The result includes n=0, T=0, rank-zero E, zero normals and zero rates; the simplex is empty for n>0,T=0. This extends the source bounded nonnegative test substitution to measurable ENNReal tests without asserting integrability. It proves only the unnormalized finite-sector change of variables. Normalized Gibbs averaging, countable summation, signed-test integrability, invariance, restart/Markovness, hypocoercivity, simulation errors, expected costs and full paper/composition results remain separate.

theorem actual_weighted_sector_lintegral
    {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_weighted_sector_statement hα hαβ hV hH hη hβη

private def actual_weighted_sector_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 := by
  classical
  exact
    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 Rec := (ℝ≥0 × (E × E)) ⊕ Unit
    let Hist : ℕ → Type _ := fun n => Fin (n + 1) → Rec
    let Δ : (n : ℕ) → ℝ≥0 → Set (Fin n → ℝ) := fun n T =>
      {t | StrictMono (Fin.cons (0 : ℝ) t) ∧ ∀ i, t i < (T : ℝ)}
    let Prefix : (n : ℕ) → ℝ≥0 → Type := fun n T => {t : Fin n → ℝ // t ∈ Δ n T}
    let zAt : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → Fin (n + 1) → (E × E) := fun y xRef z₀ n T t =>
      Fin.induction z₀ (fun i z =>
        S xRef (Φ y xRef (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc) z))
    let K : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → Hist n := fun y xRef z₀ n T t j =>
      Sum.inl (Real.toNNReal ((Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) j), zAt y xRef z₀ n T t j)
    let qReal : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → ℝ := fun y xRef z₀ n T t =>
      ∏ i : Fin n,
        rate xRef (Φ y xRef (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc)
          (zAt y xRef z₀ n T t i.castSucc)) *
        Real.exp (-Λ y xRef (zAt y xRef z₀ n T t i.castSucc)
          (Real.toNNReal (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc)))
    let q : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → ℝ≥0∞ := fun y xRef z₀ n T t =>
      ENNReal.ofReal (qReal y xRef z₀ n T t)
    let liveTime : Rec → ℝ≥0 := fun r => r.elim Prod.fst (fun _ => 0)
    let d : (n : ℕ) → ℝ≥0 → Hist n → ℝ≥0 :=
      fun n T h => T - liveTime (h ⟨n, Nat.lt_succ_self n⟩)
    let weight : E → E → Rec → ℝ≥0 → ℝ≥0∞ :=
      fun y xRef r u => r.elim
        (fun a => ENNReal.ofReal (Real.exp (-Λ y xRef a.2 u))) (fun _ => 0)
    let Path : ℝ≥0 → Type _ := fun T => {s : ℝ≥0 // s ≤ T} → E × E
    let Ψ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Hist n → Path T :=
      fun y xRef z₀ n T h s =>
        Fin.foldl (n + 1) (fun z j => (h j).elim
          (fun a => if a.1 ≤ s.val then Φ y xRef ((s.val - a.1 : ℝ≥0) : ℝ) a.2 else z)
          (fun _ => z)) z₀
    let Γ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Prefix n T → Path T :=
      fun y xRef z₀ n T t => Ψ y xRef z₀ n T (K y xRef z₀ n T t)
    let ρ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Prefix n T → ℝ≥0∞ :=
      fun y xRef z₀ n T t => q y xRef z₀ n T t *
        weight y xRef ((K y xRef z₀ n T t) ⟨n, Nat.lt_succ_self n⟩)
          (d n T (K y xRef z₀ n T t))
    let R : E × E → E × E := fun z => (z.1, -z.2)
    let U : E → E × E → ℝ := fun y z =>
      V z.1 + ‖z.1 - y‖ ^ 2 / (2 * η) + ‖z.2‖ ^ 2 / 2
    let w : E → E × E → ℝ := fun y z => Real.exp (-U y z)
    let ell : Measure (E × E) := (volume : Measure E).prod (volume : Measure E)
    let m : (n : ℕ) → (T : ℝ≥0) → Measure (Prefix n T) := fun n T =>
      Measure.comap (fun t : Prefix n T => t.val) (volume : Measure (Fin n → ℝ))
    ∀ n : ℕ, ∀ T : ℝ≥0, ∃ rho : Prefix n T → Prefix n T,
      (∀ t : Prefix n T, ∀ i : Fin n, (rho t).val i = (T : ℝ) - t.val i.rev) ∧
      ∀ y r : E,
        let A : (E × E) × Prefix n T → E × E :=
          fun q => Γ y r q.1 n T q.2 ⟨T, le_rfl⟩
        let Theta : (E × E) × Prefix n T → (E × E) × Prefix n T :=
          fun q => (R (A q), rho q.2)
        let W : (E × E) × Prefix n T → ℝ≥0∞ :=
          fun q => ENNReal.ofReal (w y q.1) * ρ y r q.1 n T q.2
        ∀ F : (E × E) × Prefix n T → ℝ≥0∞, Measurable F →
          (∫⁻ q, W q * F (Theta q) ∂(ell.prod (m n T))) =
            ∫⁻ q, W q * F q ∂(ell.prod (m n T))

Proof roadmap

1. 1Identify one time reversal

   Use zero-based coordinates i=0,...,n-1. The measure-preserving endpoint map and density balance each produce a reversal with coordinates T-t_(n-1-i). Coordinate extensionality identifies their witnesses before choosing y,r or the test function.

2. 2Preserve the actual phase and time measure

   The actual endpoint/time theorem proves measure preservation on the phase-first Lebesgue times strict-simplex measure. Its endpoint is the actual terminal Gamma, including the final flow arc.

3. 3Preserve the actual weight

   Apply the ENNReal part of the weighted-density theorem. This is the literal Gibbs weight times q_n and terminal survival at both actual inputs; no arbitrary density is substituted.

4. 4Derive joint density measurability

   The actual finite-count path law supplies density measurability jointly in parameters, initial phase and event tuple. Compose it with the measurable embedding that fixes y,r and retains z,t.

5. 5Derive joint Gibbs-weight measurability

   C2 regularity implies continuous V. Squared norms, addition, division by fixed constants and exp show w_y is continuous. Compose with the phase projection and ofReal, then multiply by the joint density.

6. 6Apply nonnegative change of variables

   Replace W(q) by W(Theta q), then apply the measure-preserving lintegral composition theorem to the measurable product W*F. This works even if either integral is infinite; no subtraction, cancellation or normalization is used.