OAI/Analysis/LipschitzHilbert/Trees/SourceReverseBlocks.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

The source line windows grow along the angular path. Reading those windows in reverse gives increasing levels in one finite line grid. Only the factors are reordered: the stopping budget retains its forward mass path, including the possibility of a zero terminal mass.

  1. def OAI.LipschitzHilbert.ShiftedBlocks.reverseLevel line 21
  2. def OAI.LipschitzHilbert.ShiftedBlocks.reverseIndex line 24
  3. theorem OAI.LipschitzHilbert.ShiftedBlocks.reverseLevel_zero line 26
  4. theorem OAI.LipschitzHilbert.ShiftedBlocks.reverseLevel_last line 30
  5. theorem OAI.LipschitzHilbert.ShiftedBlocks.reverseLevel_le line 34
  6. theorem OAI.LipschitzHilbert.ShiftedBlocks.reverseLevel_monotone line 37
  7. theorem OAI.LipschitzHilbert.ShiftedBlocks.reverseLevel_step_lt line 43
  8. theorem OAI.LipschitzHilbert.ShiftedBlocks.reverseIndex_lt line 50
  9. theorem OAI.LipschitzHilbert.ShiftedBlocks.reverseIndex_involutive line 55
  10. theorem OAI.LipschitzHilbert.ShiftedBlocks.reverseLevel_block_start line 60
  11. theorem OAI.LipschitzHilbert.ShiftedBlocks.reverseLevel_block_end line 67
  12. theorem OAI.LipschitzHilbert.ShiftedBlocks.reverseLevel_block_length line 74
  13. theorem OAI.LipschitzHilbert.ShiftedBlocks.sum_reverseIndex line 84
  14. theorem OAI.LipschitzHilbert.ShiftedBlocks.prod_reverseIndex line 89
  15. def OAI.LipschitzHilbert.sourceReverseLineGrid line 100

    Source documentation

    A single root line grid contains every source block window, in reverse angular order. Its depth includes the shorter initial source block exactly.

    def sourceReverseLineGrid {K : ℕ} (g : AngularGrid) (L origin : ℝ) {w : ℝ}
    (hw : 0 < w) (σ : Fin K) (count : ℕ) : FiniteLineGrid :=
…

    Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.FiniteLineGrid

  16. theorem OAI.LipschitzHilbert.sourceReverseLineGrid_levels line 106
  17. theorem OAI.LipschitzHilbert.source_reverse_line_mesh line 115
  18. theorem OAI.LipschitzHilbert.source_reverse_block_coarse line 127

    Source documentation

    The coarse side of original block j is its child window.

    theorem source_reverse_block_coarse {K : ℕ} (g : AngularGrid) (L origin : ℝ) {w : ℝ}
    (hw : 0 < w) (σ : Fin K) (hK : 0 < K) {count j : ℕ} (hj : j < count)
    (hbranch : (g.branching:ℝ) = SourceParameters.step L) :
    (sourceReverseLineGrid g L origin hw σ count).meshWidth
        (ShiftedBlocks.reverseLevel σ count (ShiftedBlocks.reverseIndex count j)) =
      sourceLineScale g L w (ShiftedBlocks.endpoint σ (j+1)) := by
…

    Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SourceParameters.step, OAI.LipschitzHilbert.sourceReverseLineGrid, OAI.LipschitzHilbert.ShiftedBlocks.reverseLevel, OAI.LipschitzHilbert.ShiftedBlocks.reverseIndex, OAI.LipschitzHilbert.sourceLineScale, OAI.LipschitzHilbert.ShiftedBlocks.endpoint

  19. theorem OAI.LipschitzHilbert.source_reverse_block_fine line 139

    Source documentation

    Refining that child window across the block gives its parent mesh.

    theorem source_reverse_block_fine {K : ℕ} (g : AngularGrid) (L origin : ℝ) {w : ℝ}
    (hw : 0 < w) (σ : Fin K) (hK : 0 < K) {count j : ℕ} (hj : j < count)
    (hbranch : (g.branching:ℝ) = SourceParameters.step L) :
    (sourceReverseLineGrid g L origin hw σ count).meshWidth
        (ShiftedBlocks.reverseLevel σ count (ShiftedBlocks.reverseIndex count j+1)) =
      sourceLineScale g L w (ShiftedBlocks.endpoint σ j) := by
…

    Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SourceParameters.step, OAI.LipschitzHilbert.sourceReverseLineGrid, OAI.LipschitzHilbert.ShiftedBlocks.reverseLevel, OAI.LipschitzHilbert.ShiftedBlocks.reverseIndex, OAI.LipschitzHilbert.sourceLineScale, OAI.LipschitzHilbert.ShiftedBlocks.endpoint

  20. theorem OAI.LipschitzHilbert.source_reverse_local_mesh line 150
  21. theorem OAI.LipschitzHilbert.source_reverse_local_path_integral line 170

    Source documentation

    Local prediction factors can be integrated in reverse angular order. The hypothesis on their errors remains the original forward sum. Thus a forward stopped-mass estimate can be used without reversing its masses.

    theorem source_reverse_local_path_integral
    (g : FiniteLineGrid) (T : SlopeBox) (K D y E : ℝ)
    (hK : 1 ≤ K) (hD : 0 ≤ D) (hwidth : g.width ≤ T.length)
    (level : ℕ → ℕ) (count : ℕ) (hlevel : ∀ j ≤ count, level j ≤ g.depth)
    (hmono : ∀ j < count, level j ≤ level (j+1))
    (good : Set ℝ) (beta error : ℕ → ℝ → ℝ) (F : ℕ → ℕ → ℝ → ℝ)
    (hF : ∀ j < count, ∀ i < g.branching^level j, ∀ x,
      0 ≤ F (ShiftedBlocks.reverseIndex count j) i x)
    (hint : ∀ j < count, ∀ i < g.branching^level j,
      Integrable (F (ShiftedBlocks.reverseIndex count j) i) (intervalProbability
        (g.lineWindow (level j) i (level (j+1)-level j)).origin
        ((g.lineWindow (level j) i (level (j+1)-level j)).origin+
…

    Mentions: OAI.LipschitzHilbert.FiniteLineGrid, OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.ShiftedBlocks.reverseIndex, OAI.LipschitzHilbert.intervalProbability