LineDerivative.lean`

30 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem358.hasFDerivAt_of_local_lipschitz_lineDeriv line 18
Source documentation
For a locally Lipschitz real function, a linear family of genuine line derivatives is already its full Fréchet derivative. This local form does not require an artificial global Lipschitz bound on moving-cell parameters.
```
theorem hasFDerivAt_of_local_lipschitz_lineDeriv
    {f : E → ℝ} {x : E} {L : E →L[ℝ] ℝ} {S : Set E} {C : ℝ≥0}
    (hS : S ∈ 𝓝 x) (hf : LipschitzOnWith C f S)
    (hline : ∀ v, HasLineDerivAt ℝ f (L v) x v) :
    HasFDerivAt f L x := by
…
```

theorem OAI.Problem358.contDiffOn_one_of_local_lipschitz_lineDeriv line 36

Source documentation

A continuous field of linear line derivatives for a locally Lipschitz real function proves genuine C¹ regularity on an open parameter domain.

theorem contDiffOn_one_of_local_lipschitz_lineDeriv
    {f : E → ℝ} {U : Set E} {L : E → E →L[ℝ] ℝ}
    (hU : IsOpen U) (hL : ContinuousOn L U)
    (hlip : ∀ x ∈ U, ∃ (S : Set E) (C : ℝ≥0), S ∈ 𝓝 x ∧ LipschitzOnWith C f S)
    (hline : ∀ x ∈ U, ∀ v, HasLineDerivAt ℝ f (L x v) x v) :
    ContDiffOn ℝ 1 f U := by
…

theorem OAI.Problem358.hasFDerivAt_pi_of_local_lipschitz_lineDeriv line 51

Source documentation

Finite-vector version, suited to the full vector of cell masses.

theorem hasFDerivAt_pi_of_local_lipschitz_lineDeriv
    {ι : Type*} [Fintype ι] {f : E → ι → ℝ} {x : E}
    {L : E →L[ℝ] (ι → ℝ)} {S : Set E} {C : ℝ≥0}
    (hS : S ∈ 𝓝 x) (hf : LipschitzOnWith C f S)
    (hline : ∀ v, HasLineDerivAt ℝ f (L v) x v) :
    HasFDerivAt f L x := by
…

theorem OAI.Problem358.contDiffOn_one_pi_of_local_lipschitz_lineDeriv line 70

Source documentation

The locally Lipschitz finite-vector function is C¹ when its linear line-derivative field is continuous.

theorem contDiffOn_one_pi_of_local_lipschitz_lineDeriv
    {ι : Type*} [Fintype ι] {f : E → ι → ℝ} {U : Set E}
    {L : E → E →L[ℝ] (ι → ℝ)}
    (hU : IsOpen U) (hL : ContinuousOn L U)
    (hlip : ∀ x ∈ U, ∃ (S : Set E) (C : ℝ≥0), S ∈ 𝓝 x ∧ LipschitzOnWith C f S)
    (hline : ∀ x ∈ U, ∀ v, HasLineDerivAt ℝ f (L x v) x v) :
    ContDiffOn ℝ 1 f U := by
…

lemma OAI.Problem358.hasDerivAt_line_of_hasLineDerivAt line 98
lemma OAI.Problem358.norm_sub_le_of_continuous_linear_line_derivatives line 111
lemma OAI.Problem358.hasStrictFDerivAt_of_continuousAt_lineDeriv line 139
Source documentation
A continuous field of bounded linear directional derivatives implies strict Fréchet differentiability. No completeness or finite-dimensional hypothesis is needed.
```
lemma hasStrictFDerivAt_of_continuousAt_lineDeriv
    {f : V → F} {D : V → V →L[ℝ] F} {x : V}
    (hD : ∀ᶠ y in 𝓝 x, ∀ v, HasLineDerivAt ℝ f (D y v) y v)
    (hc : ContinuousAt D x) : HasStrictFDerivAt f (D x) x := by
…
```

lemma OAI.Problem358.contDiffOn_one_of_continuousOn_lineDeriv line 163

Source documentation

On an open set, a continuous field of bounded linear line derivatives gives C¹.

lemma contDiffOn_one_of_continuousOn_lineDeriv
    {s : Set V} (hs : IsOpen s) {f : V → F} {D : V → V →L[ℝ] F}
    (hD : ∀ x ∈ s, ∀ v, HasLineDerivAt ℝ f (D x v) x v)
    (hc : ContinuousOn D s) : ContDiffOn ℝ 1 f s := by
…

def OAI.Problem358.FaceDerivative.linearMap line 192
Source documentation
A face contribution to the mass derivative, with its scalar and vector moments made explicit. The input is the site and intercept variation (v,r).
```
def linearMap (A M : ℝ) (B : V) : V × ℝ →L[ℝ] ℝ :=
…
```
lemma OAI.Problem358.FaceDerivative.linearMap_apply line 196

theorem OAI.Problem358.FaceDerivative.continuousAt_linearMap line 204

Source documentation

Operator-norm continuity of the face derivative follows solely from continuity of its nonzero normal scale, face mass, and vector face moment.

theorem continuousAt_linearMap {P : Type*} [TopologicalSpace P]
    {A M : P → ℝ} {B : P → V} {p : P}
    (hA : ContinuousAt A p) (hM : ContinuousAt M p) (hB : ContinuousAt B p)
    (hzero : A p ≠ 0) :
    ContinuousAt (fun q => linearMap (A q) (M q) (B q)) p := by
…

Mentions: OAI.Problem358.FaceDerivative.linearMap

theorem OAI.Problem358.FaceDerivative.continuous_linearMap line 215

Source documentation

Globally continuous coefficient fields give a continuous derivative field.

theorem continuous_linearMap {P : Type*} [TopologicalSpace P]
    {A M : P → ℝ} {B : P → V}
    (hA : Continuous A) (hM : Continuous M) (hB : Continuous B)
    (hzero : ∀ p, A p ≠ 0) :
    Continuous (fun q => linearMap (A q) (M q) (B q)) := by
…

Mentions: OAI.Problem358.FaceDerivative.linearMap

theorem OAI.Problem358.FaceDerivative.continuousOn_linearMap line 225

Source documentation

The same coefficient criterion on an arbitrary configuration domain.

theorem continuousOn_linearMap {P : Type*} [TopologicalSpace P]
    {S : Set P} {A M : P → ℝ} {B : P → V}
    (hA : ContinuousOn A S) (hM : ContinuousOn M S) (hB : ContinuousOn B S)
    (hzero : ∀ p ∈ S, A p ≠ 0) :
    ContinuousOn (fun q => linearMap (A q) (M q) (B q)) S := by
…

Mentions: OAI.Problem358.FaceDerivative.linearMap

def OAI.Problem358.FaceDerivative.pairVariation line 239
Source documentation
Extract the difference of the two site and intercept perturbations.
```
def pairVariation (i j : ι) : ((ι → V) × (ι → ℝ)) →L[ℝ] V × ℝ :=
…
```
lemma OAI.Problem358.FaceDerivative.pairVariation_apply line 247
def OAI.Problem358.FaceDerivative.cellLinearMap line 252
Source documentation
Face derivatives assembled into one continuous linear cell-mass derivative. The index set can exclude the diagonal or any inactive faces.
```
def cellLinearMap (J : Finset ι) (i : ι) (A M : ι → ℝ) (B : ι → V) :
    ((ι → V) × (ι → ℝ)) →L[ℝ] ℝ :=
…
```
lemma OAI.Problem358.FaceDerivative.cellLinearMap_apply line 256

theorem OAI.Problem358.FaceDerivative.continuousOn_cellLinearMap line 265

Source documentation

A finite cell derivative field is continuous in operator norm whenever all its face scales and scalar/vector moments are continuous.

theorem continuousOn_cellLinearMap [Fintype ι]
    {P : Type*} [TopologicalSpace P] {S : Set P}
    (J : Finset ι) (i : ι) {A M : P → ι → ℝ} {B : P → ι → V}
    (hA : ∀ j ∈ J, ContinuousOn (fun p => A p j) S)
    (hM : ∀ j ∈ J, ContinuousOn (fun p => M p j) S)
    (hB : ∀ j ∈ J, ContinuousOn (fun p => B p j) S)
    (hzero : ∀ p ∈ S, ∀ j ∈ J, A p j ≠ 0) :
    ContinuousOn (fun p => cellLinearMap J i (A p) (M p) (B p)) S := by
…

Mentions: OAI.Problem358.FaceDerivative.cellLinearMap

lemma OAI.Problem358.FaceDerivative.integrable_speed_trace line 286
Source documentation
Integrability of a moving-face speed times its trace follows from the two natural face-moment integrability hypotheses.
```
lemma integrable_speed_trace (hτ : Integrable τ μ)
    (hz : Integrable (fun x => τ x • z x) μ) (A r : ℝ) (v : V) :
    Integrable (fun x => ((r + ⟪v, z x⟫_ℝ) / A) * τ x) μ := by
…
```

theorem OAI.Problem358.FaceDerivative.integral_speed_trace line 300

Source documentation

The genuine face integral is linear in the site and intercept variation.

theorem integral_speed_trace (hτ : Integrable τ μ)
    (hz : Integrable (fun x => τ x • z x) μ) (A r : ℝ) (v : V) :
    (∫ x, ((r + ⟪v, z x⟫_ℝ) / A) * τ x ∂μ) =
      (r / A) * (∫ x, τ x ∂μ) + (1 / A) * ⟪v, ∫ x, τ x • z x ∂μ⟫_ℝ := by
…

theorem OAI.Problem358.FaceDerivative.integral_speed_trace_eq_linearMap line 313

Source documentation

The integral formula is exactly evaluation of the continuous linear face map.

theorem integral_speed_trace_eq_linearMap (hτ : Integrable τ μ)
    (hz : Integrable (fun x => τ x • z x) μ) (A r : ℝ) (v : V) :
    (∫ x, ((r + ⟪v, z x⟫_ℝ) / A) * τ x ∂μ) =
      linearMap A (∫ x, τ x ∂μ) (∫ x, τ x • z x ∂μ) (v, r) := by
…

Mentions: OAI.Problem358.FaceDerivative.linearMap

theorem OAI.Problem358.FaceDerivative.contDiffOn_one_of_local_line_fields line 337

Source documentation

Local continuous line-derivative fields patch to C¹ without choosing a global normal chart. Each field need only be continuous at its own centre.

theorem contDiffOn_one_of_local_line_fields
    {S : Set W} (hS : IsOpen S) {f : W → F}
    (hlocal : ∀ x ∈ S, ∃ D : W → W →L[ℝ] F,
      ContinuousAt D x ∧
      ∀ᶠ y in 𝓝 x, ∀ v, HasLineDerivAt ℝ f (D y v) y v) :
    ContDiffOn ℝ 1 f S := by
…

theorem OAI.Problem358.FaceDerivative.hasLineDerivAt_of_cell_formula line 367

Source documentation

The scalar line formula of the cell calculus is a bounded linear directional derivative, with exactly the site/intercept order used by closedCell.

theorem hasLineDerivAt_of_cell_formula
    {f : ((ι → V) × (ι → ℝ)) → ℝ} {p : (ι → V) × (ι → ℝ)}
    (J : Finset ι) (i : ι) (A M : ι → ℝ) (B : ι → V)
    (hderiv : ∀ (v : ι → V) (r : ι → ℝ),
      HasDerivAt (fun t : ℝ => f (p + t • (v, r)))
        (∑ j ∈ J, (((r i - r j) / A j) * M j +
          (1 / A j) * ⟪v i - v j, B j⟫_ℝ)) 0) :
    ∀ w, HasLineDerivAt ℝ f (cellLinearMap J i A M B w) p w := by
…

Mentions: OAI.Problem358.FaceDerivative.cellLinearMap

theorem OAI.Problem358.FaceDerivative.hasStrictFDerivAt_of_local_cell_formula line 381

Source documentation

A local face chart need only provide coefficient continuity at its centre. The formulas must hold at nearby configurations, but their coefficients need not be defined by any global choice of hyperplane coordinates.

theorem hasStrictFDerivAt_of_local_cell_formula
    {f : ((ι → V) × (ι → ℝ)) → ℝ}
    (J : Finset ι) (i : ι)
    {A M : ((ι → V) × (ι → ℝ)) → ι → ℝ}
    {B : ((ι → V) × (ι → ℝ)) → ι → V}
    {p : (ι → V) × (ι → ℝ)}
    (hA : ∀ j ∈ J, ContinuousAt (fun q => A q j) p)
    (hM : ∀ j ∈ J, ContinuousAt (fun q => M q j) p)
    (hB : ∀ j ∈ J, ContinuousAt (fun q => B q j) p)
    (hzero : ∀ j ∈ J, A p j ≠ 0)
    (hderiv : ∀ᶠ q in 𝓝 p, ∀ (v : ι → V) (r : ι → ℝ),
      HasDerivAt (fun t : ℝ => f (q + t • (v, r)))
…

theorem OAI.Problem358.FaceDerivative.hasStrictFDerivAt_of_cell_formula line 409

Source documentation

Continuous scalar and vector face coefficients upgrade the actual line derivative formula to a strict Fréchet derivative. The domain may be any open set of admissible configurations; no global chart is required.

theorem hasStrictFDerivAt_of_cell_formula
    {S : Set ((ι → V) × (ι → ℝ))} (hS : IsOpen S)
    {f : ((ι → V) × (ι → ℝ)) → ℝ}
    (J : Finset ι) (i : ι)
    {A M : ((ι → V) × (ι → ℝ)) → ι → ℝ}
    {B : ((ι → V) × (ι → ℝ)) → ι → V}
    (hA : ∀ j ∈ J, ContinuousOn (fun p => A p j) S)
    (hM : ∀ j ∈ J, ContinuousOn (fun p => M p j) S)
    (hB : ∀ j ∈ J, ContinuousOn (fun p => B p j) S)
    (hzero : ∀ p ∈ S, ∀ j ∈ J, A p j ≠ 0)
    (hderiv : ∀ p ∈ S, ∀ (v : ι → V) (r : ι → ℝ),
      HasDerivAt (fun t : ℝ => f (p + t • (v, r)))
…

theorem OAI.Problem358.FaceDerivative.contDiffOn_one_of_cell_formula line 435

Source documentation

The joint C¹ conclusion needed before applying the normalized cell implicit function theorem. All geometry is confined to the scalar line formula and the continuous face coefficients.

theorem contDiffOn_one_of_cell_formula
    {S : Set ((ι → V) × (ι → ℝ))} (hS : IsOpen S)
    {f : ((ι → V) × (ι → ℝ)) → ℝ}
    (J : Finset ι) (i : ι)
    {A M : ((ι → V) × (ι → ℝ)) → ι → ℝ}
    {B : ((ι → V) × (ι → ℝ)) → ι → V}
    (hA : ∀ j ∈ J, ContinuousOn (fun p => A p j) S)
    (hM : ∀ j ∈ J, ContinuousOn (fun p => M p j) S)
    (hB : ∀ j ∈ J, ContinuousOn (fun p => B p j) S)
    (hzero : ∀ p ∈ S, ∀ j ∈ J, A p j ≠ 0)
    (hderiv : ∀ p ∈ S, ∀ (v : ι → V) (r : ι → ℝ),
      HasDerivAt (fun t : ℝ => f (p + t • (v, r)))
…

theorem OAI.Problem358.FaceDerivative.sum_integral_speed_trace_eq_cellLinearMap line 462

Source documentation

Convert the actual finite sum of moving-face integrals to the bounded linear cell derivative. Each face may have its own intrinsic parameter space.

theorem sum_integral_speed_trace_eq_cellLinearMap
    (J : Finset ι) (i : ι) (μ : ∀ j, Measure (X j))
    (z : ∀ j, X j → V) (τ : ∀ j, X j → ℝ)
    (hτ : ∀ j ∈ J, Integrable (τ j) (μ j))
    (hz : ∀ j ∈ J, Integrable (fun x => τ j x • z j x) (μ j))
    (A : ι → ℝ) (v : ι → V) (r : ι → ℝ) :
    (∑ j ∈ J, ∫ x, ((r i - r j + ⟪v i - v j, z j x⟫_ℝ) / A j) *
      τ j x ∂μ j) =
      cellLinearMap J i A (fun j => ∫ x, τ j x ∂μ j)
        (fun j => ∫ x, τ j x • z j x ∂μ j) (v, r) := by
…

Mentions: OAI.Problem358.FaceDerivative.cellLinearMap

theorem OAI.Problem358.FaceDerivative.hasStrictFDerivAt_cells line 482

Source documentation

Simultaneous strict differentiation of a finite family of cell quantities. No extra operator-continuity argument is needed after the scalar quantities have been treated.

theorem hasStrictFDerivAt_cells
    {κ : Type*} [Fintype κ]
    {f : ((ι → V) × (ι → ℝ)) → κ → ℝ}
    {D : κ → ((ι → V) × (ι → ℝ)) →L[ℝ] ℝ}
    {p : (ι → V) × (ι → ℝ)}
    (h : ∀ k, HasStrictFDerivAt (fun q => f q k) (D k) p) :
    HasStrictFDerivAt f (ContinuousLinearMap.pi D) p :=
…

theorem OAI.Problem358.FaceDerivative.continuousAt_normalized_faceMoment_of_coordinates line 504

Source documentation

In finite-dimensional Euclidean space, scalar coordinate face integrals control the vector face moment, including its transverse normalization.

theorem continuousAt_normalized_faceMoment_of_coordinates
    {d : ℕ} {P X : Type*} [TopologicalSpace P] [MeasurableSpace X]
    {μ : Measure X} {a : P → ℝ} {τ : P → X → ℝ} {z : P → X → E d}
    {p : P}
    (hint : ∀ q, Integrable (fun x => τ q x • z q x) μ)
    (hcoord : ∀ k : Fin d, ContinuousAt
      (fun q => (∫ x, τ q x * z q x k ∂μ) / a q) p) :
    ContinuousAt (fun q => (a q)⁻¹ • ∫ x, τ q x • z q x ∂μ) p := by
…

theorem OAI.Problem358.FaceDerivative.cellLinearMap_normalize line 531
Source documentation
Absorb the transverse normal scale into the scalar and vector coefficients. The equality remains valid for the totalized zero denominator.
```
theorem cellLinearMap_normalize (J : Finset ι) (i : ι)
    (A M : ι → ℝ) (B : ι → V) :
    cellLinearMap J i A M B =
      cellLinearMap J i (fun _ => 1) (fun j => M j / A j)
        (fun j => (A j)⁻¹ • B j) := by
…
```
Mentions: OAI.Problem358.FaceDerivative.cellLinearMap