SourceLabeledResidualEnvelope.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A block's original packet set is restricted to each length before using the fixed positive reference family. The bound is independent of which path or mass cutoff selected the block.

theorem OAI.LipschitzHilbert.sum_sigma_fiber line 17
def OAI.LipschitzHilbert.SourceLabeledLattice.physicalPacketValue line 33
theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalPacketValue_length_envelope line 39

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physical_packet_residual_square_sum line 66

Source documentation

The actual source residual square now follows from the original coefficient split and packet geometry; no residual-envelope premise remains.

theorem physical_packet_residual_square_sum {τ : Type*}
    (horder : 6 ≤ P.order) (i : Fin 3) (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