OAI/Geometry/DoublingHilbert/SelectedSheets.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DoublingHilbert.IsBoundedField.add line 18
2. theorem OAI.DoublingHilbert.IsBoundedField.const_mul line 25
3. theorem OAI.DoublingHilbert.horizontal_mean_bound_stripes line 40

   Source documentation

   Horizontal integration on each separate vertical strip; discontinuous selections are never differentiated across strip boundaries.

   theorem horizontal_mean_bound_stripes {ι : Type*} [Fintype ι] [MeasurableSpace ι]
       [MeasurableSingletonClass ι] (a h : ℝ) {n : ℕ} (hh : 0 < h) (hn : 0 < n)
       (J : Segment) {F : Base → E} {G : ι → Base → E}
       {C : NNReal} {C' : ι → NNReal}
       (hF : LipschitzWith C F) (hG : ∀ i, LipschitzWith (C' i) (G i))
       {σ : ℝ → ι} (hσ : Measurable σ) (c : Fin n → ι) {R : ℝ}
       (hcolor : ∀ i : Fin n, ∀ x ∈ Ioo (Segment.cell a h hh i).lo
         (Segment.cell a h hh i).hi, σ x = c i)
       (hbound : ∀ i : Fin n, ∀ x ∈ Ioo (Segment.cell a h hh i).lo
         (Segment.cell a h hh i).hi, ∀ y ∈ Ioo J.lo J.hi, ‖G (c i) (x, y) - F (x, y)‖ ≤ R) :
       ‖(∫ p, column (G (σ p.1)) (1, 0) p ∂(Rectangle.mk (Segment.grid a h n hh hn) J).law) -
         (∫ p, column F (1, 0) p ∂(Rectangle.mk (Segment.grid a h n hh hn) J).law)‖ ≤
   …

   Mentions: OAI.DoublingHilbert.Segment, OAI.DoublingHilbert.Base, OAI.DoublingHilbert.Segment.cell, OAI.DoublingHilbert.column, OAI.DoublingHilbert.Segment.grid

4. def OAI.DoublingHilbert.stripWidth line 103
5. theorem OAI.DoublingHilbert.stripWidth_pos line 105
6. def OAI.DoublingHilbert.xPeriod line 108
7. def OAI.DoublingHilbert.yPeriod line 110
8. theorem OAI.DoublingHilbert.xPeriod_pos line 112
9. theorem OAI.DoublingHilbert.yPeriod_pos line 115
10. structure OAI.DoublingHilbert.PeriodGrid line 119

    Source documentation

    A finite rectangle of complete level-j period blocks.

    structure PeriodGrid (j : ℕ) where
    …

11. def OAI.DoublingHilbert.PeriodGrid.rectangle line 130
12. theorem OAI.DoublingHilbert.PeriodGrid.exists_inside line 134
13. def OAI.DoublingHilbert.PeriodGrid.block line 147
14. theorem OAI.DoublingHilbert.PeriodGrid.block_subset line 151
15. theorem OAI.DoublingHilbert.PeriodGrid.exists_block_integral_le line 157
16. theorem OAI.DoublingHilbert.PeriodGrid.rectangle_x_subdivided line 167
17. theorem OAI.DoublingHilbert.PeriodGrid.block_x line 172
18. theorem OAI.DoublingHilbert.PeriodGrid.block_y line 179
19. def OAI.DoublingHilbert.residueColor line 188
20. theorem OAI.DoublingHilbert.residueColor_val line 193
21. theorem OAI.DoublingHilbert.color_on_cell line 197
22. theorem OAI.DoublingHilbert.Rectangle.interior_subset_closed line 219
23. def OAI.DoublingHilbert.addedSheet line 229
24. def OAI.DoublingHilbert.horizontalColumn line 233
25. def OAI.DoublingHilbert.verticalColumn line 237
26. theorem OAI.DoublingHilbert.bounded_horizontalColumn line 242
27. theorem OAI.DoublingHilbert.bounded_verticalColumn line 253
28. theorem OAI.DoublingHilbert.ae_horizontal_pair line 263
29. theorem OAI.DoublingHilbert.ae_vertical_pair line 280
30. theorem OAI.DoublingHilbert.horizontalColumn_mean line 298
31. theorem OAI.DoublingHilbert.verticalColumn_y_mean line 319
32. theorem OAI.DoublingHilbert.verticalColumn_x_mean line 352

    Source documentation

    The discontinuous vertical selection is integrated strip by strip.

    theorem verticalColumn_x_mean {f : constructedSet → E} {D : NNReal}
        (hf : LipschitzWith D f) (w : Tuple) (j : ℕ) (hj : w j = 0)
        (G : PeriodGrid j) (hQ : G.rectangle.closed ⊆ sheetDomain w) :
        ‖(∫ p, verticalColumn hf w j (1, 0) p ∂G.rectangle.law) -
          (∫ p, column (globalSheet hf w) (1, 0) p ∂G.rectangle.law)‖ ≤
          2 * D / (widthFactor j : ℝ) := by
    …

    Mentions: OAI.DoublingHilbert.constructedSet, OAI.DoublingHilbert.Tuple, OAI.DoublingHilbert.PeriodGrid, OAI.DoublingHilbert.sheetDomain, OAI.DoublingHilbert.verticalColumn, OAI.DoublingHilbert.column, OAI.DoublingHilbert.globalSheet, OAI.DoublingHilbert.widthFactor