SourceShiftedScales.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual shifted angular blocks meet the source scale conditions. The first block is included with its original shorter length.

theorem OAI.LipschitzHilbert.AngularGrid.source_width_ratio line 13

Source documentation

The ratio of actual angular widths is exactly the iterated step.

theorem source_width_ratio (g : AngularGrid) (L : ℝ) {lower upper : ℕ}
    (hle : lower ≤ upper) (hbranch : (g.branching:ℝ) = SourceParameters.step L) :
    g.width lower = SourceParameters.step L^(upper-lower)*g.width upper := by
…

Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SourceParameters.step

theorem OAI.LipschitzHilbert.AngularGrid.source_shifted_width_bounds line 25

Source documentation

Every source block has width ratio between G and B, with exactly the same conclusion for the initial block.

theorem source_shifted_width_bounds (g : AngularGrid) (L : ℝ)
    (hbranch : (g.branching:ℝ) = SourceParameters.step L)
    (hK : 0 < SourceParameters.blockCount L) (σ : Fin (SourceParameters.blockCount L)) (j : ℕ) :
    SourceParameters.step L*g.width (ShiftedBlocks.endpoint σ (j+1)) ≤
        g.width (ShiftedBlocks.endpoint σ j) ∧
      g.width (ShiftedBlocks.endpoint σ j) ≤
        SourceParameters.branching L*g.width (ShiftedBlocks.endpoint σ (j+1)) := by
…

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

theorem OAI.LipschitzHilbert.AngularGrid.source_shifted_count_scales line 47

Source documentation

Consequently the geometric precision and span hypotheses for the simultaneous count follow from the shifted source block itself.

theorem source_shifted_count_scales (g : AngularGrid) (L : ℝ)
    (hbranch : (g.branching:ℝ) = SourceParameters.step L)
    (hK : 0 < SourceParameters.blockCount L) (σ : Fin (SourceParameters.blockCount L)) (j : ℕ) :
    (g.rootWidth/(SourceParameters.branching L)^2)/
        (g.branching:ℝ)^(ShiftedBlocks.endpoint σ (j+1)) ≤
      g.sourceGap L (ShiftedBlocks.endpoint σ (j+1))/(SourceParameters.branching L)^2 ∧
    g.width (ShiftedBlocks.endpoint σ j) ≤ SourceParameters.branching L*
      g.sourceGap L (ShiftedBlocks.endpoint σ (j+1)) :=
…

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