SourceFrozenCellIntegral.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Actual frozen long sums are measurable, have finite cell suprema, and integrate against the original common angular-support mask.

theorem OAI.LipschitzHilbert.masked_cell_norm_integral line 15

Source documentation

A bounded measurable function on a finite cell integrates over its mask with the exact mass of the intersection.

theorem masked_cell_norm_integral {X E : Type*} [MeasurableSpace X]
    [NormedAddCommGroup E] [NormedSpace ℝ E]
    (μ : Measure X) (C A : Set X) (hC : MeasurableSet C) (hA : MeasurableSet A)
    (hfin : μ C≠∞) (f : X → E) (hf : AEStronglyMeasurable f μ)
    (M : ℝ) (hbound : ∀ z∈C, ‖f z‖≤M) :
    IntegrableOn (A.indicator f) C μ ∧
      (∫ z in C, ‖A.indicator f z‖ ∂μ)≤M*μ.real (C∩A) := by
…

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalLongInterval_uniform_bound line 49
def OAI.LipschitzHilbert.SourceLabeledLattice.longCellSup line 70
theorem OAI.LipschitzHilbert.SourceLabeledLattice.longCellSup_nonneg line 76
theorem OAI.LipschitzHilbert.SourceLabeledLattice.frozenLongValue_measurable line 82

theorem OAI.LipschitzHilbert.SourceLabeledLattice.frozenLongValue_le_cell_sup line 108

Source documentation

Pointwise interval extraction controls the actual variable frozen selector on every half-open cell.

theorem frozenLongValue_le_cell_sup (w : ℝ) (hw : 0≤w)
    (c : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ)
    (u : ℝ×ℝ → ℝ) (b : ℝ) (p : (ℤ×ℤ)×ℤ) {z : ℝ×ℝ}
    (hz : z∈partitionCell b P.width p) :
    ‖P.frozenLongValue 0 (DyadicLineGrid.scale p.1.1) w (u z) c z‖≤P.longCellSup c b p := by
…

Mentions: OAI.LipschitzHilbert.DyadicLineGrid.scale

theorem OAI.LipschitzHilbert.SourceLabeledLattice.frozen_cell_integral line 118