OAI/Analysis/LipschitzHilbert/Phase/AngularGraphPrediction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.AngularGrid.subtype_independent_card_le line 17
2. theorem OAI.LipschitzHilbert.AngularGrid.angular_graph_prediction_average line 41

   Source documentation

   The actual carrier frequencies inherit their gap from angular nonneighbors; the graph cardinality comes from the common spatial count, applied to finite subcollections of these cells.

   theorem angular_graph_prediction_average {κ : Type*} [Fintype κ]
       (g : AngularGrid) (level : ℕ) (cells : Finset ℤ)
       {gap etaMin D p : ℝ}
       (w m : cells → ℝ) (hw : ∀ i, 0 < w i)
       (hm : ∀ i, orderMass w (closedNeighborhood
         (fun i j : cells => g.neighbors level gap i.val j.val) i) ≤ m i)
       (ν : Measure ℝ) [IsProbabilityMeasure ν]
       (s : ℝ) (eta : κ → ℝ) (l : cells → ℝ)
       (X : cells → EuclideanSpace ℂ κ) (lambda : cells → ℂ)
       (hgap : 0 < gap) (hetaMin : 0 < etaMin)
       (heta : ∀ k, etaMin ≤ |eta k|)
       (hν : PhaseCombinatorics.FourierGap ν (gap * etaMin)) (hD : 1 ≤ D) (hp : 4 ≤ p)
   …

   Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.orderMass, OAI.LipschitzHilbert.closedNeighborhood, OAI.LipschitzHilbert.PhaseCombinatorics.FourierGap