MassDerivative.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The actual normalized cell-mass line derivative with canonical coefficients.

theorem OAI.Problem358.CellGeometry.hasDerivAt_uniformMass_line line 19

Source documentation

Compact convex positive-cell geometry alone gives the normalized mass derivative. The auxiliary interior tie points are chosen internally.

theorem hasDerivAt_uniformMass_line
    {ρ : Measure (E d)} (hρ : ρ ≪ volume)
    {K : Set (E d)} (hK : IsCompact K) (hconv : Convex ℝ K)
    (y v : ι → E d) (c r : ι → ℝ) (hy : Function.Injective y)
    (hpos : ∀ k, ρ (closedCell K y c k) ≠ 0) (i : ι) :
    HasDerivAt (fun t : ℝ => (uniformMeasure K).real
      (closedCell K (fun j => y j + t • v j) (fun j => c j + t * r j) i))
      (∑ j, (
        (IntrinsicSurface.interfaceMeasure (y i) (y j) (c i) (c j)
          (closedCell K y c i ∩ closedCell K y c j)).toReal /
            ((volume K).toReal * ‖y i - y j‖) * (r i - r j) +
          ⟪faceMoment K y c i j, v i - v j⟫)) 0 := by
…

Mentions: OAI.Problem358.CellGeometry.closedCell, OAI.Problem358.IntrinsicSurface.interfaceMeasure, OAI.Problem358.CellGeometry.faceMoment

theorem OAI.Problem358.PositiveCellFullDerivative.normalized_faceVariation_coordinate_stationary line 83

Source documentation

The stationary coordinate face derivative has exactly the canonical vector coefficient and source-volume normalization.

theorem normalized_faceVariation_coordinate_stationary
    {d : ℕ} {ι : Type*} [Fintype ι] [DecidableEq ι]
    {K : Set (E d)} (hK : IsCompact K) (y : ι → E d) (c q : ι → ℝ)
    {i j : ι} (hy : y i ≠ y j) {z : E d}
    (htie : ⟪z, y i⟫_ℝ + c i = ⟪z, y j⟫_ℝ + c j) (k : Fin d) :
    (volume K).toReal⁻¹ * faceVariation K y (fun _ => 0) c q (fun x => x k) i j z =
      (q i - q j) * faceMoment K y c i j k := by
…

Mentions: OAI.Problem358.PositiveCellFullDerivative.faceVariation

theorem OAI.Problem358.PositiveCellFullDerivative.hasDerivAt_uniform_closedCell_moment_stationary line 106

Source documentation

Actual stationary-site moment differential with the canonical intrinsic face moments. No directional derivative or face regularity premise remains.

theorem hasDerivAt_uniform_closedCell_moment_stationary
    {d : ℕ} {ι : Type*} [Fintype ι] [DecidableEq ι]
    {ρ : Measure (E d)} (hρ : ρ ≪ volume)
    {K : Set (E d)} (hK : IsCompact K) (hconv : Convex ℝ K)
    (y : ι → E d) (c q : ι → ℝ) (hy : Function.Injective y)
    (hpos : ∀ k, ρ (closedCell K y c k) ≠ 0) (i : ι) :
    HasDerivAt (fun t : ℝ => ∫ x in
      closedCell K y (fun j => c j + t * q j) i, x ∂uniformMeasure K)
      (∑ j, (q i - q j) • faceMoment K y c i j) 0 := by
…

def OAI.Problem358.CellGeometry.massLinearMap line 162
Source documentation
The actual mass derivative as a bounded linear map in sites and intercepts.
```
def massLinearMap (K : Set (E d)) (y : ι → E d) (c : ι → ℝ) (i : ι) :
    ((ι → E d) × (ι → ℝ)) →L[ℝ] ℝ :=
…
```
theorem OAI.Problem358.CellGeometry.massLinearMap_apply line 168

theorem OAI.Problem358.CellGeometry.hasLineDerivAt_uniformMass line 179

Source documentation

Geometry supplies all directional derivatives of the true uniform masses.

theorem hasLineDerivAt_uniformMass
    {ρ : Measure (E d)} (hρ : ρ ≪ volume)
    {K : Set (E d)} (hK : IsCompact K) (hconv : Convex ℝ K)
    (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
    (hpos : ∀ k, ρ (closedCell K y c k) ≠ 0) (i : ι)
    (w : (ι → E d) × (ι → ℝ)) :
    HasLineDerivAt ℝ (fun p : (ι → E d) × (ι → ℝ) =>
      (uniformMeasure K).real (closedCell K p.1 p.2 i))
      (massLinearMap K y c i w) (y, c) w := by
…

Mentions: OAI.Problem358.CellGeometry.closedCell, OAI.Problem358.CellGeometry.massLinearMap

theorem OAI.Problem358.CellGeometry.continuousAt_massLinearMap line 195

Source documentation

Continuity of the true mass derivative in operator norm.

theorem continuousAt_massLinearMap
    {ρ : Measure (E d)} (hρ : ρ ≪ volume)
    {K : Set (E d)} (hK : IsCompact K) (hconv : Convex ℝ K)
    (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
    (hpos : ∀ k, ρ (closedCell K y c k) ≠ 0) (i : ι) :
    ContinuousAt (fun p : (ι → E d) × (ι → ℝ) =>
      massLinearMap K p.1 p.2 i) (y, c) := by
…

Mentions: OAI.Problem358.CellGeometry.closedCell, OAI.Problem358.CellGeometry.massLinearMap

def OAI.Problem358.CellGeometry.positiveMassConfigurations line 211
Source documentation
Distinct configurations with strictly positive actual cell masses.
```
def positiveMassConfigurations (K : Set (E d)) : Set ((ι → E d) × (ι → ℝ)) :=
…
```
theorem OAI.Problem358.CellGeometry.nonzero_cellMass_of_positive line 215
theorem OAI.Problem358.CellGeometry.contDiffOn_uniformMassMap line 224
Source documentation
Joint C¹ regularity of the entire genuine normalized mass map, on its open positive-cell locus. All face calculus hypotheses have been discharged.
```
theorem contDiffOn_uniformMassMap
    {K : Set (E d)} (hK : IsCompact K) (hconv : Convex ℝ K) :
    ContDiffOn ℝ 1 (fun p : (ι → E d) × (ι → ℝ) =>
      fun i => (uniformMeasure K).real (closedCell K p.1 p.2 i))
      (positiveMassConfigurations K) := by
…
```
Mentions: OAI.Problem358.CellGeometry.closedCell, OAI.Problem358.CellGeometry.positiveMassConfigurations

theorem OAI.Problem358.CellGeometry.contDiffAt_uniformMassMap line 242

Source documentation

The pointwise C¹ form consumed by normalized implicit-function arguments.

theorem contDiffAt_uniformMassMap
    {K : Set (E d)} (hK : IsCompact K) (hconv : Convex ℝ K)
    (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
    (hpos : ∀ i, 0 < (uniformMeasure K).real (closedCell K y c i)) :
    ContDiffAt ℝ 1 (fun p : (ι → E d) × (ι → ℝ) =>
      fun i => (uniformMeasure K).real (closedCell K p.1 p.2 i)) (y, c) :=
…

Mentions: OAI.Problem358.CellGeometry.closedCell