production module
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteJumpRecursion
Read the mathematical statements and proofs in order
2 named declarations scanned from AutoSamplingTheory/ExampleCases/ProximalBPS/ActualFiniteJumpRecursion.lean.
Declarations
def AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteJumpRecursion.actual_fixed_reference_finite_jump_recursion_statement Partial Not mapped
No declaration docstring.
private def actual_fixed_reference_finite_jump_recursion_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 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 H : E → E → (E × E) → ℝ := fun y xRef z =>
(η⁻¹ * ‖z.1 - c y xRef‖ ^ 2 + ‖z.2‖ ^ 2) / 2
let C : E → E → (E × E) → ℝ := fun y xRef z =>
Real.sqrt η * (β : ℝ) * Real.sqrt (2 * H y xRef z) *
(Real.sqrt (2 * η * H y xRef z) + ‖c y xRef - 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
-- Source excerpt truncated; follow the exact source link.AutoSamplingTheory/ExampleCases/ProximalBPS/ActualFiniteJumpRecursion.lean:16published source at ed709a7f320d
Excerpt truncated; the exact source link is authoritative.
theorem AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteJumpRecursion.actual_fixed_reference_finite_jump_recursion Partial Not mapped
Read the complete mathematical statement and proof, with Lean below each
No declaration docstring.
theorem actual_fixed_reference_finite_jump_recursion
{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_fixed_reference_finite_jump_recursion_statement hα hαβ hV hH hη hβη := by
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 H : E → E → (E × E) → ℝ := fun y xRef z =>
(η⁻¹ * ‖z.1 - c y xRef‖ ^ 2 + ‖z.2‖ ^ 2) / 2
let C : E → E → (E × E) → ℝ := fun y xRef z =>
Real.sqrt η * (β : ℝ) * Real.sqrt (2 * H y xRef z) *
(Real.sqrt (2 * η * H y xRef z) + ‖c y xRef - 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 :=
-- Source excerpt truncated; follow the exact source link.AutoSamplingTheory/ExampleCases/ProximalBPS/ActualFiniteJumpRecursion.lean:104published source at ed709a7f320dOpen detailed card
Excerpt truncated; the exact source link is authoritative.
Complete Lean source
AutoSamplingTheory/ExampleCases/ProximalBPS/ActualFiniteJumpRecursion.lean — full module with imports and context
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualHazardClock
import Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop
import Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-! Prospective header76 only: actual finite stopped postjump recursion.
Active records are Sum.inl (finite time, phase); Sum.inr () means stopped,
has event time infinity and carries no phase at infinity. Threshold e n is
source E_(n+1). Zero thresholds are a deterministic extension; no global
physical-time phase or iid/nonexplosion/Markov/invariance is asserted. -/
namespace AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteJumpRecursion
open InnerProductSpace MeasureTheory
open scoped ContDiff NNReal ENNReal Topology Interval
noncomputable section
set_option autoImplicit false
private def actual_fixed_reference_finite_jump_recursion_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 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 H : E → E → (E × E) → ℝ := fun y xRef z =>
(η⁻¹ * ‖z.1 - c y xRef‖ ^ 2 + ‖z.2‖ ^ 2) / 2
let C : E → E → (E × E) → ℝ := fun y xRef z =>
Real.sqrt η * (β : ℝ) * Real.sqrt (2 * H y xRef z) *
(Real.sqrt (2 * η * H y xRef z) + ‖c y xRef - 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 _ => ⊤)
(∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0,
record y xRef z₀ e 0 = Sum.inl (0, z₀)) ∧
(∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0, ∀ n : ℕ,
record y xRef z₀ e (n + 1) = next y xRef (e n) (record y xRef z₀ e n) ∧
(∀ a : ℝ≥0 × (E × E), record y xRef z₀ e n = Sum.inl a →
(record y xRef z₀ e (n + 1) = Sum.inr () ↔ τ y xRef a.2 (e n) = ⊤) ∧
(τ y xRef a.2 (e n) ≠ ⊤ → record y xRef z₀ e (n + 1) =
Sum.inl (a.1 + (τ y xRef a.2 (e n)).untopD 0,
S xRef (Φ y xRef (((τ y xRef a.2 (e n)).untopD 0 : ℝ≥0) : ℝ) a.2))))) ∧
Measurable (fun a : (E × E) × ℝ≥0 × ((ℝ≥0 × (E × E)) ⊕ Unit) =>
next a.1.1 a.1.2 a.2.1 a.2.2) ∧
(∀ n : ℕ, Measurable (fun a : (E × E) × (E × E) × (ℕ → ℝ≥0) =>
record a.1.1 a.1.2 a.2.1 a.2.2 n)) ∧
(∀ n : ℕ, Measurable (fun a : (E × E) × (E × E) × (ℕ → ℝ≥0) =>
eventTime a.1.1 a.1.2 a.2.1 a.2.2 n)) ∧
(∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0,
eventTime y xRef z₀ e 0 = 0 ∧ Monotone (eventTime y xRef z₀ e)) ∧
(∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0, ∀ n k : ℕ,
record y xRef z₀ e n = Sum.inr () →
record y xRef z₀ e (n + k) = Sum.inr ()) ∧
(∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0, ∀ n : ℕ,
∀ a : ℝ≥0 × (E × E), record y xRef z₀ e n = Sum.inl a →
H y xRef a.2 = H y xRef z₀ ∧
∀ t : ℝ≥0, (t : WithTop ℝ≥0) < τ y xRef a.2 (e n) →
H y xRef (Φ y xRef (t : ℝ) a.2) = H y xRef z₀ ∧
0 ≤ rate xRef (Φ y xRef (t : ℝ) a.2) ∧
rate xRef (Φ y xRef (t : ℝ) a.2) ≤ C y xRef z₀) ∧
(∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0,
0 ≤ C y xRef z₀ ∧
(0 < C y xRef z₀ → ∀ n : ℕ,
eventTime y xRef z₀ e n +
(Real.toNNReal ((e n : ℝ) / C y xRef z₀) : WithTop ℝ≥0) ≤
eventTime y xRef z₀ e (n + 1)) ∧
(C y xRef z₀ = 0 → ∀ n : ℕ, ∀ a : ℝ≥0 × (E × E),
record y xRef z₀ e n = Sum.inl a → 0 < e n →
record y xRef z₀ e (n + 1) = Sum.inr ())) ∧
(∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0, ∀ n : ℕ,
∀ a : ℝ≥0 × (E × E), record y xRef z₀ e n = Sum.inl a →
(e n = 0 → record y xRef z₀ e (n + 1) = Sum.inl (a.1, S xRef a.2)) ∧
(∀ b : ℝ≥0 × (E × E), 0 < e n →
record y xRef z₀ e (n + 1) = Sum.inl b → a.1 < b.1))
set_option maxHeartbeats 1600000 in
theorem actual_fixed_reference_finite_jump_recursion
{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_fixed_reference_finite_jump_recursion_statement hα hαβ hV hH hη hβη := by
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 H : E → E → (E × E) → ℝ := fun y xRef z =>
(η⁻¹ * ‖z.1 - c y xRef‖ ^ 2 + ‖z.2‖ ^ 2) / 2
let C : E → E → (E × E) → ℝ := fun y xRef z =>
Real.sqrt η * (β : ℝ) * Real.sqrt (2 * H y xRef z) *
(Real.sqrt (2 * η * H y xRef z) + ‖c y xRef - 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 _ => ⊤)
change
(∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0,
record y xRef z₀ e 0 = Sum.inl (0, z₀)) ∧
(∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0, ∀ n : ℕ,
record y xRef z₀ e (n + 1) = next y xRef (e n) (record y xRef z₀ e n) ∧
(∀ a : ℝ≥0 × (E × E), record y xRef z₀ e n = Sum.inl a →
(record y xRef z₀ e (n + 1) = Sum.inr () ↔ τ y xRef a.2 (e n) = ⊤) ∧
(τ y xRef a.2 (e n) ≠ ⊤ → record y xRef z₀ e (n + 1) =
Sum.inl (a.1 + (τ y xRef a.2 (e n)).untopD 0,
S xRef (Φ y xRef (((τ y xRef a.2 (e n)).untopD 0 : ℝ≥0) : ℝ) a.2))))) ∧
Measurable (fun a : (E × E) × ℝ≥0 × ((ℝ≥0 × (E × E)) ⊕ Unit) =>
next a.1.1 a.1.2 a.2.1 a.2.2) ∧
(∀ n : ℕ, Measurable (fun a : (E × E) × (E × E) × (ℕ → ℝ≥0) =>
record a.1.1 a.1.2 a.2.1 a.2.2 n)) ∧
(∀ n : ℕ, Measurable (fun a : (E × E) × (E × E) × (ℕ → ℝ≥0) =>
eventTime a.1.1 a.1.2 a.2.1 a.2.2 n)) ∧
(∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0,
eventTime y xRef z₀ e 0 = 0 ∧ Monotone (eventTime y xRef z₀ e)) ∧
(∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0, ∀ n k : ℕ,
record y xRef z₀ e n = Sum.inr () →
record y xRef z₀ e (n + k) = Sum.inr ()) ∧
(∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0, ∀ n : ℕ,
∀ a : ℝ≥0 × (E × E), record y xRef z₀ e n = Sum.inl a →
H y xRef a.2 = H y xRef z₀ ∧
∀ t : ℝ≥0, (t : WithTop ℝ≥0) < τ y xRef a.2 (e n) →
H y xRef (Φ y xRef (t : ℝ) a.2) = H y xRef z₀ ∧
0 ≤ rate xRef (Φ y xRef (t : ℝ) a.2) ∧
rate xRef (Φ y xRef (t : ℝ) a.2) ≤ C y xRef z₀) ∧
(∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0,
0 ≤ C y xRef z₀ ∧
(0 < C y xRef z₀ → ∀ n : ℕ,
eventTime y xRef z₀ e n +
(Real.toNNReal ((e n : ℝ) / C y xRef z₀) : WithTop ℝ≥0) ≤
eventTime y xRef z₀ e (n + 1)) ∧
(C y xRef z₀ = 0 → ∀ n : ℕ, ∀ a : ℝ≥0 × (E × E),
record y xRef z₀ e n = Sum.inl a → 0 < e n →
record y xRef z₀ e (n + 1) = Sum.inr ())) ∧
(∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0, ∀ n : ℕ,
∀ a : ℝ≥0 × (E × E), record y xRef z₀ e n = Sum.inl a →
(e n = 0 → record y xRef z₀ e (n + 1) = Sum.inl (a.1, S xRef a.2)) ∧
(∀ b : ℝ≥0 × (E × E), 0 < e n →
record y xRef z₀ e (n + 1) = Sum.inl b → a.1 < b.1))
have hf := ActualHarmonicFlow.actual_harmonic_flow_laws hα hαβ hV hH hη hβη
have hb := ActualBounceRate.actual_bounce_rate_energy_laws hα hαβ hV hH hη hβη
have hk := ActualHazardClock.actual_integrated_hazard_clock_laws hα hαβ hV hH hη hβη
have hΦmeas : Measurable (fun a : (E × E) × ℝ × (E × E) =>
Φ a.1.1 a.1.2 a.2.1 a.2.2) := hf.2.1
have hΦzero (y xRef : E) (z : E × E) : Φ y xRef 0 z = z := hf.2.2.1 y xRef z
have hΦH (y xRef : E) (t : ℝ) (z : E × E) :
H y xRef (Φ y xRef t z) = H y xRef z := hf.2.2.2.2.2.2.2.1 y xRef t z
have hSmeas : Measurable (fun a : E × (E × E) => S a.1 a.2) := hb.1
have hSH (y xRef : E) (z : E × E) : H y xRef (S xRef z) = H y xRef z :=
hb.2.2.2.2.2.2.1 y xRef z
have hrate0 (xRef : E) (z : E × E) : 0 ≤ rate xRef z :=
(hb.2.2.2.2.2.2.2.1 xRef z).1
have hratecap (y xRef : E) (z₀ z : E × E) (hz : H y xRef z = H y xRef z₀) :
rate xRef z ≤ C y xRef z₀ :=
((hb.2.2.2.2.2.2.2.2.2 y xRef z₀).2 z hz).2.2
have hτpositive (y xRef : E) (z : E × E) (e : ℝ≥0) :
0 < e → (0 : WithTop ℝ≥0) < τ y xRef z e :=
(hk.2.2.2.2.2.1 y xRef z e).2.2.1
have hτzero (y xRef : E) (z : E × E) : τ y xRef z 0 = 0 :=
(hk.2.2.2.2.2.1 y xRef z 0).2.2.2
have hτmeas : Measurable (fun a : (E × E) × (E × E) × ℝ≥0 =>
τ a.1.1 a.1.2 a.2.1 a.2.2) := hk.2.2.2.2.2.2.1
have hC0 (y xRef : E) (z : E × E) : 0 ≤ C y xRef z :=
(hk.2.2.2.2.2.2.2.2.1 y xRef z).1
have hwait (y xRef : E) (z : E × E) (e : ℝ≥0) :
(0 < C y xRef z →
(Real.toNNReal ((e : ℝ) / C y xRef z) : WithTop ℝ≥0) ≤ τ y xRef z e) ∧
(C y xRef z = 0 → 0 < e → τ y xRef z e = ⊤) :=
hk.2.2.2.2.2.2.2.2.2 y xRef z e
have hfiniteval (q : ℝ≥0) : (q : WithTop ℝ≥0).untopD 0 = q := rfl
have hzeroval : (0 : WithTop ℝ≥0).untopD 0 = 0 := rfl
have hrec0 (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) :
record y xRef z₀ e 0 = Sum.inl (0, z₀) := rfl
have hrecstep (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) (n : ℕ) :
record y xRef z₀ e (n + 1) = next y xRef (e n) (record y xRef z₀ e n) := rfl
have hbranches (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) (n : ℕ)
(a : ℝ≥0 × (E × E)) (ha : record y xRef z₀ e n = Sum.inl a) :
(record y xRef z₀ e (n + 1) = Sum.inr () ↔ τ y xRef a.2 (e n) = ⊤) ∧
(τ y xRef a.2 (e n) ≠ ⊤ → record y xRef z₀ e (n + 1) =
Sum.inl (a.1 + (τ y xRef a.2 (e n)).untopD 0,
S xRef (Φ y xRef (((τ y xRef a.2 (e n)).untopD 0 : ℝ≥0) : ℝ) a.2))) := by
rw [hrecstep, ha]
dsimp only [next]
split_ifs with ht <;> simp [ht]
have hnextmeas : Measurable
(fun a : (E × E) × ℝ≥0 × ((ℝ≥0 × (E × E)) ⊕ Unit) =>
next a.1.1 a.1.2 a.2.1 a.2.2) := by
let g : ((E × E) × ℝ≥0) × (ℝ≥0 × (E × E)) →
((ℝ≥0 × (E × E)) ⊕ Unit) := fun a =>
if τ a.1.1.1 a.1.1.2 a.2.2 a.1.2 = ⊤ then Sum.inr () else
Sum.inl (a.2.1 + (τ a.1.1.1 a.1.1.2 a.2.2 a.1.2).untopD 0,
S a.1.1.2 (Φ a.1.1.1 a.1.1.2
(((τ a.1.1.1 a.1.1.2 a.2.2 a.1.2).untopD 0 : ℝ≥0) : ℝ) a.2.2))
have hparams : Measurable
(fun a : ((E × E) × ℝ≥0) × (ℝ≥0 × (E × E)) =>
(a.1.1, a.2.2, a.1.2)) :=
measurable_fst.fst.prodMk (measurable_snd.snd.prodMk measurable_fst.snd)
have ht0 := hτmeas.comp hparams
have ht : Measurable (fun a : ((E × E) × ℝ≥0) × (ℝ≥0 × (E × E)) =>
τ a.1.1.1 a.1.1.2 a.2.2 a.1.2) := ht0
have hq := ht.untopD (0 : ℝ≥0)
have hp := hΦmeas.comp (measurable_fst.fst.prodMk
((measurable_coe_nnreal_real.comp hq).prodMk measurable_snd.snd))
have hs := hSmeas.comp (measurable_fst.fst.snd.prodMk hp)
have hg : Measurable g := measurable_const.ite
(measurableSet_eq_fun ht measurable_const)
(measurable_inl.comp ((measurable_snd.fst.add hq).prodMk hs))
have hsum := hg.sumElim
(show Measurable (fun _ : ((E × E) × ℝ≥0) × Unit =>
(Sum.inr () : (ℝ≥0 × (E × E)) ⊕ Unit)) from measurable_const)
have hm := hsum.comp ((MeasurableEquiv.prodSumDistrib
((E × E) × ℝ≥0) (ℝ≥0 × (E × E)) Unit).measurable.comp
((measurable_fst.prodMk measurable_snd.fst).prodMk measurable_snd.snd))
convert hm using 1
funext a
rcases a with ⟨⟨y, xRef⟩, e, r⟩
cases r <;> rfl
have hrecordmeas (n : ℕ) : Measurable
(fun a : (E × E) × (E × E) × (ℕ → ℝ≥0) =>
record a.1.1 a.1.2 a.2.1 a.2.2 n) := by
induction n with
| zero => exact measurable_inl.comp (measurable_const.prodMk measurable_snd.fst)
| succ n ih =>
exact hnextmeas.comp (measurable_fst.prodMk
(((measurable_pi_apply n).comp measurable_snd.snd).prodMk ih))
have htimemeas (n : ℕ) : Measurable
(fun a : (E × E) × (E × E) × (ℕ → ℝ≥0) =>
eventTime a.1.1 a.1.2 a.2.1 a.2.2 n) :=
((WithTop.measurable_coe.comp measurable_fst).sumElim measurable_const).comp
(hrecordmeas n)
have henergy (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) (n : ℕ)
(a : ℝ≥0 × (E × E)) (ha : record y xRef z₀ e n = Sum.inl a) :
H y xRef a.2 = H y xRef z₀ := by
induction n generalizing a with
| zero =>
have heq : (0, z₀) = a := Sum.inl.inj ha
subst a
rfl
| succ n ih =>
rw [hrecstep] at ha
cases hr : record y xRef z₀ e n with
| inr u => simp [hr, next] at ha
| inl b =>
rw [hr] at ha
dsimp only [next] at ha
by_cases ht : τ y xRef b.2 (e n) = ⊤
· simp only [if_pos ht] at ha
cases ha
· rw [if_neg ht] at ha
have heq := Sum.inl.inj ha
rw [← heq]
exact (hSH y xRef _).trans ((hΦH y xRef _ _).trans (ih b hr))
have hmono (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) :
Monotone (eventTime y xRef z₀ e) := by
apply monotone_nat_of_le_succ
intro n
dsimp only [eventTime]
rw [hrecstep]
cases hr : record y xRef z₀ e n with
| inr u => simp [next]
| inl a =>
dsimp only [next]
split_ifs with ht
· exact le_top
· exact WithTop.coe_le_coe.mpr (le_add_of_nonneg_right zero_le)
have hstopped (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) (n k : ℕ)
(hn : record y xRef z₀ e n = Sum.inr ()) :
record y xRef z₀ e (n + k) = Sum.inr () := by
induction k with
| zero => simpa using hn
| succ k ih => simpa only [Nat.add_succ, hrecstep, ih, next]
have harcs (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) (n : ℕ)
(a : ℝ≥0 × (E × E)) (ha : record y xRef z₀ e n = Sum.inl a) :
H y xRef a.2 = H y xRef z₀ ∧
∀ t : ℝ≥0, (t : WithTop ℝ≥0) < τ y xRef a.2 (e n) →
H y xRef (Φ y xRef (t : ℝ) a.2) = H y xRef z₀ ∧
0 ≤ rate xRef (Φ y xRef (t : ℝ) a.2) ∧
rate xRef (Φ y xRef (t : ℝ) a.2) ≤ C y xRef z₀ := by
have hEa := henergy y xRef z₀ e n a ha
refine ⟨hEa, fun t _ => ?_⟩
have hEt := (hΦH y xRef t a.2).trans hEa
exact ⟨hEt, hrate0 xRef _, hratecap y xRef z₀ _ hEt⟩
have hcap_eq (y xRef : E) (z₀ z : E × E) (hz : H y xRef z = H y xRef z₀) :
C y xRef z = C y xRef z₀ := by simp only [C, hz]
have hincrement (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0)
(hC : 0 < C y xRef z₀) (n : ℕ) :
eventTime y xRef z₀ e n +
(Real.toNNReal ((e n : ℝ) / C y xRef z₀) : WithTop ℝ≥0) ≤
eventTime y xRef z₀ e (n + 1) := by
cases hr : record y xRef z₀ e n with
| inr u =>
dsimp only [eventTime]
rw [hrecstep, hr]
change (⊤ : WithTop ℝ≥0) + _ ≤ ⊤
exact le_top
| inl a =>
have hCa := hcap_eq y xRef z₀ a.2 (henergy y xRef z₀ e n a hr)
have hw := (hwait y xRef a.2 (e n)).1 (by simpa only [hCa] using hC)
rw [hCa] at hw
dsimp only [eventTime]
rw [hrecstep, hr]
dsimp only [next]
split_ifs with ht
· exact le_top
· have hq : (((τ y xRef a.2 (e n)).untopD 0 : ℝ≥0) : WithTop ℝ≥0) =
τ y xRef a.2 (e n) := by
induction hτ : τ y xRef a.2 (e n) using WithTop.recTopCoe with
| top => exact False.elim (ht hτ)
| coe q => exact congrArg (fun q : ℝ≥0 => (q : WithTop ℝ≥0)) (hfiniteval q)
change (a.1 : WithTop ℝ≥0) + _ ≤
((a.1 + (τ y xRef a.2 (e n)).untopD 0 : ℝ≥0) : WithTop ℝ≥0)
rw [WithTop.coe_add, hq]
exact add_le_add le_rfl hw
have hzerocap (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0)
(hC : C y xRef z₀ = 0) (n : ℕ) (a : ℝ≥0 × (E × E))
(ha : record y xRef z₀ e n = Sum.inl a) (he : 0 < e n) :
record y xRef z₀ e (n + 1) = Sum.inr () := by
apply (hbranches y xRef z₀ e n a ha).1.mpr
apply (hwait y xRef a.2 (e n)).2 _ he
exact (hcap_eq y xRef z₀ a.2 (henergy y xRef z₀ e n a ha)).trans hC
have hzeroevent (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) (n : ℕ)
(a : ℝ≥0 × (E × E)) (ha : record y xRef z₀ e n = Sum.inl a)
(he : e n = 0) :
record y xRef z₀ e (n + 1) = Sum.inl (a.1, S xRef a.2) := by
rw [hrecstep, ha]
simp only [next, he, hτzero, WithTop.zero_ne_top, ↓reduceIte,
hzeroval, add_zero, NNReal.coe_zero, hΦzero]
have hstrictevent (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) (n : ℕ)
(a : ℝ≥0 × (E × E)) (ha : record y xRef z₀ e n = Sum.inl a)
(b : ℝ≥0 × (E × E)) (he : 0 < e n)
(hb : record y xRef z₀ e (n + 1) = Sum.inl b) : a.1 < b.1 := by
have ht : τ y xRef a.2 (e n) ≠ ⊤ := by
intro ht
have hs := (hbranches y xRef z₀ e n a ha).1.mpr ht
rw [hb] at hs
cases hs
have hq : 0 < (τ y xRef a.2 (e n)).untopD 0 := by
have hp := hτpositive y xRef a.2 (e n) he
induction hτ : τ y xRef a.2 (e n) using WithTop.recTopCoe with
| top => exact False.elim (ht hτ)
| coe q => simpa only [hτ, hfiniteval, ← WithTop.coe_zero,
WithTop.coe_lt_coe] using hp
have hupdate := (hbranches y xRef z₀ e n a ha).2 ht
rw [hb] at hupdate
have heq := Sum.inl.inj hupdate
have hbtime := congrArg Prod.fst heq
rw [hbtime]
exact lt_add_of_pos_right _ hq
exact ⟨hrec0, fun y xRef z₀ e n =>
⟨hrecstep y xRef z₀ e n, hbranches y xRef z₀ e n⟩,
hnextmeas, hrecordmeas, htimemeas,
fun y xRef z₀ e => ⟨rfl, hmono y xRef z₀ e⟩, hstopped, harcs,
fun y xRef z₀ e => ⟨hC0 y xRef z₀, hincrement y xRef z₀ e,
hzerocap y xRef z₀ e⟩,
fun y xRef z₀ e n a ha => ⟨hzeroevent y xRef z₀ e n a ha,
hstrictevent y xRef z₀ e n a ha⟩⟩
end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteJumpRecursion