OAI/Analysis/LipschitzHilbert/Phase/DiagonalCarrier.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Removing a distinguished diagonal carrier

The path-child carrier is a coordinatewise unitary. Removing it leaves the path vector fixed and subtracts its frequency from every off-path component. This is the exact transition to the small-drop model in §9.

  1. def OAI.LipschitzHilbert.diagonalRemainderFrequency line 27

    Source documentation

    Frequencies after the distinguished child's diagonal carrier is removed.

    def diagonalRemainderFrequency (frequency : ι → κ → ℝ) (i₀ : ι)
    (i : RemainderIndex i₀) (j : κ) : ℝ := frequency i j - frequency i₀ j
…
  2. theorem OAI.LipschitzHilbert.diagonal_carrier_identity line 31
  3. theorem OAI.LipschitzHilbert.diagonal_carrier_norm line 51
  4. theorem OAI.LipschitzHilbert.diagonal_carrier_energyRatio line 58
  5. theorem OAI.LipschitzHilbert.diagonalRemainderFrequency_separated line 68
  6. theorem OAI.LipschitzHilbert.diagonalRemainderFrequency_bound line 75
  7. theorem OAI.LipschitzHilbert.off_path_coefficient_sum line 83
  8. theorem OAI.LipschitzHilbert.diagonal_prediction_deficit line 91

    Source documentation

    A bounded off-path coefficient mass gives the relative prediction deficit for the original phase sum, after its carrier is removed exactly.

    theorem diagonal_prediction_deficit (frequency : ι → κ → ℝ)
    (a : ι → EuclideanSpace ℂ κ) (i₀ : ι) {p denominator B : ℝ}
    (hp : 1 ≤ p) (hd : 0 < denominator) (hB : 0 ≤ B)
    (hmass : (∑ i : RemainderIndex i₀, ‖a i‖) ≤ B)
    (hexceeds : ∃ t, 1 < energyRatio p denominator (diagonalFourierSum frequency a t)) (t : ℝ) :
    max (1 - energyRatio p denominator (diagonalFourierSum frequency a t)) 0 ≤ 2 * p * B := by
…

    Mentions: OAI.LipschitzHilbert.energyRatio