FixedMass.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem358.FixedMassIntercepts.masses line 15
Source documentation
The actual closed-cell mass vector, without a choice of maximizing selector.
```
def masses (K : Set (E d)) (y : ι → E d) (c : ι → ℝ) : ι → ℝ :=
…
```

theorem OAI.Problem358.FixedMassIntercepts.closedCell_ae_eq_selector line 19

Source documentation

Null ties identify every maximizing selector's fibers with the closed cells.

theorem closedCell_ae_eq_selector {K : Set (E d)} (hK : MeasurableSet K)
    (y : ι → E d) (hy : Function.Injective y) (c : ι → ℝ)
    (k : E d → ι)
    (hk : ∀ x j, ⟪x, y j⟫ + c j ≤ ⟪x, y (k x)⟫ + c (k x)) (i : ι) :
    CellGeometry.closedCell K y c i =ᵐ[uniformMeasure K] {x | k x = i} := by
…

Mentions: OAI.Problem358.CellGeometry.closedCell

theorem OAI.Problem358.FixedMassIntercepts.masses_eq_selector line 36

Source documentation

The selector law and geometric closed-cell masses have exactly the same real masses.

theorem masses_eq_selector {K : Set (E d)} (hK : MeasurableSet K)
    (y : ι → E d) (hy : Function.Injective y) (c : ι → ℝ)
    (k : E d → ι)
    (hk : ∀ x j, ⟪x, y j⟫ + c j ≤ ⟪x, y (k x)⟫ + c (k x)) (i : ι) :
    masses K y c i = (uniformMeasure K).real {x | k x = i} := by
…

Mentions: OAI.Problem358.FixedMassIntercepts.masses

theorem OAI.Problem358.FixedMassIntercepts.existsUnique_normalized line 49
Source documentation
Prescribed positive masses uniquely determine a normalized intercept vector. This is an actual existence and uniqueness result for the geometric cells; it has no cell-differentiability hypothesis.
```
theorem existsUnique_normalized {K : Set (E d)}
    (hK : IsCompact K) (hconv : Convex ℝ K) (hne : (interior K).Nonempty)
    (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
    (y : ι → E d) (hy : Function.Injective y) :
    ∃! c : CellLaplacian.normalizedSpace m, masses K y c = m := by
…
```
Mentions: OAI.Problem358.CellLaplacian.normalizedSpace, OAI.Problem358.FixedMassIntercepts.masses
def OAI.Problem358.FixedMassIntercepts.intercepts line 78
Source documentation
The canonical normalized intercept vector. It is zero on configurations with repeated sites; all uses of the prescribed-mass specification have distinct sites.
```
def intercepts {K : Set (E d)}
    (hK : IsCompact K) (hconv : Convex ℝ K) (hne : (interior K).Nonempty)
    (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
    (y : ι → E d) : CellLaplacian.normalizedSpace m :=
…
```
Mentions: OAI.Problem358.CellLaplacian.normalizedSpace
theorem OAI.Problem358.FixedMassIntercepts.intercepts_spec line 86
theorem OAI.Problem358.FixedMassIntercepts.eq_intercepts line 94
def OAI.Problem358.CellGeometry.normalizedMassMap line 116
Source documentation
The actual closed-cell masses, restricted to normalized intercepts.
```
def normalizedMassMap (K : Set (E d)) (m : ι → ℝ) :
    ((ι → E d) × CellLaplacian.normalizedSpace m) → (ι → ℝ) :=
…
```
Mentions: OAI.Problem358.CellLaplacian.normalizedSpace
theorem OAI.Problem358.CellGeometry.eventually_injective_sites line 121
Source documentation
Distinctness of finitely many sites persists on a neighborhood.
```
theorem eventually_injective_sites {y : ι → E d} (hy : Function.Injective y) :
    ∀ᶠ z in 𝓝 y, Function.Injective z := by
…
```
theorem OAI.Problem358.CellGeometry.sum_normalizedMassMap line 134
Source documentation
The coordinate mass map takes values in probability vectors whenever the sites are distinct. This is derived from the actual closed-cell partition.
```
theorem sum_normalizedMassMap [Nonempty ι] {K : Set (E d)} (hK : IsCompact K)
    (hne : (interior K).Nonempty) (m : ι → ℝ)
    (p : (ι → E d) × CellLaplacian.normalizedSpace m)
    (hy : Function.Injective p.1) :
    ∑ i, normalizedMassMap K m p i = 1 := by
…
```
Mentions: OAI.Problem358.CellLaplacian.normalizedSpace, OAI.Problem358.CellGeometry.normalizedMassMap
theorem OAI.Problem358.CellGeometry.normalizedMassResidual_eq_zero_iff line 154
Source documentation
The normalized mass residual vanishes exactly at the prescribed physical closed-cell masses, without a selector or residual-range assumption.
```
theorem normalizedMassResidual_eq_zero_iff [Nonempty ι] {K : Set (E d)} (hK : IsCompact K)
    (hne : (interior K).Nonempty) (m : ι → ℝ) (hm : ∑ i, m i = 1)
    (p : (ι → E d) × CellLaplacian.normalizedSpace m)
    (hy : Function.Injective p.1) :
    CellLaplacian.massResidual m hm (normalizedMassMap K m) p = 0 ↔
      ∀ i, (uniformMeasure K).real (closedCell K p.1 p.2 i) = m i := by
…
```
Mentions: OAI.Problem358.CellLaplacian.normalizedSpace, OAI.Problem358.CellLaplacian.massResidual, OAI.Problem358.CellGeometry.normalizedMassMap, OAI.Problem358.CellGeometry.closedCell
def OAI.Problem358.CellGeometry.normalizedConfigInclusion line 165
Source documentation
Include the normalization hyperplane into the unrestricted configuration space.
```
def normalizedConfigInclusion (m : ι → ℝ) :
    ((ι → E d) × CellLaplacian.normalizedSpace m) →L[ℝ] ((ι → E d) × (ι → ℝ)) :=
…
```
Mentions: OAI.Problem358.CellLaplacian.normalizedSpace
theorem OAI.Problem358.CellGeometry.normalizedConfigInclusion_apply line 169
theorem OAI.Problem358.CellGeometry.contDiffAt_normalizedMassMap_of_raw line 175
Source documentation
Restrict geometric C¹ regularity on ordinary site/intercept coordinates to the weighted normalization hyperplane used by the implicit function theorem.
```
theorem contDiffAt_normalizedMassMap_of_raw {K : Set (E d)} (m : ι → ℝ)
    (p : (ι → E d) × CellLaplacian.normalizedSpace m)
    (hM : ContDiffAt ℝ 1
      (fun z : (ι → E d) × (ι → ℝ) => fun i =>
        (uniformMeasure K).real (closedCell K z.1 z.2 i))
      (p.1, (p.2 : ι → ℝ))) :
    ContDiffAt ℝ 1 (normalizedMassMap K m) p :=
…
```
Mentions: OAI.Problem358.CellLaplacian.normalizedSpace, OAI.Problem358.CellGeometry.closedCell, OAI.Problem358.CellGeometry.normalizedMassMap

theorem OAI.Problem358.CellGeometry.hasFDerivAt_normalizedMassMap_of_raw line 186

Source documentation

The normalized mass derivative is the unrestricted geometric derivative composed with the actual hyperplane inclusion.

theorem hasFDerivAt_normalizedMassMap_of_raw {K : Set (E d)} (m : ι → ℝ)
    (p : (ι → E d) × CellLaplacian.normalizedSpace m)
    (A : ((ι → E d) × (ι → ℝ)) →L[ℝ] (ι → ℝ))
    (hD : HasFDerivAt
      (fun z : (ι → E d) × (ι → ℝ) => fun i =>
        (uniformMeasure K).real (closedCell K z.1 z.2 i)) A
      (p.1, (p.2 : ι → ℝ))) :
    HasFDerivAt (normalizedMassMap K m) (A ∘L normalizedConfigInclusion m) p := by
…

Mentions: OAI.Problem358.CellLaplacian.normalizedSpace, OAI.Problem358.CellGeometry.closedCell, OAI.Problem358.CellGeometry.normalizedMassMap, OAI.Problem358.CellGeometry.normalizedConfigInclusion

theorem OAI.Problem358.CellLaplacian.normalizedSpace_eq_zero_of_subsingleton line 214
Source documentation
For one site, the weighted normalization hyperplane is the zero space. This uses only the total mass, and does not need positivity or a graph lemma.
```
theorem normalizedSpace_eq_zero_of_subsingleton (m : ι → ℝ)
    (hsum : ∑ i, m i = 1) (q : normalizedSpace m) : q = 0 := by
…
```
Mentions: OAI.Problem358.CellLaplacian.normalizedSpace
theorem OAI.Problem358.CellLaplacian.subsingleton_normalizedSpace line 225
theorem OAI.Problem358.CellGeometry.closedCell_eq_of_subsingleton line 236
Source documentation
A one-site closed affine cell is the entire source set.
```
theorem closedCell_eq_of_subsingleton {d : ℕ} {ι : Type*} [Subsingleton ι]
    (K : Set (E d)) (y : ι → E d) (c : ι → ℝ) (i : ι) :
    closedCell K y c i = K := by
…
```
Mentions: OAI.Problem358.CellGeometry.closedCell

theorem OAI.Problem358.FixedMassIntercepts.intercepts_eq_zero_of_subsingleton line 254

Source documentation

The actual globally selected normalized intercept is zero for a one-site target.

@[simp] theorem intercepts_eq_zero_of_subsingleton {K : Set (E d)}
    (hK : IsCompact K) (hconv : Convex ℝ K) (hne : (interior K).Nonempty)
    (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
    (y : ι → E d) : intercepts hK hconv hne m hm hsum y = 0 :=
…

Mentions: OAI.Problem358.FixedMassIntercepts.intercepts

theorem OAI.Problem358.FixedMassIntercepts.contDiff_intercepts_of_subsingleton line 261

Source documentation

The one-site intercept selection is smooth independently of any cell calculus.

theorem contDiff_intercepts_of_subsingleton {K : Set (E d)}
    (hK : IsCompact K) (hconv : Convex ℝ K) (hne : (interior K).Nonempty)
    (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
    (n : ℕ∞ω) : ContDiff ℝ n (intercepts hK hconv hne m hm hsum) := by
…

Mentions: OAI.Problem358.FixedMassIntercepts.intercepts

theorem OAI.Problem358.FixedMassIntercepts.hasDerivAt_intercepts_path_of_subsingleton line 274

Source documentation

Even an arbitrary site path gives a constant normalized intercept path if there is only one site. In particular its intercept energy is exactly zero.

theorem hasDerivAt_intercepts_path_of_subsingleton {K : Set (E d)}
    (hK : IsCompact K) (hconv : Convex ℝ K) (hne : (interior K).Nonempty)
    (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
    (y : ℝ → ι → E d) (t : ℝ) :
    HasDerivAt (fun s => intercepts hK hconv hne m hm hsum (y s)) 0 t := by
…

Mentions: OAI.Problem358.FixedMassIntercepts.intercepts

theorem OAI.Problem358.FixedMassIntercepts.contDiffAt_intercepts_of_massDifferential line 301

Source documentation

The actual canonical prescribed-mass intercepts are C¹ at each distinct-site configuration where the geometric mass map is C¹ with its connected cell Laplacian as intercept derivative. Neither continuity nor uniqueness of a chosen branch is assumed: both are supplied by the geometric closed-cell construction.

theorem contDiffAt_intercepts_of_massDifferential {K : Set (E d)}
    (hK : IsCompact K) (hconv : Convex ℝ K) (hne : (interior K).Nonempty)
    (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
    (y : ι → E d) (hy : Function.Injective y)
    (g : ι → ι → ℝ) (hsym : ∀ i j, g i j = g j i)
    (hnonneg : ∀ i j, 0 ≤ g i j) (G : SimpleGraph ι)
    (hG : G.Connected) (hpos : ∀ i j, G.Adj i j → 0 < g i j)
    (A : ((ι → E d) × CellLaplacian.normalizedSpace m) →L[ℝ] (ι → ℝ))
    (hM : ContDiffAt ℝ 1 (CellGeometry.normalizedMassMap K m)
      (y, intercepts hK hconv hne m hm hsum y))
    (hD : HasFDerivAt (CellGeometry.normalizedMassMap K m) A
      (y, intercepts hK hconv hne m hm hsum y))
…

Mentions: OAI.Problem358.CellLaplacian.normalizedSpace, OAI.Problem358.CellGeometry.normalizedMassMap, OAI.Problem358.FixedMassIntercepts.intercepts

theorem OAI.Problem358.FixedMassIntercepts.hasDerivAt_intercepts_comp_and_mass_constraint line 339

Source documentation

Along a differentiable site path, the actual canonical intercept derivative satisfies the differentiated fixed-mass constraint. Its weighted mean vanishes because it belongs to the normalization subspace.

theorem hasDerivAt_intercepts_comp_and_mass_constraint {K : Set (E d)}
    (hK : IsCompact K) (hconv : Convex ℝ K) (hne : (interior K).Nonempty)
    (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
    (Y : ℝ → (ι → E d)) (v : ι → E d) (t : ℝ)
    (hY : HasDerivAt Y v t) (hy : Function.Injective (Y t))
    (hs : DifferentiableAt ℝ (intercepts hK hconv hne m hm hsum) (Y t))
    (A : ((ι → E d) × CellLaplacian.normalizedSpace m) →L[ℝ] (ι → ℝ))
    (hD : HasFDerivAt (CellGeometry.normalizedMassMap K m) A
      (Y t, intercepts hK hconv hne m hm hsum (Y t))) :
    let c := fun q => intercepts hK hconv hne m hm hsum (Y q)
…

Mentions: OAI.Problem358.FixedMassIntercepts.intercepts, OAI.Problem358.CellLaplacian.normalizedSpace, OAI.Problem358.CellGeometry.normalizedMassMap

theorem OAI.Problem358.FixedMassIntercepts.laplacian_intercepts_comp_deriv line 364

Source documentation

Coordinate form of the fixed-mass derivative equation. This is the actual constraint consumed by the symmetric flux / intercept energy calculation.

theorem laplacian_intercepts_comp_deriv {K : Set (E d)}
    (hK : IsCompact K) (hconv : Convex ℝ K) (hne : (interior K).Nonempty)
    (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
    (Y : ℝ → (ι → E d)) (v : ι → E d) (t : ℝ)
    (hY : HasDerivAt Y v t) (hy : Function.Injective (Y t))
    (hs : DifferentiableAt ℝ (intercepts hK hconv hne m hm hsum) (Y t))
    (A : ((ι → E d) × CellLaplacian.normalizedSpace m) →L[ℝ] (ι → ℝ))
    (hD : HasFDerivAt (CellGeometry.normalizedMassMap K m) A
      (Y t, intercepts hK hconv hne m hm hsum (Y t)))
    (g : ι → ι → ℝ)
    (hA : ∀ q : CellLaplacian.normalizedSpace m, A (0, q) = CellLaplacian.apply g q) :
    CellLaplacian.apply g
…

Mentions: OAI.Problem358.FixedMassIntercepts.intercepts, OAI.Problem358.CellLaplacian.normalizedSpace, OAI.Problem358.CellGeometry.normalizedMassMap, OAI.Problem358.CellLaplacian.apply