PhaseMotion.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Motion of diagonal Fourier predictions

Bounded frequencies give explicit Lipschitz bounds for the actual characters and Hilbert-valued phase sums. Together with logarithmic energy control these give the multiplicative cell-supremum bound required by §9.

theorem OAI.LipschitzHilbert.character_motion line 27
theorem OAI.LipschitzHilbert.diagonalModulation_motion line 40

theorem OAI.LipschitzHilbert.diagonalFourierSum_motion line 66

Source documentation

Uniform frequency control bounds the motion by the total coefficient norm.

theorem diagonalFourierSum_motion (frequency : ι → κ → ℝ)
    (a : ι → EuclideanSpace ℂ κ) {L : ℝ} (hL : 0 ≤ L)
    (hfrequency : ∀ i j, |frequency i j| ≤ L) (s t : ℝ) :
    ‖diagonalFourierSum frequency a t - diagonalFourierSum frequency a s‖ ≤
      L * (∑ i, ‖a i‖) * |t - s| := by
…

theorem OAI.LipschitzHilbert.diagonal_prediction_log_motion line 80

Source documentation

The fixed positive denominator disappears from logarithmic motion.

theorem diagonal_prediction_log_motion (frequency : ι → κ → ℝ)
    (a : ι → EuclideanSpace ℂ κ) {L p denominator : ℝ}
    (hL : 0 ≤ L) (hp : 1 ≤ p) (hd : 0 < denominator)
    (hfrequency : ∀ i j, |frequency i j| ≤ L) (s t : ℝ) :
    |Real.log (energyRatio p denominator (diagonalFourierSum frequency a t)) -
      Real.log (energyRatio p denominator (diagonalFourierSum frequency a s))| ≤
        p * L * (∑ i, ‖a i‖) * |t - s| := by
…

Mentions: OAI.LipschitzHilbert.energyRatio

theorem OAI.LipschitzHilbert.diagonal_prediction_cell_sup line 97

Source documentation

The actual Fourier prediction, maximized on a cell of bounded diameter, differs from its value by the stated exponential factor.

theorem diagonal_prediction_cell_sup (frequency : ι → κ → ℝ)
    (a : ι → EuclideanSpace ℂ κ) (I : Set ℝ) {s L p denominator H : ℝ}
    (hs : s ∈ I) (hL : 0 ≤ L) (hp : 1 ≤ p) (hd : 0 < denominator)
    (hfrequency : ∀ i j, |frequency i j| ≤ L)
    (hdiameter : ∀ t ∈ I, |t - s| ≤ H) :
    energyRatio p denominator (diagonalFourierSum frequency a s) ≤
      predictionCellSup (fun t => energyRatio p denominator (diagonalFourierSum frequency a t)) I ∧
    predictionCellSup (fun t => energyRatio p denominator (diagonalFourierSum frequency a t)) I ≤
      Real.exp (p * L * (∑ i, ‖a i‖) * H) *
        energyRatio p denominator (diagonalFourierSum frequency a s) := by
…

Mentions: OAI.LipschitzHilbert.energyRatio, OAI.LipschitzHilbert.predictionCellSup

theorem OAI.LipschitzHilbert.fixed_path_diagonal_log_motion line 114

Source documentation

Removing the path carrier leaves a fixed vector. Its size does not enter logarithmic motion; only the off-path Fourier coefficients contribute.

theorem fixed_path_diagonal_log_motion (frequency : ι → κ → ℝ)
    (a : ι → EuclideanSpace ℂ κ) (Y : EuclideanSpace ℂ κ)
    {L p denominator : ℝ} (hL : 0 ≤ L) (hp : 1 ≤ p) (hd : 0 < denominator)
    (hfrequency : ∀ i j, |frequency i j| ≤ L) (s t : ℝ) :
    |Real.log (energyRatio p denominator (Y + diagonalFourierSum frequency a t)) -
      Real.log (energyRatio p denominator (Y + diagonalFourierSum frequency a s))| ≤
        p * L * (∑ i, ‖a i‖) * |t - s| := by
…

Mentions: OAI.LipschitzHilbert.energyRatio

theorem OAI.LipschitzHilbert.fixed_path_diagonal_cell_sup line 132

Source documentation

The source's small-drop form of step supremum control: when the off-path coefficient mass is at most K*u, the exponent retains the factor u.

theorem fixed_path_diagonal_cell_sup (frequency : ι → κ → ℝ)
    (a : ι → EuclideanSpace ℂ κ) (Y : EuclideanSpace ℂ κ) (I : Set ℝ)
    {s L p denominator H K u : ℝ} (hs : s ∈ I)
    (hL : 0 ≤ L) (hp : 1 ≤ p) (hd : 0 < denominator) (hH : 0 ≤ H)
    (hfrequency : ∀ i j, |frequency i j| ≤ L)
    (hdiameter : ∀ t ∈ I, |t - s| ≤ H) (hmass : ∑ i, ‖a i‖ ≤ K * u) :
    energyRatio p denominator (Y + diagonalFourierSum frequency a s) ≤
      predictionCellSup (fun t => energyRatio p denominator (Y + diagonalFourierSum frequency a t)) I ∧
    predictionCellSup (fun t => energyRatio p denominator (Y + diagonalFourierSum frequency a t)) I ≤
      Real.exp ((p * L * K * H) * u) *
        energyRatio p denominator (Y + diagonalFourierSum frequency a s) := by
…

Mentions: OAI.LipschitzHilbert.energyRatio, OAI.LipschitzHilbert.predictionCellSup

theorem OAI.LipschitzHilbert.blend_log_contraction line 157

Source documentation

Blending a positive prediction with one contracts its logarithmic oscillation. This proves the blend step without differentiating the ratio.

theorem blend_log_contraction {θ x y : ℝ} (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1)
    (hx : 0 < x) (hy : 0 < y) :
    |Real.log ((1 - θ) * x + θ) - Real.log ((1 - θ) * y + θ)| ≤
      |Real.log x - Real.log y| := by
…

theorem OAI.LipschitzHilbert.fixed_path_blended_cell_sup line 196

Source documentation

The source's final blended prediction obeys the same relative-drop cell supremum bound as its unblended model.

theorem fixed_path_blended_cell_sup (frequency : ι → κ → ℝ)
    (a : ι → EuclideanSpace ℂ κ) (Y : EuclideanSpace ℂ κ) (I : Set ℝ)
    {s L p denominator H K u θ : ℝ} (hs : s ∈ I)
    (hL : 0 ≤ L) (hp : 1 ≤ p) (hd : 0 < denominator) (hH : 0 ≤ H)
    (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1)
    (hfrequency : ∀ i j, |frequency i j| ≤ L)
    (hdiameter : ∀ t ∈ I, |t - s| ≤ H) (hmass : ∑ i, ‖a i‖ ≤ K * u) :
    let B := fun t => (1 - θ) * energyRatio p denominator (Y + diagonalFourierSum frequency a t) + θ
…

Mentions: OAI.LipschitzHilbert.energyRatio