OAI/Geometry/DoublingHilbert/Rectangles.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Rectangle probability measures, transport estimates, and finite averaging.

  1. structure OAI.DoublingHilbert.Segment line 16

    Source documentation

    Uniform probability on a nondegenerate real interval.

    structure Segment where
…
  2. def OAI.DoublingHilbert.Segment.length line 23
  3. theorem OAI.DoublingHilbert.Segment.length_pos line 25
  4. def OAI.DoublingHilbert.Segment.law line 27
  5. instance OAI.DoublingHilbert.Segment.(instance at line 30) line 30
  6. theorem OAI.DoublingHilbert.Segment.ae_iff line 37
  7. theorem OAI.DoublingHilbert.Segment.ae_mem line 42
  8. theorem OAI.DoublingHilbert.Segment.ae_of_ae line 47
  9. theorem OAI.DoublingHilbert.Segment.integral_eq line 50
  10. theorem OAI.DoublingHilbert.Segment.integrable_iff line 56
  11. structure OAI.DoublingHilbert.Rectangle line 67
  12. def OAI.DoublingHilbert.Rectangle.law line 73
  13. def OAI.DoublingHilbert.Rectangle.closed line 75
  14. def OAI.DoublingHilbert.Rectangle.interior line 78
  15. instance OAI.DoublingHilbert.Rectangle.(instance at line 81) line 81
  16. theorem OAI.DoublingHilbert.Rectangle.ae_mem line 85
  17. theorem OAI.DoublingHilbert.Rectangle.ae_of_ae line 89
  18. theorem OAI.DoublingHilbert.Rectangle.integral_eq line 96
  19. theorem OAI.DoublingHilbert.Rectangle.integral_eq_swap line 101
  20. def OAI.DoublingHilbert.IsBoundedField line 112

    Source documentation

    Globally bounded strongly measurable fields; all derivative selections below have this property.

    def IsBoundedField (g : X → E) : Prop :=
…
  21. theorem OAI.DoublingHilbert.IsBoundedField.integrable line 117
  22. theorem OAI.DoublingHilbert.IsBoundedField.norm_sq line 122
  23. theorem OAI.DoublingHilbert.IsBoundedField.sub line 129
  24. theorem OAI.DoublingHilbert.IsBoundedField.const line 135
  25. theorem OAI.DoublingHilbert.Rectangle.law_eq line 149
  26. theorem OAI.DoublingHilbert.IsBoundedField.comp_measurable line 163
  27. theorem OAI.DoublingHilbert.IsBoundedField.select line 167
  28. theorem OAI.DoublingHilbert.IsBoundedField.integral_snd line 188
  29. theorem OAI.DoublingHilbert.IsBoundedField.integral_fst line 195
  30. theorem OAI.DoublingHilbert.boundedField_column line 215
  31. theorem OAI.DoublingHilbert.norm_integral_rectangle_le_x line 220
  32. theorem OAI.DoublingHilbert.norm_integral_rectangle_le_y line 228
  33. theorem OAI.DoublingHilbert.horizontal_mean_bound line 236

    Source documentation

    Endpoint transport for a measurably selected horizontal sheet on each row.

    theorem horizontal_mean_bound {ι : Type*} [Fintype ι] [MeasurableSpace ι]
    [MeasurableSingletonClass ι] (Q : Rectangle)
    {F : Base → E} {G : ι → Base → E} {C : NNReal} {C' : ι → NNReal}
    (hF : LipschitzWith C F) (hG : ∀ i, LipschitzWith (C' i) (G i))
    {σ : ℝ → ι} (hσ : Measurable σ) {R : ℝ}
    (hleft : ∀ᵐ y ∂Q.y.law, ‖G (σ y) (Q.x.lo, y) - F (Q.x.lo, y)‖ ≤ R)
    (hright : ∀ᵐ y ∂Q.y.law, ‖G (σ y) (Q.x.hi, y) - F (Q.x.hi, y)‖ ≤ R) :
    ‖(∫ p, column (G (σ p.2)) (1, 0) p ∂Q.law) -
      (∫ p, column F (1, 0) p ∂Q.law)‖ ≤ 2 * R / Q.x.length := by
…

    Mentions: OAI.DoublingHilbert.Rectangle, OAI.DoublingHilbert.Base, OAI.DoublingHilbert.column

  34. theorem OAI.DoublingHilbert.vertical_mean_bound line 272

    Source documentation

    Endpoint transport for a selected vertical sheet on each column.

    theorem vertical_mean_bound {ι : Type*} [Fintype ι] [MeasurableSpace ι]
    [MeasurableSingletonClass ι] (Q : Rectangle)
    {F : Base → E} {G : ι → Base → E} {C : NNReal} {C' : ι → NNReal}
    (hF : LipschitzWith C F) (hG : ∀ i, LipschitzWith (C' i) (G i))
    {σ : ℝ → ι} (hσ : Measurable σ) {R : ℝ}
    (hbottom : ∀ᵐ x ∂Q.x.law, ‖G (σ x) (x, Q.y.lo) - F (x, Q.y.lo)‖ ≤ R)
    (htop : ∀ᵐ x ∂Q.x.law, ‖G (σ x) (x, Q.y.hi) - F (x, Q.y.hi)‖ ≤ R) :
    ‖(∫ p, column (G (σ p.1)) (0, 1) p ∂Q.law) -
      (∫ p, column F (0, 1) p ∂Q.law)‖ ≤ 2 * R / Q.y.length := by
…

    Mentions: OAI.DoublingHilbert.Rectangle, OAI.DoublingHilbert.Base, OAI.DoublingHilbert.column

  35. def OAI.DoublingHilbert.Rectangle.area line 317
  36. theorem OAI.DoublingHilbert.Rectangle.area_pos line 319
  37. theorem OAI.DoublingHilbert.Rectangle.law_eq_closed line 321
  38. theorem OAI.DoublingHilbert.Rectangle.volume_closed line 328
  39. theorem OAI.DoublingHilbert.Rectangle.integral_eq_average_closed line 332
  40. theorem OAI.DoublingHilbert.Rectangle.integral_eq_closed line 337
  41. theorem OAI.DoublingHilbert.Rectangle.area_mul_integral line 343
  42. theorem OAI.DoublingHilbert.Rectangle.integral_le_four_of_subset line 348

    Source documentation

    Trimming at most half of each side increases a nonnegative mean by at most four.

    theorem integral_le_four_of_subset (P Q : Rectangle) {g : Base → ℝ}
    (hg : IsBoundedField g) (hpos : ∀ p, 0 ≤ g p)
    (hsub : Q.closed ⊆ P.closed)
    (hx : P.x.length / 2 ≤ Q.x.length) (hy : P.y.length / 2 ≤ Q.y.length) :
    (∫ p, g p ∂Q.law) ≤ 4 * (∫ p, g p ∂P.law) := by
…

    Mentions: OAI.DoublingHilbert.Rectangle, OAI.DoublingHilbert.Base, OAI.DoublingHilbert.IsBoundedField

  43. def OAI.DoublingHilbert.Rectangle.square line 366
  44. theorem OAI.DoublingHilbert.Rectangle.square_closed line 369
  45. theorem OAI.DoublingHilbert.goodSheetPoint_exists_rectangle line 382

    Source documentation

    Actual Lebesgue-good derivative points supply arbitrarily accurate base squares.

    theorem goodSheetPoint_exists_rectangle {f : constructedSet → E} {D : NNReal}
    (hf : LipschitzWith D f) {w : Tuple} {p : Base} (hp : goodSheetPoint f w p)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ Q : Rectangle, Q.closed ⊆ sheetDomain w ∧
      (∫ q, ‖column (globalSheet hf w) (1, 0) q -
        sheetColumn (embeddingSheet f w) (sheetDomain w) (1, 0) p‖ ^ 2 ∂Q.law) < ε ∧
      (∫ q, ‖column (globalSheet hf w) (0, 1) q -
        sheetColumn (embeddingSheet f w) (sheetDomain w) (0, 1) p‖ ^ 2 ∂Q.law) < ε := by
…

    Mentions: OAI.DoublingHilbert.constructedSet, OAI.DoublingHilbert.Tuple, OAI.DoublingHilbert.Base, OAI.DoublingHilbert.goodSheetPoint, OAI.DoublingHilbert.Rectangle, OAI.DoublingHilbert.sheetDomain, OAI.DoublingHilbert.column, OAI.DoublingHilbert.globalSheet, OAI.DoublingHilbert.sheetColumn, OAI.DoublingHilbert.embeddingSheet

  46. def OAI.DoublingHilbert.Segment.grid line 419
  47. def OAI.DoublingHilbert.Segment.cell line 424
  48. theorem OAI.DoublingHilbert.Segment.grid_length line 427
  49. theorem OAI.DoublingHilbert.Segment.cell_length line 430
  50. theorem OAI.DoublingHilbert.Segment.integral_grid line 434

    Source documentation

    Exact finite averaging over adjacent equal cells.

    theorem integral_grid {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (a h : ℝ) {n : ℕ} (hh : 0 < h) (hn : 0 < n) {g : ℝ → E}
    (hg : IsBoundedField g) :
    (∫ x, g x ∂(grid a h n hh hn).law) =
      (n : ℝ)⁻¹ • ∑ i : Fin n, ∫ x, g x ∂(cell a h hh i).law := by
…

    Mentions: OAI.DoublingHilbert.IsBoundedField, OAI.DoublingHilbert.Segment.grid, OAI.DoublingHilbert.Segment.law, OAI.DoublingHilbert.Segment.cell

  51. theorem OAI.DoublingHilbert.Rectangle.integral_grid_x line 456

    Source documentation

    Exact integration by columns.

    theorem integral_grid_x {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (a h : ℝ) {n : ℕ} (hh : 0 < h) (hn : 0 < n) (J : Segment) {g : ℝ × ℝ → E}
    (hg : IsBoundedField g) :
    (∫ p, g p ∂(Rectangle.mk (Segment.grid a h n hh hn) J).law) =
      (n : ℝ)⁻¹ • ∑ i : Fin n, ∫ p, g p ∂(Rectangle.mk (Segment.cell a h hh i) J).law := by
…

    Mentions: OAI.DoublingHilbert.Segment, OAI.DoublingHilbert.IsBoundedField, OAI.DoublingHilbert.Segment.grid, OAI.DoublingHilbert.Rectangle.law, OAI.DoublingHilbert.Segment.cell

  52. theorem OAI.DoublingHilbert.Rectangle.integral_grid_y line 470

    Source documentation

    Exact integration by rows.

    theorem integral_grid_y {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (a h : ℝ) {n : ℕ} (hh : 0 < h) (hn : 0 < n) (I : Segment) {g : ℝ × ℝ → E}
    (hg : IsBoundedField g) :
    (∫ p, g p ∂(Rectangle.mk I (Segment.grid a h n hh hn)).law) =
      (n : ℝ)⁻¹ • ∑ i : Fin n, ∫ p, g p ∂(Rectangle.mk I (Segment.cell a h hh i)).law := by
…

    Mentions: OAI.DoublingHilbert.Segment, OAI.DoublingHilbert.IsBoundedField, OAI.DoublingHilbert.Segment.grid, OAI.DoublingHilbert.Rectangle.law, OAI.DoublingHilbert.Segment.cell