OAI/Analysis/LipschitzHilbert/Trees/SourceCenteredCoefficient.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LipschitzHilbert.SourceLatticePacket.physicalCenteredWave line 16
2. def OAI.LipschitzHilbert.SourceLatticePacket.physicalCenteredCoefficient line 20
3. theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalCenteredWave_eq line 25
4. theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalCenteredCoefficient_eq line 45

   Source documentation

   Exact coefficient identity used for symmetric frozen selectors. All three terms have monotone thresholds whenever the original d does.

   theorem physicalCenteredCoefficient_eq (s t : ℝ) (d : Fin N → ℝ) (hd : ∀ j, 0 ≤ d j)
       (v : ℝ×ℝ → ℝ) (hv : Measurable v)
       (g : ℝ×ℝ → EuclideanSpace ℂ κ) (hg : Measurable g) (hg1 : ∀ z, ‖g z‖ ≤ 1)
       (j : Fin N) (u : ι j) :
       P.physicalCenteredCoefficient s t d v g j u =
         P.physicalCoefficient s (fun j => t+d j) v g j u+
         P.physicalCoefficient s (fun j => d j-t) (fun z => -v z) g j u-
         P.physicalCoefficient s (fun _ => 0) (fun _ => 0) g j u := by
   …

5. theorem OAI.LipschitzHilbert.SourceLatticePacket.centered_upper_monotone line 69
6. theorem OAI.LipschitzHilbert.SourceLatticePacket.centered_lower_monotone line 75