Integration.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Line integration and global Lipschitz extensions of sheets.

theorem OAI.DoublingHilbert.integral_eq_sub_of_lipschitz_ae_derivative line 21

Source documentation

Vector-valued FTC for a Lipschitz curve with its a.e. derivative specified. This is the scalar absolutely-continuous FTC tested against the continuous dual.

theorem integral_eq_sub_of_lipschitz_ae_derivative
    {f g : ℝ → E} {a b : ℝ} {C : NNReal}
    (hf : LipschitzOnWith C f (uIcc a b))
    (hg : IntervalIntegrable g volume a b)
    (hderiv : ∀ᵐ x, x ∈ uIcc a b → HasDerivAt f (g x) x) :
    (∫ x in a..b, g x) = f b - f a := by
…

theorem OAI.DoublingHilbert.norm_integral_derivative_sub_le line 39

Source documentation

The endpoint estimate used for each full horizontal or vertical strip.

theorem norm_integral_derivative_sub_le
    {f g f' g' : ℝ → E} {a b R : ℝ} {C₁ C₂ : NNReal}
    (hf : LipschitzOnWith C₁ f (uIcc a b))
    (hg : LipschitzOnWith C₂ g (uIcc a b))
    (hf' : IntervalIntegrable f' volume a b)
    (hg' : IntervalIntegrable g' volume a b)
    (hdf : ∀ᵐ x, x ∈ uIcc a b → HasDerivAt f (f' x) x)
    (hdg : ∀ᵐ x, x ∈ uIcc a b → HasDerivAt g (g' x) x)
    (ha : ‖f a - g a‖ ≤ R) (hb : ‖f b - g b‖ ≤ R) :
    ‖∫ x in a..b, f' x - g' x‖ ≤ 2 * R := by
…

theorem OAI.DoublingHilbert.norm_average_sq_le_average_norm_sq line 64

Source documentation

Hilbert-space Cauchy--Schwarz in the form needed for line transport; in fact convexity makes this valid for every normed target.

theorem norm_average_sq_le_average_norm_sq [IsFiniteMeasure μ] [NeZero μ]
    {G : X → E} (hG : Integrable G μ)
    (hG2 : Integrable (fun x => ‖G x‖ ^ 2) μ) :
    ‖⨍ x, G x ∂μ‖ ^ 2 ≤ ⨍ x, ‖G x‖ ^ 2 ∂μ := by
…

theorem OAI.DoublingHilbert.norm_integral_sq_le_mass_mul line 74

Source documentation

The integral version of the preceding averaged estimate, retaining the exact mass.

theorem norm_integral_sq_le_mass_mul [IsFiniteMeasure μ]
    {G : X → E} (hG : Integrable G μ)
    (hG2 : Integrable (fun x => ‖G x‖ ^ 2) μ) :
    ‖∫ x, G x ∂μ‖ ^ 2 ≤ μ.real Set.univ * (∫ x, ‖G x‖ ^ 2 ∂μ) := by
…

theorem OAI.DoublingHilbert.curve_oscillation_sq_le_integral line 90

Source documentation

Squared oscillation of a Lipschitz curve is bounded by its derivative energy.

theorem curve_oscillation_sq_le_integral
    {f g : ℝ → E} {a b : ℝ} {C : NNReal} (hab : a ≤ b)
    (hf : LipschitzOnWith C f (uIcc a b))
    (hg : IntervalIntegrable g volume a b)
    (hg2 : IntervalIntegrable (fun x => ‖g x‖ ^ 2) volume a b)
    (hderiv : ∀ᵐ x, x ∈ uIcc a b → HasDerivAt f (g x) x) :
    ‖f b - f a‖ ^ 2 ≤ (b - a) * (∫ x in a..b, ‖g x‖ ^ 2) := by
…

def OAI.DoublingHilbert.column line 115
Source documentation
Actual derivative columns of global extensions.
```
def column (f : ℝ × ℝ → E) (v : ℝ × ℝ) (p : ℝ × ℝ) : E := fderiv ℝ f p v
…
```
theorem OAI.DoublingHilbert.norm_column_le line 118
theorem OAI.DoublingHilbert.stronglyMeasurable_column line 124
theorem OAI.DoublingHilbert.intervalIntegrable_of_bound line 132
theorem OAI.DoublingHilbert.intervalIntegrable_column_x line 139
theorem OAI.DoublingHilbert.intervalIntegrable_column_y line 148
theorem OAI.DoublingHilbert.lipschitz_line_x line 157
theorem OAI.DoublingHilbert.lipschitz_line_y line 164
theorem OAI.DoublingHilbert.ae_line_derivative_x line 171
theorem OAI.DoublingHilbert.ae_line_derivative_y line 181
theorem OAI.DoublingHilbert.ae_integral_column_x line 190
Source documentation
Fubini plus the vector FTC controls every subinterval on almost every horizontal line.
```
theorem ae_integral_column_x {f : ℝ × ℝ → E} {C : NNReal} (hf : LipschitzWith C f) :
    ∀ᵐ y, ∀ a b : ℝ, (∫ x in a..b, column f (1, 0) (x, y)) = f (b, y) - f (a, y) := by
…
```
Mentions: OAI.DoublingHilbert.column

theorem OAI.DoublingHilbert.ae_integral_column_y line 198

Source documentation

The corresponding vertical-line identity.

theorem ae_integral_column_y {f : ℝ × ℝ → E} {C : NNReal} (hf : LipschitzWith C f) :
    ∀ᵐ x, ∀ a b : ℝ, (∫ y in a..b, column f (0, 1) (x, y)) = f (x, b) - f (x, a) := by
…

Mentions: OAI.DoublingHilbert.column

def OAI.DoublingHilbert.globalSheet line 216
theorem OAI.DoublingHilbert.globalSheet_lipschitz line 221
theorem OAI.DoublingHilbert.globalSheet_eqOn line 229
theorem OAI.DoublingHilbert.column_globalSheet line 237
theorem OAI.DoublingHilbert.ae_globalSheet_pair line 245