OAI/Analysis/LipschitzHilbert/Trees/SourceBlockGraph.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.AngularGrid.source_block_coefficient_bounds line 19

   Source documentation

   The transition coefficient on each actual child satisfies the graph bound with the actual source boundary mass.

   theorem source_block_coefficient_bounds {ι : Type*}
       (g : AngularGrid) (tops : Finset ι) (slope precision : ι → ℝ) (cutoff : ℝ)
       (weight : ι → (ℝ × ℝ) → ℝ) (hp : ∀ t ∈ tops, 0 ≤ precision t)
       (hw : ∀ t z, 0 < weight t z) {Kb : ℕ} (hKb : 0 < Kb)
       (gap : ℕ → ℝ) (phase : Fin Kb → ℂ) (σ : Fin Kb) (j : ℕ)
       (hphase : ∀ τ, τ ≠ σ → (phase τ).re = 0) (μ : ℝ) (hμ : 0 ≤ μ)
       (hreal : (phase σ).re = μ) (parent : ℤ) (z : ℝ × ℝ) :
       let lower := ShiftedBlocks.endpoint σ j
   …

   Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.ShiftedBlocks.endpoint

2. theorem OAI.LipschitzHilbert.AngularGrid.source_block_graph_data line 73

   Source documentation

   All positivity, graph-mass, separated-frequency, and supported-count premises follow from the actual shifted block and the separated-top count.

   theorem source_block_graph_data {ι κ : Type} [DecidableEq ι] [Fintype κ]
       (g : AngularGrid) (L : ℝ) (hbranch : (g.branching:ℝ) = SourceParameters.step L)
       (hKb : 0 < SourceParameters.blockCount L) (σ : Fin (SourceParameters.blockCount L)) (j : ℕ)
       (tops : Finset ι) (T : ι → SlopeBox) (w : ℝ) (hw : 0 < w)
       (weight : ι → (ℝ × ℝ) → ℝ) (hweight : ∀ t z, 0 < weight t z)
       (parent : ℤ) (z : ℝ × ℝ)
       (path : g.sourceBlockCells tops (fun t => (T t).slope) (fun t => w/(T t).length)
         (g.rootWidth/(SourceParameters.branching L)^2)
         (ShiftedBlocks.endpoint σ j) (ShiftedBlocks.endpoint σ (j+1)) parent)
       (A : g.sourceBlockCells tops (fun t => (T t).slope) (fun t => w/(T t).length)
         (g.rootWidth/(SourceParameters.branching L)^2)
         (ShiftedBlocks.endpoint σ j) (ShiftedBlocks.endpoint σ (j+1)) parent → EuclideanSpace ℂ κ)
   …

   Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SourceParameters.step, OAI.LipschitzHilbert.SourceParameters.blockCount, OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.SourceParameters.branching, OAI.LipschitzHilbert.ShiftedBlocks.endpoint