SourceBlockModulus.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

At a vertex of the phase simplex, a complete shifted source block has only one nonunit transition modulus. Its coefficient is exactly the child-to-boundary power used in the dominant-path comparison.

theorem OAI.LipschitzHilbert.AngularGrid.source_shifted_block_norm line 14
theorem OAI.LipschitzHilbert.AngularGrid.source_shifted_block_mass_bounds line 43
theorem OAI.LipschitzHilbert.AngularGrid.source_shifted_path_coefficient_eq line 61

theorem OAI.LipschitzHilbert.AngularGrid.source_shifted_path_coefficient_motion line 87

Source documentation

The actual shifted-block coefficient inherits the complementary-mass motion estimate, with the path drop left as a factor.

theorem source_shifted_path_coefficient_motion {ι : Type*} {Kb : ℕ}
    (g : AngularGrid) (tops : Finset ι) (T : ι → SlopeBox)
    (w B Kw D : ℝ) (hw : 0 < w) (hB : 1 ≤ B) (hKw : 0 < Kw) (hD : 0 ≤ D)
    (hwidth : ∀ t ∈ tops, B^2*w ≤ (T t).width)
    (hKb : 0 < Kb) (gap : ℕ → ℝ) (phase : Fin Kb → ℂ) (σ : Fin Kb) (j : ℕ)
    (μ r u : ℝ) (hμ0 : 0 ≤ μ) (hμ1 : μ ≤ 1) (hr : 1 ≤ r)
    (ha : 0 ≤ 1-μ-1/r)
    (hphase : ∀ τ, τ ≠ σ → (phase τ).re = 0) (hreal : (phase σ).re = μ)
    (top : ι) (htop : top ∈ tops)
    (he : g.eligible (g.rootWidth/B^2) (w/(T top).length) (ShiftedBlocks.endpoint σ (j+1)))
    (h : ℕ) (hbase : h ≤ ShiftedBlocks.endpoint σ j)
    (sR : ℝ) (hs : g.index h (T top).slope = g.index h sR)
…

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