AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalEnergyLocalizer

- Times in `[0,T]` at which completed energy equals a prescribed level.

def energyLevelSet
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (level : ℝ) (omega : Omega) : Set ℝ≥0 :=
  {t | t ∈ Icc (0 : ℝ≥0) T ∧ completedEnergy hUsual eta t omega = level}

/-- An energy level set is closed. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalEnergyLocalizer.lean:30published source at 7bcd37294df1

- An energy level set is closed.

theorem isClosed_energyLevelSet
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (level : ℝ) (omega : Omega) :
    IsClosed (energyLevelSet hUsual eta level omega) := by
  have heq : IsClosed
      {t | completedEnergy hUsual eta t omega = level} :=
    isClosed_eq (continuous_completedEnergy hUsual eta omega) continuous_const
  change IsClosed (Icc (0 : ℝ≥0) T ∩
    {t | completedEnergy hUsual eta t omega = level})
  exact isClosed_Icc.inter heq

/-- First equality-level time, or `T` if the level is not reached. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalEnergyLocalizer.lean:37published source at 7bcd37294df1

- First equality-level time, or `T` if the level is not reached.

noncomputable def canonicalEnergyLocalizer
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (level : ℝ) (omega : Omega) : ℝ≥0 := by
  classical
  exact if h : (energyLevelSet hUsual eta level omega).Nonempty then
    sInf (energyLevelSet hUsual eta level omega)
  else T

/-- If the level set is nonempty, the canonical localizer belongs to it. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalEnergyLocalizer.lean:50published source at 7bcd37294df1

- If the level set is nonempty, the canonical localizer belongs to it.

theorem canonicalEnergyLocalizer_mem
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (level : ℝ) (omega : Omega)
    (hne : (energyLevelSet hUsual eta level omega).Nonempty) :
    canonicalEnergyLocalizer hUsual eta level omega ∈
      energyLevelSet hUsual eta level omega := by
  classical
  rw [canonicalEnergyLocalizer, dif_pos hne]
  exact (isClosed_energyLevelSet hUsual eta level omega).csInf_mem hne
    ⟨0, fun x _ => zero_le⟩

/-- The canonical localizer is no later than any member of its level set. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalEnergyLocalizer.lean:60published source at 7bcd37294df1

- The canonical localizer is no later than any member of its level set.

theorem canonicalEnergyLocalizer_le_of_mem
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (level : ℝ) (omega : Omega) {s : ℝ≥0}
    (hs : s ∈ energyLevelSet hUsual eta level omega) :
    canonicalEnergyLocalizer hUsual eta level omega ≤ s := by
  classical
  have hne : (energyLevelSet hUsual eta level omega).Nonempty := ⟨s, hs⟩
  rw [canonicalEnergyLocalizer, dif_pos hne]
  exact csInf_le ⟨0, fun y _ => zero_le⟩ hs

/-- Every canonical localizer is capped by the terminal horizon. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalEnergyLocalizer.lean:73published source at 7bcd37294df1

- Every canonical localizer is capped by the terminal horizon.

theorem canonicalEnergyLocalizer_le_terminal
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (level : ℝ) (omega : Omega) :
    canonicalEnergyLocalizer hUsual eta level omega ≤ T := by
  classical
  by_cases hne : (energyLevelSet hUsual eta level omega).Nonempty
  · exact (canonicalEnergyLocalizer_mem hUsual eta level omega hne).1.2
  · rw [canonicalEnergyLocalizer, dif_neg hne]

/-- If completed energy at time `t` dominates a nonnegative level, continuity
produces an equality-level time no later than `t`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalEnergyLocalizer.lean:85published source at 7bcd37294df1

- If completed energy at time `t` dominates a nonnegative level, continuity produces an equality-level time no later than `t`.

theorem exists_level_time_of_le
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    {level : ℝ} (hlevel : 0 ≤ level) {t : ℝ≥0} (_htT : t ≤ T)
    (hcross : level ≤ completedEnergy hUsual eta t omega) :
    ∃ s ∈ Icc (0 : ℝ≥0) t,
      completedEnergy hUsual eta s omega = level := by
  have hmem : level ∈ Icc
      (completedEnergy hUsual eta 0 omega)
      (completedEnergy hUsual eta t omega) := by
    constructor
    · simpa only [completedEnergy_zero] using hlevel
    · exact hcross
  have himage :=
    (intermediate_value_Icc (zero_le : (0 : ℝ≥0) ≤ t)
      (continuous_completedEnergy hUsual eta omega).continuousOn) hmem
  rcases himage with ⟨s, hs, hvalue⟩
  exact ⟨s, hs, hvalue⟩

/-- Fixed-time characterization of the canonical localizer. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalEnergyLocalizer.lean:97published source at 7bcd37294df1

- Fixed-time characterization of the canonical localizer.

theorem canonicalEnergyLocalizer_le_iff
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    {level : ℝ} (hlevel : 0 ≤ level) (omega : Omega) (t : ℝ≥0) :
    canonicalEnergyLocalizer hUsual eta level omega ≤ t ↔
      T ≤ t ∨ level ≤ completedEnergy hUsual eta t omega := by
  classical
  constructor
  · intro hstop
    by_cases hTt : T ≤ t
    · exact Or.inl hTt
    · right
      have hne : (energyLevelSet hUsual eta level omega).Nonempty := by
        by_contra hempty
        have hterminal : canonicalEnergyLocalizer hUsual eta level omega = T := by
          rw [canonicalEnergyLocalizer, dif_neg hempty]
        exact hTt (hterminal ▸ hstop)
      have hmem := canonicalEnergyLocalizer_mem hUsual eta level omega hne
      have hmono := monotone_completedEnergy hUsual eta omega hstop
      calc
        level = completedEnergy hUsual eta
            (canonicalEnergyLocalizer hUsual eta level omega) omega := hmem.2.symm
        _ ≤ completedEnergy hUsual eta t omega := hmono
  · rintro (hTt | hcross)
    · exact (canonicalEnergyLocalizer_le_terminal hUsual eta level omega).trans hTt
    · by_cases htT : t ≤ T
      · rcases exists_level_time_of_le hUsual eta hlevel htT hcross with
          ⟨s, hs, hvalue⟩
        have hmem : s ∈ energyLevelSet hUsual eta level omega :=
          ⟨⟨hs.1, hs.2.trans htT⟩, hvalue⟩
        exact (canonicalEnergyLocalizer_le_of_mem hUsual eta level omega hmem).trans hs.2
      · exact (canonicalEnergyLocalizer_le_terminal hUsual eta level omega).trans
          (lt_of_not_ge htT).le

/-- Canonical-localizer events are measurable at the observation time. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalEnergyLocalizer.lean:117published source at 7bcd37294df1

- Canonical-localizer events are measurable at the observation time.

theorem measurableSet_canonicalEnergyLocalizer_le
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    {level : ℝ} (hlevel : 0 ≤ level) (t : ℝ≥0) :
    MeasurableSet[filtration t]
      {omega | canonicalEnergyLocalizer hUsual eta level omega ≤ t} := by
  by_cases hTt : T ≤ t
  · have heq :
        {omega | canonicalEnergyLocalizer hUsual eta level omega ≤ t} = Set.univ := by
      ext omega
      simp only [Set.mem_ofPred_eq, Set.mem_univ, iff_true]
      exact (canonicalEnergyLocalizer_le_terminal hUsual eta level omega).trans hTt
    rw [heq]
    exact MeasurableSet.univ
  · have heq :
        {omega | canonicalEnergyLocalizer hUsual eta level omega ≤ t} =
          {omega | level ≤ completedEnergy hUsual eta t omega} := by
      ext omega
      rw [Set.mem_ofPred_eq, Set.mem_ofPred_eq,
        canonicalEnergyLocalizer_le_iff hUsual eta hlevel omega t]
      simp only [hTt, false_or]
    rw [heq]
    exact measurableSet_completedEnergy_ge hUsual eta level t

/-- On a reached level, completed energy at the canonical localizer equals the
level exactly. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalEnergyLocalizer.lean:152published source at 7bcd37294df1

- On a reached level, completed energy at the canonical localizer equals the level exactly.

theorem completedEnergy_at_canonical_eq_of_nonempty
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (level : ℝ) (omega : Omega)
    (hne : (energyLevelSet hUsual eta level omega).Nonempty) :
    completedEnergy hUsual eta
      (canonicalEnergyLocalizer hUsual eta level omega) omega = level :=
  (canonicalEnergyLocalizer_mem hUsual eta level omega hne).2

/-- Whether or not the level is reached before `T`, stopped completed energy is
bounded by the requested nonnegative level. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalEnergyLocalizer.lean:178published source at 7bcd37294df1

- Whether or not the level is reached before `T`, stopped completed energy is bounded by the requested nonnegative level.

theorem completedEnergy_at_canonical_le
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    {level : ℝ} (hlevel : 0 ≤ level) (omega : Omega) :
    completedEnergy hUsual eta
      (canonicalEnergyLocalizer hUsual eta level omega) omega ≤ level := by
  classical
  by_cases hne : (energyLevelSet hUsual eta level omega).Nonempty
  · rw [completedEnergy_at_canonical_eq_of_nonempty hUsual eta level omega hne]
  · have hstop : canonicalEnergyLocalizer hUsual eta level omega = T := by
      rw [canonicalEnergyLocalizer, dif_neg hne]
    rw [hstop]
    by_contra hnot
    have hcross : level ≤ completedEnergy hUsual eta T omega :=
      (lt_of_not_ge hnot).le
    rcases exists_level_time_of_le hUsual eta hlevel le_rfl hcross with
      ⟨s, hs, hvalue⟩
    apply hne
    exact ⟨s, ⟨hs, hvalue⟩⟩

/-- Higher energy levels are reached no earlier than lower levels. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalEnergyLocalizer.lean:189published source at 7bcd37294df1

- Higher energy levels are reached no earlier than lower levels.

theorem canonicalEnergyLocalizer_mono_level
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    {c d : ℝ} (hc : 0 ≤ c) (hcd : c ≤ d) (omega : Omega) :
    canonicalEnergyLocalizer hUsual eta c omega ≤
      canonicalEnergyLocalizer hUsual eta d omega := by
  classical
  by_cases hne : (energyLevelSet hUsual eta d omega).Nonempty
  · have hdmem := canonicalEnergyLocalizer_mem hUsual eta d omega hne
    have hcross : c ≤ completedEnergy hUsual eta
        (canonicalEnergyLocalizer hUsual eta d omega) omega := by
      rw [hdmem.2]
      exact hcd
    rcases exists_level_time_of_le hUsual eta hc hdmem.1.2 hcross with
      ⟨s, hs, hvalue⟩
    have hcmem : s ∈ energyLevelSet hUsual eta c omega :=
      ⟨⟨hs.1, hs.2.trans hdmem.1.2⟩, hvalue⟩
    exact (canonicalEnergyLocalizer_le_of_mem hUsual eta c omega hcmem).trans hs.2
  · have hd : canonicalEnergyLocalizer hUsual eta d omega = T := by
      rw [canonicalEnergyLocalizer, dif_neg hne]
    rw [hd]
    exact canonicalEnergyLocalizer_le_terminal hUsual eta c omega

/-- Chewi's canonical localizer uses the positive integer level `n+1`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalEnergyLocalizer.lean:210published source at 7bcd37294df1

- Chewi's canonical localizer uses the positive integer level `n+1`.

noncomputable def canonicalLocalizingTime
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (n : ℕ) (omega : Omega) : ℝ≥0 :=
  canonicalEnergyLocalizer hUsual eta (n + 1 : ℝ) omega

/-- Canonical localizing times increase with `n`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalEnergyLocalizer.lean:234published source at 7bcd37294df1

- Canonical localizing times increase with `n`.

theorem canonicalLocalizingTime_mono
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (omega : Omega) :
    Monotone (fun n => canonicalLocalizingTime hUsual eta n omega) := by
  intro n k hnk
  apply canonicalEnergyLocalizer_mono_level hUsual eta (by positivity)
  exact_mod_cast Nat.succ_le_succ hnk

/-- Every path is eventually left unstopped: once the integer level exceeds
terminal energy, the localizer equals `T`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalEnergyLocalizer.lean:241published source at 7bcd37294df1

- Every path is eventually left unstopped: once the integer level exceeds terminal energy, the localizer equals `T`.

theorem canonicalLocalizingTime_eventually_eq_terminal
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (omega : Omega) :
    ∀ᶠ n in Filter.atTop,
      canonicalLocalizingTime hUsual eta n omega = T := by
  classical
  obtain ⟨N, hN⟩ := exists_nat_gt
    (completedEnergy hUsual eta T omega)
  filter_upwards [Filter.eventually_ge_atTop N] with n hn
  have hlevel : completedEnergy hUsual eta T omega < (n + 1 : ℝ) := by
    have hNn : (N : ℝ) ≤ n := by exact_mod_cast hn
    exact hN.trans_le (hNn.trans (by norm_num))
  have hempty :
      ¬(energyLevelSet hUsual eta (n + 1 : ℝ) omega).Nonempty := by
    rintro ⟨t, ⟨_ht0, htT⟩, hvalue⟩
    have hmono : completedEnergy hUsual eta t omega ≤
        completedEnergy hUsual eta T omega :=
      monotone_completedEnergy hUsual eta omega htT
    have hlevel_le_terminal : (n + 1 : ℝ) ≤
        completedEnergy hUsual eta T omega := by
      calc
        (n + 1 : ℝ) = completedEnergy hUsual eta t omega := hvalue.symm
        _ ≤ completedEnergy hUsual eta T omega := hmono
    exact (not_le_of_gt hlevel) hlevel_le_terminal
  rw [canonicalLocalizingTime, canonicalEnergyLocalizer, dif_neg hempty]

/-- Canonical localizing times converge pointwise to the terminal horizon. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalEnergyLocalizer.lean:252published source at 7bcd37294df1

- Canonical localizing times converge pointwise to the terminal horizon.

theorem tendsto_canonicalLocalizingTime
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (omega : Omega) :
    Filter.Tendsto (fun n => canonicalLocalizingTime hUsual eta n omega)
      Filter.atTop (𝓝 T) := by
  exact (Filter.tendsto_congr'
    (canonicalLocalizingTime_eventually_eq_terminal hUsual eta omega)).2
    tendsto_const_nhds

/-- The stopped completed energy at the `n`-th localizer is bounded by `n+1`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalEnergyLocalizer.lean:280published source at 7bcd37294df1Open detailed card

- The stopped completed energy at the `n`-th localizer is bounded by `n+1`.

theorem completedEnergy_at_canonicalLocalizingTime_le
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (n : ℕ) (omega : Omega) :
    completedEnergy hUsual eta
      (canonicalLocalizingTime hUsual eta n omega) omega ≤ (n + 1 : ℝ) := by
  exact completedEnergy_at_canonical_le hUsual eta (by positivity) omega

end CanonicalEnergyLocalizer
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalEnergyLocalizer.lean:291published source at 7bcd37294df1Open detailed card