OAI/Analysis/LipschitzHilbert/Trees/SourceLabeledCrossResidual.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.actual_cross_packet_subset_envelope line 25

   Source documentation

   Change only synthesis profiles; the analyzing coefficient and both positive reference quantities remain those of the original family.

   theorem actual_cross_packet_subset_envelope (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)
       (g : ℝ×ℝ → EuclideanSpace ℂ κ) (hg : Measurable g) (hg1 : ∀ z, ‖g z‖ ≤ 1)
       (j : Fin N) (Q : Finset (Σ l : P.labels j, Item j l)) (y x : ℝ) :
       (∑ q ∈ Q, ‖(P.withProfile alt hAlt).rawPacketValue i j q.1 q.2
         (P.physicalMultiplierCoefficient t b v g j q.1 q.2) y x‖) ≤
           P.absoluteConstant*(P.physicalErrorScale t a b v g j y x+
             P.physicalMainScale t a b v g j y x) := by
   …

   Mentions: OAI.LipschitzHilbert.SourceLabeledLattice.rawPacketValue

2. def OAI.LipschitzHilbert.SourceLabeledLattice.physicalCrossPacketValue line 41
3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalCrossPacketValue_length_envelope line 47
4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physical_cross_packet_residual_square_sum line 74

   Source documentation

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

   theorem physical_cross_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

5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physical_cross_packet_residual_square_polynomial line 119