OAI/Analysis/LipschitzHilbert/Phase/SourceAngularPrediction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.AngularGrid.source_angular_prediction_data line 18

   Source documentation

   Geometric data for a nonempty block, using exactly its eligible tops. The counting conclusion concerns only the shrunken support and the path.

   theorem source_angular_prediction_data {ι κ : Type} [DecidableEq ι] [Fintype κ]
       (g : AngularGrid) (tops : Finset ι) (T : ι → SlopeBox) (d : ι → ℝ)
       (cutoff : ℝ) (weight : ι → (ℝ × ℝ) → ℝ)
       (hd : ∀ i ∈ tops, 0 ≤ d i) (hw : ∀ i z, 0 < weight i z)
       (z : ℝ × ℝ) (base level : ℕ) (hle : base ≤ level) (parent : ℤ)
       (cells : Finset ℤ) (representative : cells → ℝ)
       (hcell : ∀ c, g.index (level+1) (representative c) = c.val)
       (hancestor : ∀ c, g.index base (representative c) = parent)
       (hnonempty : ∀ c : cells,
         (g.cellTops tops (fun i => (T i).slope) d cutoff (level+1) c.val).Nonempty)
       (path : cells) (A : cells → EuclideanSpace ℂ κ)
       {gap B K D ε threshold etaMin sR : ℝ}
   …

   Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SlopeBox