SourcePhysicalResidualSquare.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The original masked physical residual blocks inherit the square bound from the original analyzing/alternate-synthesis decomposition.

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physical_masked_packet_residual_square_polynomial line 19

Source documentation

Actual top masks and original physical packets satisfy the marked residual square estimate; the analyzing coefficient is unchanged.

theorem physical_masked_packet_residual_square_polynomial {τ : Type*}
    (horder : 6 ≤ P.order) (t a : ℝ)
    (b : ∀ j, P.labels j → κ → ℝ → ℂ) (hb : ∀ j l k, Measurable (b j l k))
    (hb1 : ∀ j l k s, ‖b j l k s‖ ≤ 1)
    (v : ℝ×ℝ → ℝ) (hv : Measurable v)
    (f : ℝ×ℝ → EuclideanSpace ℂ κ) (hf : Measurable f) (hf1 : ∀ z, ‖f z‖ ≤ 1)
    (grid : AngularGrid) (tops : Finset τ) (slope precision : τ → ℝ) (cutoff : ℝ)
    (weight : τ → ℝ×ℝ → ℝ)
    (hp : ∀ T ∈ tops, 0 ≤ precision T) (hw : ∀ T z, 0 < weight T z)
    {K : ℕ} (hK : 0 < K) (gap : ℕ → ℝ) (phase : ℕ → ℂ)
    (hz : ∀ k, 0 ≤ (phase k).re) (alpha : ℝ) (ha : 0 ≤ alpha) (z : ℝ×ℝ)
    (packets : Finset P.PacketIndex) (assigned : P.PacketIndex → τ)
…

Mentions: OAI.LipschitzHilbert.AngularGrid