SourceSupportedGrid.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Zero snapshot vectors do not enter the angular count. Retain the chosen path even when its snapshot vanishes, so all relative errors use the same path.

theorem OAI.LipschitzHilbert.sum_restrict_zero line 16
theorem OAI.LipschitzHilbert.sum_injective_nonneg line 22
theorem OAI.LipschitzHilbert.restricted_neighborhood_mass line 29

theorem OAI.LipschitzHilbert.exists_source_supported_grid_prediction line 48

Source documentation

The graph count is needed only on nonzero snapshot children and the path. The original prediction and its full off-path coefficient budget are preserved.

theorem exists_source_supported_grid_prediction :
    ∃ C L0 : ℝ, 1 ≤ C ∧ ∀ L : ℝ, L0 ≤ L →
      ∀ (ι κ : Type) [Fintype ι] [Fintype κ]
      (grid : FiniteLineGrid) (level : ℕ), level ≤ grid.depth →
      ∀ (G : ι → ι → Prop), (∀ ⦃i j⦄, G i j → G j i) →
      ∀ (w m : ι → ℝ), (∀ i, 0 < w i) →
      (∀ i, orderMass w (closedNeighborhood G i) ≤ m i) →
      ∀ (frequency : ι → κ → ℝ) (l : ι → ℝ) (X : ι → EuclideanSpace ℂ κ)
        (lam : ι → ℂ) (i₀ : ι) (D p K u freqBound θ : ℝ),
      1 ≤ D → 4 ≤ p →
      (∀ i j, i ≠ j → ¬G i j → ∀ k,
        1/(grid.width*SourceParameters.step L^(-(1/8:ℝ))) ≤
…

Mentions: OAI.LipschitzHilbert.FiniteLineGrid, OAI.LipschitzHilbert.orderMass, OAI.LipschitzHilbert.closedNeighborhood, OAI.LipschitzHilbert.SourceParameters.step