Derivatives.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Derivative fields, good points, and the compact set of derivative norms.

theorem OAI.DoublingHilbert.locallyIntegrable_of_uniform_bound line 20

Source documentation

A measurable uniformly bounded field on the source plane is locally integrable.

theorem locallyIntegrable_of_uniform_bound {G : ℝ × ℝ → E}
    (hG : AEStronglyMeasurable G volume) {M : ℝ}
    (hM : 0 ≤ M) (hbound : ∀ p, ‖G p‖ ≤ M) :
    LocallyIntegrable G volume := by
…

theorem OAI.DoublingHilbert.ae_tendsto_average_norm_sub_sq line 29

Source documentation

Lebesgue differentiation for bounded fields.

theorem ae_tendsto_average_norm_sub_sq {G : ℝ × ℝ → E}
    (hG : AEStronglyMeasurable G volume) {M : ℝ}
    (hM : 0 ≤ M) (hbound : ∀ p, ‖G p‖ ≤ M) :
    ∀ᵐ p, Tendsto (fun r : ℝ => ⨍ q in Metric.closedBall p r, ‖G q - G p‖ ^ 2)
      (𝓝[>] 0) (𝓝 0) := by
…

def OAI.DoublingHilbert.sheetColumn line 71
Source documentation
Derivative column, extended by zero off the open sheet domain.
```
def sheetColumn (f : ℝ × ℝ → E) (Ω : Set (ℝ × ℝ)) (v : ℝ × ℝ) : ℝ × ℝ → E :=
…
```
theorem OAI.DoublingHilbert.norm_sheetColumn_le line 75
theorem OAI.DoublingHilbert.aestronglyMeasurable_sheetColumn line 86

theorem OAI.DoublingHilbert.ae_good_sheet_points line 96

Source documentation

Good derivative points have full measure on every sheet.

theorem ae_good_sheet_points {f : ℝ × ℝ → E} {Ω : Set (ℝ × ℝ)}
    (hΩ : IsOpen Ω) {C : NNReal} (hf : LipschitzOnWith C f Ω) (v₁ v₂ : ℝ × ℝ) :
    ∀ᵐ p, p ∈ Ω → DifferentiableAt ℝ f p ∧
      Tendsto (fun r : ℝ => ⨍ q in Metric.closedBall p r,
        ‖sheetColumn f Ω v₁ q - sheetColumn f Ω v₁ p‖ ^ 2)
        (𝓝[>] 0) (𝓝 0) ∧
      Tendsto (fun r : ℝ => ⨍ q in Metric.closedBall p r,
        ‖sheetColumn f Ω v₂ q - sheetColumn f Ω v₂ p‖ ^ 2)
        (𝓝[>] 0) (𝓝 0) := by
…

Mentions: OAI.DoublingHilbert.sheetColumn

def OAI.DoublingHilbert.embeddingSheet line 124
Source documentation
A sheet is the actual embedding on its domain; the arbitrary outside value is zero.
```
def embeddingSheet (f : constructedSet → E) (w : Tuple) (p : Base) : E := by
…
```
Mentions: OAI.DoublingHilbert.constructedSet, OAI.DoublingHilbert.Tuple, OAI.DoublingHilbert.Base
theorem OAI.DoublingHilbert.embeddingSheet_eq line 129
theorem OAI.DoublingHilbert.embeddingSheet_lipschitz line 134
def OAI.DoublingHilbert.goodSheetPoint line 146
theorem OAI.DoublingHilbert.ae_good_embeddingSheet line 157
def OAI.DoublingHilbert.derivativePair line 165
Source documentation
Squared derivative columns, the pairs used in the one fixed compact set.
```
def derivativePair (f : constructedSet → E) (w : Tuple) (p : Base) : ℝ × ℝ :=
…
```
Mentions: OAI.DoublingHilbert.constructedSet, OAI.DoublingHilbert.Tuple, OAI.DoublingHilbert.Base
def OAI.DoublingHilbert.derivativeData line 169
def OAI.DoublingHilbert.derivativeCompact line 172
theorem OAI.DoublingHilbert.derivativePair_bounds line 175
theorem OAI.DoublingHilbert.derivativeCompact_subset line 186
theorem OAI.DoublingHilbert.isCompact_derivativeCompact line 194
theorem OAI.DoublingHilbert.derivativeData_nonempty line 198
theorem OAI.DoublingHilbert.derivativeCompact_nonempty line 203

theorem OAI.DoublingHilbert.exists_lipschitz_extension_finiteDimensional line 216

Source documentation

Finite-dimensional Lipschitz sheet maps have some global Lipschitz extension. Only agreement on the original open domain is used for sharp derivative estimates.

theorem exists_lipschitz_extension_finiteDimensional
    {X E : Type*} [PseudoMetricSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] {f : X → E} {s : Set X} {C : NNReal}
    (hf : LipschitzOnWith C f s) :
    ∃ g : X → E, ∃ L : NNReal, LipschitzWith L g ∧ EqOn f g s := by
…