AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.DyadicElementaryRefinement

- Number of fine cells inside one coarse cell.

def refinementFactor (level targetLevel : ℕ) : ℕ :=
  2 ^ (targetLevel - level)

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:29published source at 7bcd37294df1

No declaration docstring.

theorem refinementFactor_pos (level targetLevel : ℕ) :
    0 < refinementFactor level targetLevel := by
  simp [refinementFactor]

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:32published source at 7bcd37294df1

No declaration docstring.

theorem pow_mul_refinementFactor {level targetLevel : ℕ}
    (hle : level ≤ targetLevel) :
    2 ^ level * refinementFactor level targetLevel = 2 ^ targetLevel := by
  rw [refinementFactor, mul_comm]
  exact Nat.pow_sub_mul_pow 2 hle

/-- Fine-cell index viewed in its containing coarse cell. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:36published source at 7bcd37294df1

- Fine-cell index viewed in its containing coarse cell.

def coarseCell {level targetLevel : ℕ} (hle : level ≤ targetLevel)
    (j : Fin (2 ^ targetLevel)) : Fin (2 ^ level) :=
  ⟨j.val / refinementFactor level targetLevel,
    (Nat.div_lt_iff_lt_mul (refinementFactor_pos level targetLevel)).2 (by
      rw [pow_mul_refinementFactor hle]
      exact j.isLt)⟩

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:43published source at 7bcd37294df1

No declaration docstring.

@[simp] theorem coarseCell_val {level targetLevel : ℕ}
    (hle : level ≤ targetLevel) (j : Fin (2 ^ targetLevel)) :
    (coarseCell hle j).val = j.val / refinementFactor level targetLevel :=
  rfl

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

No declaration docstring.

theorem coarseCell_block_left {level targetLevel : ℕ}
    (hle : level ≤ targetLevel) (j : Fin (2 ^ targetLevel)) :
    (coarseCell hle j).val * refinementFactor level targetLevel ≤ j.val := by
  exact Nat.div_mul_le_self _ _

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:55published source at 7bcd37294df1

No declaration docstring.

theorem coarseCell_block_right {level targetLevel : ℕ}
    (hle : level ≤ targetLevel) (j : Fin (2 ^ targetLevel)) :
    j.val < ((coarseCell hle j).val + 1) * refinementFactor level targetLevel := by
  simpa [mul_comm] using
    Nat.lt_mul_div_succ j.val (refinementFactor_pos level targetLevel)

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

No declaration docstring.

theorem dyadicMesh_coarse_eq_factor_mul {level targetLevel : ℕ}
    (hle : level ≤ targetLevel) :
    dyadicMesh T level =
      (refinementFactor level targetLevel : ℝ≥0) * dyadicMesh T targetLevel := by
  unfold dyadicMesh
  apply (div_eq_iff (by positivity : ((2 ^ level : ℕ) : ℝ≥0) ≠ 0)).2
  calc
    T = T / (2 ^ targetLevel : ℕ) * (2 ^ targetLevel : ℕ) := by
      rw [div_mul_cancel₀]
      positivity
    _ = T / (2 ^ targetLevel : ℕ) *
        ((refinementFactor level targetLevel : ℝ≥0) * (2 ^ level : ℕ)) := by
      rw [← Nat.cast_mul, Nat.mul_comm (refinementFactor level targetLevel),
        pow_mul_refinementFactor hle]
    _ = ((refinementFactor level targetLevel : ℝ≥0) *
        (T / (2 ^ targetLevel : ℕ))) * (2 ^ level : ℕ) := by
      ac_rfl

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:66published source at 7bcd37294df1

No declaration docstring.

theorem coarse_left_endpoint_le_fine_left {level targetLevel : ℕ}
    (hle : level ≤ targetLevel) (j : Fin (2 ^ targetLevel)) :
    regularGridTimes (dyadicMesh T level) (2 ^ level) (coarseCell hle j).castSucc ≤
      regularGridTimes (dyadicMesh T targetLevel) (2 ^ targetLevel) j.castSucc := by
  rw [regularGridTimes, regularGridTimes, dyadicMesh_coarse_eq_factor_mul hle]
  simp only [Fin.val_castSucc]
  rw [← mul_assoc]
  exact mul_le_mul_of_nonneg_right
    (by exact_mod_cast coarseCell_block_left hle j)
    (by positivity)

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:84published source at 7bcd37294df1

No declaration docstring.

theorem fine_right_endpoint_le_coarse_right {level targetLevel : ℕ}
    (hle : level ≤ targetLevel) (j : Fin (2 ^ targetLevel)) :
    regularGridTimes (dyadicMesh T targetLevel) (2 ^ targetLevel) j.succ ≤
      regularGridTimes (dyadicMesh T level) (2 ^ level) (coarseCell hle j).succ := by
  rw [regularGridTimes, regularGridTimes, dyadicMesh_coarse_eq_factor_mul hle]
  simp only [Fin.val_succ, Nat.cast_add, Nat.cast_one]
  rw [← mul_assoc]
  exact mul_le_mul_of_nonneg_right
    (by
      have hnat : j.val + 1 ≤
          ((coarseCell hle j).val + 1) * refinementFactor level targetLevel :=
        Nat.succ_le_iff.2 (coarseCell_block_right hle j)
      exact_mod_cast hnat)
    (by positivity)

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:95published source at 7bcd37294df1

No declaration docstring.

theorem regularDyadic_last_time (T : ℝ≥0) (level : ℕ) :
    regularGridTimes (dyadicMesh T level) (2 ^ level) (Fin.last (2 ^ level)) = T := by
  simp only [regularGridTimes, Fin.val_last, Nat.cast_pow, Nat.cast_ofNat, dyadicMesh]
  rw [mul_comm, div_mul_cancel₀]
  positivity

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:110published source at 7bcd37294df1

No declaration docstring.

theorem DyadicElementaryProcess.horizon_pos
    (eta : DyadicElementaryProcess filtration T) : 0 < T := by
  have hindex : (0 : Fin (2 ^ eta.level + 1)) < Fin.last (2 ^ eta.level) := by
    exact_mod_cast (show 0 < 2 ^ eta.level by positivity)
  have htime := eta.process.times_strictMono hindex
  rw [congrFun eta.times_eq 0,
    congrFun eta.times_eq (Fin.last (2 ^ eta.level)),
    regularDyadic_last_time] at htime
  simpa [regularGridTimes] using htime

/-- Refine a dyadic process to a finer dyadic level by repeating each coarse
coefficient across the fine cells in its block. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:116published source at 7bcd37294df1

- Refine a dyadic process to a finer dyadic level by repeating each coarse coefficient across the fine cells in its block.

noncomputable def refineDyadic
    (eta : DyadicElementaryProcess filtration T) (targetLevel : ℕ)
    (hle : eta.level ≤ targetLevel) :
    DyadicElementaryProcess filtration T where
  level := targetLevel
  process :=
    { times := regularGridTimes (dyadicMesh T targetLevel) (2 ^ targetLevel)
      times_strictMono := regularGridTimes_strictMono
        (dyadicMesh_pos (DyadicElementaryProcess.horizon_pos eta) targetLevel) _
      coeff := fun j ↦ eta.process.coeff (coarseCell hle j)
      coeff_stronglyMeasurable := fun j ↦ by
        have hcoeff := eta.process.coeff_stronglyMeasurable (coarseCell hle j)
        rw [congrFun eta.times_eq (coarseCell hle j).castSucc] at hcoeff
        exact hcoeff.mono (filtration.mono (coarse_left_endpoint_le_fine_left hle j))
      coeff_bounded := fun j ↦ eta.process.coeff_bounded (coarseCell hle j) }
  times_eq := rfl

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:128published source at 7bcd37294df1

No declaration docstring.

@[simp] theorem refineDyadic_level
    (eta : DyadicElementaryProcess filtration T) (targetLevel : ℕ)
    (hle : eta.level ≤ targetLevel) :
    (refineDyadic eta targetLevel hle).level = targetLevel :=
  rfl

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:145published source at 7bcd37294df1

No declaration docstring.

@[simp] theorem refineDyadic_times
    (eta : DyadicElementaryProcess filtration T) (targetLevel : ℕ)
    (hle : eta.level ≤ targetLevel) :
    (refineDyadic eta targetLevel hle).process.times =
      regularGridTimes (dyadicMesh T targetLevel) (2 ^ targetLevel) :=
  rfl

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:151published source at 7bcd37294df1

No declaration docstring.

@[simp] theorem refineDyadic_coeff
    (eta : DyadicElementaryProcess filtration T) (targetLevel : ℕ)
    (hle : eta.level ≤ targetLevel) (j : Fin (2 ^ targetLevel)) (omega : Omega) :
    (refineDyadic eta targetLevel hle).process.coeff j omega =
      eta.process.coeff (coarseCell hle j) omega :=
  rfl

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:158published source at 7bcd37294df1

No declaration docstring.

theorem refineDyadic_coeff_stronglyMeasurable
    (eta : DyadicElementaryProcess filtration T) (targetLevel : ℕ)
    (hle : eta.level ≤ targetLevel) (j : Fin (2 ^ targetLevel)) :
    StronglyMeasurable[filtration
      ((refineDyadic eta targetLevel hle).process.times j.castSucc)]
      ((refineDyadic eta targetLevel hle).process.coeff j) :=
  (refineDyadic eta targetLevel hle).process.coeff_stronglyMeasurable j

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:165published source at 7bcd37294df1

No declaration docstring.

theorem refineDyadic_value_eq
    (eta : DyadicElementaryProcess filtration T) (targetLevel : ℕ)
    (hle : eta.level ≤ targetLevel) (t : ℝ≥0) (omega : Omega) :
    (refineDyadic eta targetLevel hle).process.value t omega =
      eta.process.value t omega := by
  by_cases ht0 : t = 0
  · subst t
    rw [ElementaryAdaptedProcess.value_eq_zero_of_le_first _ (by
        simp [refineDyadic, regularGridTimes])]
    rw [ElementaryAdaptedProcess.value_eq_zero_of_le_first _ (by
        rw [congrFun eta.times_eq 0]
        simp [regularGridTimes])]
  · by_cases htT : t ≤ T
    · have htpos : 0 < t := pos_of_ne_zero ht0
      obtain ⟨j, hj, _⟩ := dyadic_activeCell
        (DyadicElementaryProcess.horizon_pos eta) targetLevel htpos htT
      have hcoarse :
          regularGridTimes (dyadicMesh T eta.level) (2 ^ eta.level)
              (coarseCell hle j).castSucc < t ∧
            t ≤ regularGridTimes (dyadicMesh T eta.level) (2 ^ eta.level)
              (coarseCell hle j).succ :=
        ⟨(coarse_left_endpoint_le_fine_left hle j).trans_lt hj.1,
          hj.2.trans (fine_right_endpoint_le_coarse_right hle j)⟩
      have hfine :=
        FiniteTimeGrid.ElementaryAdaptedProcess.value_eq_coeff_of_mem_cell
          (refineDyadic eta targetLevel hle).process (omega := omega) hj
      have hcoarseValue :=
        FiniteTimeGrid.ElementaryAdaptedProcess.value_eq_coeff_of_mem_cell eta.process
          (omega := omega) (by
          simpa only [eta.times_eq] using hcoarse)
      exact hfine.trans hcoarseValue.symm
    · have hTt : T < t := lt_of_not_ge htT
      rw [ElementaryAdaptedProcess.value_eq_zero_of_last_lt _ (by
        simpa [refineDyadic, regularDyadic_last_time] using hTt)]
      rw [ElementaryAdaptedProcess.value_eq_zero_of_last_lt _ (by
        rw [congrFun eta.times_eq (Fin.last (2 ^ eta.level)),
          regularDyadic_last_time]
        exact hTt)]

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:173published source at 7bcd37294df1

No declaration docstring.

theorem refineDyadic_toLp_eq [IsFiniteMeasure mu]
    (eta : DyadicElementaryProcess filtration T) (targetLevel : ℕ)
    (hle : eta.level ≤ targetLevel) :
    (refineDyadic eta targetLevel hle).toLp mu = eta.toLp mu := by
  apply Lp.ext
  simp only [DyadicElementaryProcess.toLp, ProgressiveL2Integrand.toLp]
  filter_upwards [
    (ElementaryItoEmbedding.toProgressiveL2
      (refineDyadic eta targetLevel hle).process mu T).memLp.coeFn_toLp,
    (ElementaryItoEmbedding.toProgressiveL2 eta.process mu T).memLp.coeFn_toLp]
      with z hfine hcoarse
  rw [hfine, hcoarse]
  exact refineDyadic_value_eq eta targetLevel hle z.2 z.1

/-- Product indexing of a fine grid by coarse cell and within-cell offset. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:212published source at 7bcd37294df1

- Product indexing of a fine grid by coarse cell and within-cell offset.

def refinementEquiv {level targetLevel : ℕ} (hle : level ≤ targetLevel) :
    Fin (2 ^ level) × Fin (refinementFactor level targetLevel) ≃
      Fin (2 ^ targetLevel) :=
  finProdFinEquiv.trans (finCongr (pow_mul_refinementFactor hle))

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:227published source at 7bcd37294df1

No declaration docstring.

@[simp] theorem refinementEquiv_val {level targetLevel : ℕ}
    (hle : level ≤ targetLevel)
    (i : Fin (2 ^ level)) (r : Fin (refinementFactor level targetLevel)) :
    (refinementEquiv hle (i, r)).val =
      r.val + refinementFactor level targetLevel * i.val :=
  rfl

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:232published source at 7bcd37294df1

No declaration docstring.

@[simp] theorem coarseCell_refinementEquiv {level targetLevel : ℕ}
    (hle : level ≤ targetLevel)
    (i : Fin (2 ^ level)) (r : Fin (refinementFactor level targetLevel)) :
    coarseCell hle (refinementEquiv hle (i, r)) = i := by
  apply Fin.ext
  simp only [coarseCell_val, refinementEquiv_val]
  rw [Nat.add_mul_div_left, Nat.div_eq_of_lt r.isLt, zero_add]
  exact refinementFactor_pos level targetLevel

/-- A finite block of consecutive increments telescopes. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:239published source at 7bcd37294df1

- A finite block of consecutive increments telescopes.

theorem sum_brownianIncrements_block
    (q start : ℕ) (F : ℕ → ℝ) :
    (∑ r : Fin q, (F (start + r.val + 1) - F (start + r.val))) =
      F (start + q) - F start := by
  change (∑ r : Fin q,
      (fun k : ℕ ↦ F (start + k + 1) - F (start + k)) r) = _
  calc
    _ = ∑ r ∈ Finset.range q,
        (F (start + r + 1) - F (start + r)) :=
      Fin.sum_univ_eq_sum_range
        (fun r ↦ F (start + r + 1) - F (start + r)) q
    _ = F (start + q) - F start := by
      simpa only [Nat.add_assoc, Nat.add_zero] using
        (Finset.sum_range_sub (fun r ↦ F (start + r)) q)

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:249published source at 7bcd37294df1

No declaration docstring.

theorem fine_block_left_endpoint {level targetLevel : ℕ}
    (hle : level ≤ targetLevel) (i : Fin (2 ^ level)) :
    ((refinementFactor level targetLevel * i.val : ℕ) : ℝ≥0) *
        dyadicMesh T targetLevel =
      (i.val : ℝ≥0) * dyadicMesh T level := by
  rw [dyadicMesh_coarse_eq_factor_mul hle]
  simp only [Nat.cast_mul]
  ac_rfl

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:264published source at 7bcd37294df1

No declaration docstring.

theorem fine_block_right_endpoint {level targetLevel : ℕ}
    (hle : level ≤ targetLevel) (i : Fin (2 ^ level)) :
    ((refinementFactor level targetLevel * i.val +
        refinementFactor level targetLevel : ℕ) : ℝ≥0) *
        dyadicMesh T targetLevel =
      ((i.val + 1 : ℕ) : ℝ≥0) * dyadicMesh T level := by
  rw [dyadicMesh_coarse_eq_factor_mul hle]
  simp only [Nat.cast_add, Nat.cast_one, Nat.cast_mul]
  ring

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:273published source at 7bcd37294df1

No declaration docstring.

theorem refineDyadic_elementaryItoIntegral_eq
    (eta : DyadicElementaryProcess filtration T) (targetLevel : ℕ)
    (hle : eta.level ≤ targetLevel)
    (B : ℝ≥0 → Omega → ℝ) (S : ℝ≥0) (omega : Omega) :
    elementaryItoIntegral (refineDyadic eta targetLevel hle).process B S omega =
      elementaryItoIntegral eta.process B S omega := by
  change (∑ j : Fin (2 ^ targetLevel), eta.process.coeff (coarseCell hle j) omega *
      (B (min (regularGridTimes (dyadicMesh T targetLevel) (2 ^ targetLevel) j.succ) S) omega -
        B (min (regularGridTimes (dyadicMesh T targetLevel) (2 ^ targetLevel) j.castSucc) S)
          omega)) =
    ∑ i : Fin (2 ^ eta.level), eta.process.coeff i omega *
      (B (min (eta.process.times i.succ) S) omega -
        B (min (eta.process.times i.castSucc) S) omega)
  rw [← (refinementEquiv hle).sum_comp]
  rw [Fintype.sum_prod_type]
  simp only [coarseCell_refinementEquiv, regularGridTimes, refinementEquiv_val,
    Fin.val_succ, Fin.val_castSucc]
  simp_rw [congrFun eta.times_eq]
  apply Finset.sum_congr rfl
  intro i _
  rw [← Finset.mul_sum]
  congr 1
  have htel := sum_brownianIncrements_block
    (refinementFactor eta.level targetLevel)
    (refinementFactor eta.level targetLevel * i.val)
    (fun k ↦ B (min ((k : ℝ≥0) * dyadicMesh T targetLevel) S) omega)
  have hright :
      ((refinementFactor eta.level targetLevel +
          refinementFactor eta.level targetLevel * i.val : ℕ) : ℝ≥0) *
          dyadicMesh T targetLevel =
        ((i.val + 1 : ℕ) : ℝ≥0) * dyadicMesh T eta.level := by
    rw [Nat.add_comm]
    exact fine_block_right_endpoint hle i
  have hright' :
      ((refinementFactor eta.level targetLevel : ℝ≥0) +
          ((refinementFactor eta.level targetLevel * i.val : ℕ) : ℝ≥0)) *
          dyadicMesh T targetLevel =
        ((i.val : ℝ≥0) + 1) * dyadicMesh T eta.level := by
    simpa only [Nat.cast_add, Nat.cast_one] using hright
  simpa only [regularGridTimes, Fin.val_succ, Fin.val_castSucc,
    Nat.cast_add, Nat.cast_one, Nat.add_assoc, Nat.add_comm,
    Nat.add_left_comm, fine_block_left_endpoint hle i, hright'] using htel

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:283published source at 7bcd37294df1

No declaration docstring.

theorem refineDyadic_terminalToLp_eq
    (eta : DyadicElementaryProcess filtration T) (targetLevel : ℕ)
    (hle : eta.level ≤ targetLevel)
    (hB : IsBrownianMotionWithFiltration B filtration mu) (S : ℝ≥0) :
    elementaryItoTerminalToLp (refineDyadic eta targetLevel hle).process hB S =
      elementaryItoTerminalToLp eta.process hB S := by
  apply Lp.ext
  simp only [elementaryItoTerminalToLp]
  filter_upwards [
    (elementaryItoIntegral_memLp_two
      (refineDyadic eta targetLevel hle).process hB S).coeFn_toLp,
    (elementaryItoIntegral_memLp_two eta.process hB S).coeFn_toLp]
      with omega hfine hcoarse
  rw [hfine, hcoarse]
  exact refineDyadic_elementaryItoIntegral_eq eta targetLevel hle B S omega

/-- Terminal stochastic integral represented in `L2(mu)`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:326published source at 7bcd37294df1

- Terminal stochastic integral represented in `L2(mu)`.

noncomputable def terminalToLp
    (eta : DyadicElementaryProcess filtration T)
    (hB : IsBrownianMotionWithFiltration B filtration mu) : Lp ℝ 2 mu :=
  elementaryItoTerminalToLp eta.process hB T

/-- Product-space representative, with finiteness supplied by the Brownian
probability contract rather than exposed as an extra theorem parameter. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:343published source at 7bcd37294df1

- Product-space representative, with finiteness supplied by the Brownian probability contract rather than exposed as an extra theorem parameter.

noncomputable def processToLp
    (eta : DyadicElementaryProcess filtration T)
    (hB : IsBrownianMotionWithFiltration B filtration mu) :
    Lp ℝ 2 (processTimeMeasure mu T) := by
  let _ : IsProbabilityMeasure mu := hB.isProbabilityMeasure
  exact eta.toLp mu

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:350published source at 7bcd37294df1

No declaration docstring.

theorem elementaryProcessToLp_eq_processToLp
    (eta : DyadicElementaryProcess filtration T)
    (hB : IsBrownianMotionWithFiltration B filtration mu) :
    elementaryProcessToLp eta.process hB T = processToLp eta hB := by
  let _ : IsProbabilityMeasure mu := hB.isProbabilityMeasure
  rfl

/-- Least dyadic level containing the grids of both processes. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:357published source at 7bcd37294df1

- Least dyadic level containing the grids of both processes.

def commonDyadicLevel
    (eta xi : DyadicElementaryProcess filtration T) : ℕ :=
  max eta.level xi.level

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:365published source at 7bcd37294df1

No declaration docstring.

noncomputable def commonRefinementLeft
    (eta xi : DyadicElementaryProcess filtration T) :
    DyadicElementaryProcess filtration T :=
  refineDyadic eta (commonDyadicLevel eta xi) (le_max_left _ _)

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:369published source at 7bcd37294df1

No declaration docstring.

noncomputable def commonRefinementRight
    (eta xi : DyadicElementaryProcess filtration T) :
    DyadicElementaryProcess filtration T :=
  refineDyadic xi (commonDyadicLevel eta xi) (le_max_right _ _)

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:374published source at 7bcd37294df1

No declaration docstring.

theorem commonRefinement_times_eq
    (eta xi : DyadicElementaryProcess filtration T) :
    (commonRefinementLeft eta xi).process.times =
      (commonRefinementRight eta xi).process.times := by
  rfl

/-- Left common refinement with the shared cell count exposed in its type. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:379published source at 7bcd37294df1

- Left common refinement with the shared cell count exposed in its type.

noncomputable def commonRefinementLeftProcess
    (eta xi : DyadicElementaryProcess filtration T) :
    ElementaryAdaptedProcess filtration (2 ^ commonDyadicLevel eta xi) :=
  (refineDyadic eta (commonDyadicLevel eta xi) (le_max_left _ _)).process

/-- Right common refinement with the shared cell count exposed in its type. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:386published source at 7bcd37294df1

- Right common refinement with the shared cell count exposed in its type.

noncomputable def commonRefinementRightProcess
    (eta xi : DyadicElementaryProcess filtration T) :
    ElementaryAdaptedProcess filtration (2 ^ commonDyadicLevel eta xi) :=
  (refineDyadic xi (commonDyadicLevel eta xi) (le_max_right _ _)).process

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:392published source at 7bcd37294df1

No declaration docstring.

theorem commonRefinementProcess_times_eq
    (eta xi : DyadicElementaryProcess filtration T) :
    (commonRefinementLeftProcess eta xi).times =
      (commonRefinementRightProcess eta xi).times := by
  rfl

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:397published source at 7bcd37294df1

No declaration docstring.

theorem commonRefinementLeft_toLp_eq [IsFiniteMeasure mu]
    (eta xi : DyadicElementaryProcess filtration T) :
    (commonRefinementLeft eta xi).toLp mu = eta.toLp mu :=
  refineDyadic_toLp_eq eta (commonDyadicLevel eta xi) (le_max_left _ _)

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:403published source at 7bcd37294df1

No declaration docstring.

theorem commonRefinementRight_toLp_eq [IsFiniteMeasure mu]
    (eta xi : DyadicElementaryProcess filtration T) :
    (commonRefinementRight eta xi).toLp mu = xi.toLp mu :=
  refineDyadic_toLp_eq xi (commonDyadicLevel eta xi) (le_max_right _ _)

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:408published source at 7bcd37294df1

No declaration docstring.

theorem commonRefinementLeft_processToLp_eq
    (eta xi : DyadicElementaryProcess filtration T)
    (hB : IsBrownianMotionWithFiltration B filtration mu) :
    processToLp (commonRefinementLeft eta xi) hB = processToLp eta hB := by
  let _ : IsProbabilityMeasure mu := hB.isProbabilityMeasure
  exact commonRefinementLeft_toLp_eq eta xi

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:413published source at 7bcd37294df1

No declaration docstring.

theorem commonRefinementRight_processToLp_eq
    (eta xi : DyadicElementaryProcess filtration T)
    (hB : IsBrownianMotionWithFiltration B filtration mu) :
    processToLp (commonRefinementRight eta xi) hB = processToLp xi hB := by
  let _ : IsProbabilityMeasure mu := hB.isProbabilityMeasure
  exact commonRefinementRight_toLp_eq eta xi

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:420published source at 7bcd37294df1

No declaration docstring.

theorem commonRefinementLeft_terminalToLp_eq
    (eta xi : DyadicElementaryProcess filtration T)
    (hB : IsBrownianMotionWithFiltration B filtration mu) :
    terminalToLp (commonRefinementLeft eta xi) hB = terminalToLp eta hB :=
  refineDyadic_terminalToLp_eq eta (commonDyadicLevel eta xi)
    (le_max_left _ _) hB T

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:427published source at 7bcd37294df1

No declaration docstring.

theorem commonRefinementRight_terminalToLp_eq
    (eta xi : DyadicElementaryProcess filtration T)
    (hB : IsBrownianMotionWithFiltration B filtration mu) :
    terminalToLp (commonRefinementRight eta xi) hB = terminalToLp xi hB :=
  refineDyadic_terminalToLp_eq xi (commonDyadicLevel eta xi)
    (le_max_right _ _) hB T

/-- The elementary Ito terminal map is an exact distance isometry even when
the two processes are initially represented on different dyadic grids. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:434published source at 7bcd37294df1

- The elementary Ito terminal map is an exact distance isometry even when the two processes are initially represented on different dyadic grids.

theorem norm_terminal_sub_eq_process_sub
    (eta xi : DyadicElementaryProcess filtration T)
    (hB : IsBrownianMotionWithFiltration B filtration mu) :
    ‖terminalToLp eta hB - terminalToLp xi hB‖ =
      ‖processToLp eta hB - processToLp xi hB‖ := by
  let _ : IsProbabilityMeasure mu := hB.isProbabilityMeasure
  let eta' := commonRefinementLeft eta xi
  let xi' := commonRefinementRight eta xi
  calc
    ‖terminalToLp eta hB - terminalToLp xi hB‖ =
        ‖terminalToLp eta' hB - terminalToLp xi' hB‖ := by
      rw [commonRefinementLeft_terminalToLp_eq eta xi hB,
        commonRefinementRight_terminalToLp_eq eta xi hB]
    _ = ‖elementaryProcessToLp eta'.process hB T -
        elementaryProcessToLp xi'.process hB T‖ :=
      norm_elementaryItoTerminalToLp_sub eta'.process xi'.process
        (commonRefinement_times_eq eta xi) hB T
    _ = ‖processToLp eta' hB - processToLp xi' hB‖ := by
      rw [elementaryProcessToLp_eq_processToLp eta' hB,
        elementaryProcessToLp_eq_processToLp xi' hB]
    _ = ‖processToLp eta hB - processToLp xi hB‖ := by
      rw [commonRefinementLeft_processToLp_eq eta xi hB,
        commonRefinementRight_processToLp_eq eta xi hB]

end DyadicElementaryRefinement
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean:443published source at 7bcd37294df1Open detailed card