CellEnergy.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem358.fixed_mass_intercept_energy_le line 18

Source documentation

The connected mass Jacobian and the stationary moment estimate control the intercept velocity. The auxiliary solution of the mass equation is constructed here; in particular no quantitative inverse-Jacobian bound is assumed.

theorem fixed_mass_intercept_energy_le
    (g : ι → ι → ℝ) (b : ι → ι → F)
    (hg : ∀ i j, g i j = g j i) (hb : ∀ i j, b i j = b j i)
    (hg0 : ∀ i j, 0 ≤ g i j) (G : SimpleGraph ι)
    (hG : G.Connected) (hpos : ∀ i j, G.Adj i j → 0 < g i j)
    (m r : ι → ℝ) (v : ι → F) {k w : ℝ}
    (hm : ∀ i, 0 < m i) (hk : 0 ≤ k)
    (hmean : ∑ i, m i * r i = 0)
    (hfixed : ∀ i, CellLaplacian.apply g r i +
      (∑ j, inner ℝ (b i j) (v i - v j)) = 0)
    (hspeed : (∑ i, m i * ‖v i‖ ^ 2) ≤ w ^ 2)
    (hmoment : ∀ q : ι → ℝ,
…

Mentions: OAI.Problem358.CellLaplacian.apply

theorem OAI.Problem358.fixed_mass_intercept_energy_le_162 line 59

Source documentation

The exact universal moment constant yields the energy input used by the finite affine potential-path estimate.

theorem fixed_mass_intercept_energy_le_162
    (g : ι → ι → ℝ) (b : ι → ι → F)
    (hg : ∀ i j, g i j = g j i) (hb : ∀ i j, b i j = b j i)
    (hg0 : ∀ i j, 0 ≤ g i j) (G : SimpleGraph ι)
    (hG : G.Connected) (hpos : ∀ i j, G.Adj i j → 0 < g i j)
    (m r : ι → ℝ) (v : ι → F) {R w : ℝ}
    (hm : ∀ i, 0 < m i) (hmean : ∑ i, m i * r i = 0)
    (hfixed : ∀ i, CellLaplacian.apply g r i +
      (∑ j, inner ℝ (b i j) (v i - v j)) = 0)
    (hspeed : (∑ i, m i * ‖v i‖ ^ 2) ≤ w ^ 2)
    (hmoment : ∀ q : ι → ℝ,
      (∑ i, ‖∑ j, (q i - q j) • b i j‖ ^ 2 / m i) ≤
…

Mentions: OAI.Problem358.CellLaplacian.apply

def OAI.Problem358.CellLaplacian.siteFlux line 84
Source documentation
The mass variation caused by motion of the sites, in face coordinates.
```
def siteFlux (b : ι → ι → V) (v : ι → V) (i : ι) : ℝ :=
…
```
theorem OAI.Problem358.CellLaplacian.sum_siteFlux line 88
Source documentation
Symmetric face moments conserve total mass under every site motion.
```
theorem sum_siteFlux (b : ι → ι → V) (hb : ∀ i j, b i j = b j i)
    (v : ι → V) : ∑ i, siteFlux b v i = 0 := by
…
```
Mentions: OAI.Problem358.CellLaplacian.siteFlux
theorem OAI.Problem358.CellLaplacian.zeroSumProjection_siteFlux line 94
Source documentation
Projection onto the zero-sum mass space does not change the site flux.
```
theorem zeroSumProjection_siteFlux (m : ι → ℝ) (hm : ∑ i, m i = 1)
    (b : ι → ι → V) (hb : ∀ i j, b i j = b j i) (v : ι → V) :
    (zeroSumProjection m hm (siteFlux b v) : ι → ℝ) = siteFlux b v :=
…
```
Mentions: OAI.Problem358.CellLaplacian.zeroSumProjection, OAI.Problem358.CellLaplacian.siteFlux

theorem OAI.Problem358.CellLaplacian.massResidual_site_derivative line 104

Source documentation

The site partial derivative of the projected mass residual is exactly the physical face flux. This removes the projection introduced to type the implicit-function equation in its zero-sum codomain.

theorem massResidual_site_derivative
    (m : ι → ℝ) (hm : ∑ i, m i = 1)
    {M : P × normalizedSpace m → (ι → ℝ)} {x : P × normalizedSpace m}
    {A : P × normalizedSpace m →L[ℝ] (ι → ℝ)}
    (hM : HasFDerivAt M A x)
    (b : ι → ι → V) (hb : ∀ i j, b i j = b j i)
    (v : ι → V) (p : P) (hsite : A (p, 0) = siteFlux b v) :
    (fderiv ℝ (massResidual m hm M) x (p, 0) : ι → ℝ) = siteFlux b v := by
…

Mentions: OAI.Problem358.CellLaplacian.normalizedSpace, OAI.Problem358.CellLaplacian.siteFlux, OAI.Problem358.CellLaplacian.massResidual

theorem OAI.Problem358.CellLaplacian.deriv_normalized_solution_energy_le line 135

Source documentation

The actual derivative of the normalized implicit intercept branch obeys the uniform weighted energy bound. The site partial derivative is identified by the face formula; no derivative, normalization, or mass-equation condition on the selected branch is assumed separately.

theorem deriv_normalized_solution_energy_le
    {n : ℕ∞ω} (hn : n ≠ 0)
    (g : ι → ι → ℝ) (b : ι → ι → V)
    (hg : ∀ i j, g i j = g j i) (hb : ∀ i j, b i j = b j i)
    (hg0 : ∀ i j, 0 ≤ g i j) (G : SimpleGraph ι)
    (hG : G.Connected) (hpos : ∀ i j, G.Adj i j → 0 < g i j)
    (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hmsum : ∑ i, m i = 1)
    (F : ℝ × normalizedSpace m → normalizedSpace (fun _ : ι => 1))
    (s : ℝ → normalizedSpace m) (t : ℝ)
    (hF : ContDiffAt ℝ n F (t, s t))
    (hA : fderiv ℝ F (t, s t) ∘L ContinuousLinearMap.inr ℝ ℝ (normalizedSpace m) =
      (normalizedEquiv g hg hg0 G hG hpos m hmsum).toContinuousLinearMap)
…

Mentions: OAI.Problem358.CellLaplacian.normalizedSpace, OAI.Problem358.CellLaplacian.normalizedEquiv

theorem OAI.Problem358.CellLaplacian.deriv_massResidual_solution_energy_le line 179

Source documentation

Version of the intercept derivative-energy estimate for the ordinary coordinate-valued mass map. Both partial derivatives of the normalized residual are identified here from the actual coordinate derivative.

theorem deriv_massResidual_solution_energy_le
    {n : ℕ∞ω} (hn : n ≠ 0)
    (g : ι → ι → ℝ) (b : ι → ι → V)
    (hg : ∀ i j, g i j = g j i) (hb : ∀ i j, b i j = b j i)
    (hg0 : ∀ i j, 0 ≤ g i j) (G : SimpleGraph ι)
    (hG : G.Connected) (hpos : ∀ i j, G.Adj i j → 0 < g i j)
    (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hmsum : ∑ i, m i = 1)
    (M : ℝ × normalizedSpace m → (ι → ℝ))
    (s : ℝ → normalizedSpace m) (t : ℝ)
    (hM : ContDiffAt ℝ n M (t, s t))
    (A : ℝ × normalizedSpace m →L[ℝ] (ι → ℝ))
    (hDM : HasFDerivAt M A (t, s t))
…

Mentions: OAI.Problem358.CellLaplacian.normalizedSpace