OAI/Analysis/Brenier/Laplacian.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Algebraic facts about the weighted cell-adjacency Laplacian.

  1. def OAI.Problem358.CellLaplacian.apply line 16

    Source documentation

    The intercept derivative of the cell masses, written in coordinates.

    def apply (g : ι → ι → ℝ) (q : ι → ℝ) (i : ι) : ℝ :=
…
  2. lemma OAI.Problem358.CellLaplacian.apply_const line 19
  3. lemma OAI.Problem358.CellLaplacian.sum_apply line 24
  4. lemma OAI.Problem358.CellLaplacian.energy_identity line 36
  5. lemma OAI.Problem358.CellLaplacian.eq_of_positive_edge_of_apply_eq_zero line 67
  6. lemma OAI.Problem358.CellLaplacian.constant_of_apply_eq_zero line 85

    Source documentation

    Connectivity may be supplied by any graph whose edges have positive weights.

    lemma constant_of_apply_eq_zero
    (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)
    (q : ι → ℝ) (hq : apply g q = 0) : ∃ c : ℝ, ∀ i, q i = c := by
…

    Mentions: OAI.Problem358.CellLaplacian.apply

  7. lemma OAI.Problem358.CellLaplacian.apply_eq_zero_iff_constant line 103
  8. lemma OAI.Problem358.CellLaplacian.eq_zero_of_normalized_kernel line 116

    Source documentation

    The mass-weighted normalization eliminates the constant kernel.

    lemma eq_zero_of_normalized_kernel
    (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)
    (m q : ι → ℝ) (hm : ∑ i, m i = 1)
    (hq : apply g q = 0) (hmean : ∑ i, m i * q i = 0) : q = 0 := by
…

    Mentions: OAI.Problem358.CellLaplacian.apply

  9. lemma OAI.Problem358.CellLaplacian.pairing_symmetric line 130
  10. def OAI.Problem358.CellLaplacian.linearMap line 154

    Source documentation

    The cell Laplacian as an operator on Euclidean coordinate space.

    def linearMap (g : ι → ι → ℝ) :
    EuclideanSpace ℝ ι →ₗ[ℝ] EuclideanSpace ℝ ι where
…
  11. lemma OAI.Problem358.CellLaplacian.linearMap_apply line 173
  12. lemma OAI.Problem358.CellLaplacian.linearMap_isSymmetric line 176
  13. lemma OAI.Problem358.CellLaplacian.mem_range_iff_sum_eq_zero line 183

    Source documentation

    The image of a connected symmetric cell Laplacian is the zero-sum hyperplane.

    lemma mem_range_iff_sum_eq_zero
    (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)
    (z : EuclideanSpace ℝ ι) :
    z ∈ LinearMap.range (linearMap g) ↔ ∑ i, z i = 0 := by
…

    Mentions: OAI.Problem358.CellLaplacian.linearMap

  14. lemma OAI.Problem358.CellLaplacian.exists_apply_eq_of_sum_eq_zero line 208
  15. lemma OAI.Problem358.CellLaplacian.apply_sub_const line 219
  16. lemma OAI.Problem358.CellLaplacian.apply_sub line 227
  17. lemma OAI.Problem358.CellLaplacian.existsUnique_normalized_solution line 236

    Source documentation

    The mass-weighted normalization determines the solution of the cell equation uniquely.

    lemma existsUnique_normalized_solution
    (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)
    (m z : ι → ℝ) (hm : ∑ i, m i = 1) (hz : ∑ i, z i = 0) :
    ∃! q : ι → ℝ, apply g q = z ∧ ∑ i, m i * q i = 0 := by
…

    Mentions: OAI.Problem358.CellLaplacian.apply

  18. def OAI.Problem358.CellLaplacian.weightedMean line 266

    Source documentation

    The weighted intercept normalization functional.

    def weightedMean (m : ι → ℝ) : (ι → ℝ) →ₗ[ℝ] ℝ where
…
  19. def OAI.Problem358.CellLaplacian.normalizedSpace line 275

    Source documentation

    The hyperplane of intercepts with weighted average zero.

    def normalizedSpace (m : ι → ℝ) : Submodule ℝ (ι → ℝ) := (weightedMean m).ker

    Mentions: OAI.Problem358.CellLaplacian.weightedMean

  20. lemma OAI.Problem358.CellLaplacian.mem_normalizedSpace line 277
  21. def OAI.Problem358.CellLaplacian.coordinateLinearMap line 281

    Source documentation

    The weighted Laplacian on coordinate functions, without a change of norm.

    def coordinateLinearMap (g : ι → ι → ℝ) : (ι → ℝ) →ₗ[ℝ] (ι → ℝ) where
…
  22. lemma OAI.Problem358.CellLaplacian.coordinateLinearMap_apply line 298
  23. def OAI.Problem358.CellLaplacian.normalizedLinearMap line 302

    Source documentation

    The normalized mass Jacobian, with codomain the zero-sum mass variations.

    def normalizedLinearMap (g : ι → ι → ℝ) (hsym : ∀ i j, g i j = g j i)
    (m : ι → ℝ) : normalizedSpace m →ₗ[ℝ] normalizedSpace (fun _ : ι => 1) :=
…

    Mentions: OAI.Problem358.CellLaplacian.normalizedSpace

  24. lemma OAI.Problem358.CellLaplacian.normalizedLinearMap_apply line 310
  25. lemma OAI.Problem358.CellLaplacian.normalizedLinearMap_bijective line 314
  26. def OAI.Problem358.CellLaplacian.normalizedEquiv line 342

    Source documentation

    The invertible normalized cell-mass Jacobian. This is the continuous-linear-equivalence interface needed by the implicit function theorem. Its existence makes no assertion of a uniform bound on the inverse.

    def normalizedEquiv
    (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)
    (m : ι → ℝ) (hm : ∑ i, m i = 1) :
    normalizedSpace m ≃L[ℝ] normalizedSpace (fun _ : ι => 1) :=
…

    Mentions: OAI.Problem358.CellLaplacian.normalizedSpace

  27. lemma OAI.Problem358.CellLaplacian.normalizedEquiv_apply line 351
  28. lemma OAI.Problem358.CellLaplacian.apply_normalizedEquiv_symm line 359

    Source documentation

    Applying the inverse solves the normalized cell-mass equation.

    @[simp] lemma apply_normalizedEquiv_symm
    (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)
    (m : ι → ℝ) (hm : ∑ i, m i = 1)
    (z : normalizedSpace (fun _ : ι => 1)) :
    apply g ((normalizedEquiv g hsym hnonneg G hG hpos m hm).symm z) = z :=
…

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

  29. lemma OAI.Problem358.CellLaplacian.normalizedEquiv_symm_weightedMean line 369

    Source documentation

    The inverse automatically has the required weighted normalization.

    lemma normalizedEquiv_symm_weightedMean
    (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)
    (m : ι → ℝ) (hm : ∑ i, m i = 1)
    (z : normalizedSpace (fun _ : ι => 1)) :
    ∑ i, m i * ((normalizedEquiv g hsym hnonneg G hG hpos m hm).symm z : ι → ℝ) i = 0 :=
…

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

  30. theorem OAI.Problem358.contDiffAt_unique_implicit_solution line 398

    Source documentation

    A uniquely specified solution agrees locally with the implicit branch, and so inherits its regularity. No prior continuity of the selected solution is required.

    theorem contDiffAt_unique_implicit_solution
    {n : ℕ∞ω} {F : P × Q → R} {s : P → Q} {p : P}
    (hn : n ≠ 0) (hF : ContDiffAt ℝ n F (p, s p))
    (hpartial : (fderiv ℝ F (p, s p) ∘L ContinuousLinearMap.inr ℝ P Q).IsInvertible)
    (hzero : F (p, s p) = 0)
    (hunique : ∀ᶠ x in 𝓝 p, ∀ q, F (x, q) = 0 → q = s x) :
    ContDiffAt ℝ n s p := by
…
  31. theorem OAI.Problem358.hasStrictFDerivAt_unique_implicit_solution line 412

    Source documentation

    The derivative of the uniquely specified branch is the usual implicit derivative.

    theorem hasStrictFDerivAt_unique_implicit_solution
    {n : ℕ∞ω} {F : P × Q → R} {s : P → Q} {p : P}
    (hn : n ≠ 0) (hF : ContDiffAt ℝ n F (p, s p))
    (hpartial : (fderiv ℝ F (p, s p) ∘L ContinuousLinearMap.inr ℝ P Q).IsInvertible)
    (hzero : F (p, s p) = 0)
    (hunique : ∀ᶠ x in 𝓝 p, ∀ q, F (x, q) = 0 → q = s x) :
    HasStrictFDerivAt s
      (-(fderiv ℝ F (p, s p) ∘L ContinuousLinearMap.inr ℝ P Q).inverse ∘L
        (fderiv ℝ F (p, s p) ∘L ContinuousLinearMap.inl ℝ P Q)) p := by
…
  32. theorem OAI.Problem358.eventually_eq_of_hasStrictFDerivAt_equiv line 429

    Source documentation

    An invertible derivative makes the fiber of a map locally a singleton.

    theorem eventually_eq_of_hasStrictFDerivAt_equiv [CompleteSpace R]
    {f : Q → R} {q : Q} (e : Q ≃L[ℝ] R)
    (hf : HasStrictFDerivAt f e.toContinuousLinearMap q) :
    ∀ᶠ r in 𝓝 q, f r = f q → r = q := by
…
  33. theorem OAI.Problem358.CellLaplacian.partial_isInvertible_of_laplacian line 445

    Source documentation

    Invertibility of the intercept partial derivative follows from the connected cell graph.

    theorem partial_isInvertible_of_laplacian [CompleteSpace P]
    (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)
    (m : ι → ℝ) (hm : ∑ i, m i = 1)
    (A : P × normalizedSpace m →L[ℝ] normalizedSpace (fun _ : ι => 1))
    (hA : A ∘L ContinuousLinearMap.inr ℝ P (normalizedSpace m) =
      (normalizedEquiv g hsym hnonneg G hG hpos m hm).toContinuousLinearMap) :
    (A ∘L ContinuousLinearMap.inr ℝ P (normalizedSpace m)).IsInvertible := by
…

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

  34. theorem OAI.Problem358.CellLaplacian.contDiffAt_normalized_solution line 459

    Source documentation

    The analytic hypothesis on the mass map and the algebraic cell graph together imply smooth dependence of its uniquely normalized solution on the sites.

    theorem contDiffAt_normalized_solution
    {n : ℕ∞ω} (hn : n ≠ 0)
    (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)
    (m : ι → ℝ) (hm : ∑ i, m i = 1)
    (F : P × normalizedSpace m → normalizedSpace (fun _ : ι => 1))
    (s : P → normalizedSpace m) (p : P)
    (hF : ContDiffAt ℝ n F (p, s p))
    (hA : fderiv ℝ F (p, s p) ∘L ContinuousLinearMap.inr ℝ P (normalizedSpace m) =
      (normalizedEquiv g hsym hnonneg G hG hpos m hm).toContinuousLinearMap)
    (hzero : F (p, s p) = 0)
…

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

  35. theorem OAI.Problem358.CellLaplacian.hasDerivAt_normalized_solution line 485

    Source documentation

    Along a real parameter, the derivative of the prescribed normalized intercepts is the negative inverse mass Jacobian applied to the site variation.

    theorem hasDerivAt_normalized_solution
    {n : ℕ∞ω} (hn : n ≠ 0)
    (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)
    (m : ι → ℝ) (hm : ∑ 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 hsym hnonneg G hG hpos m hm).toContinuousLinearMap)
    (hzero : F (t, s t) = 0)
…

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

  36. theorem OAI.Problem358.CellLaplacian.laplacian_deriv_normalized_solution line 509

    Source documentation

    The differentiated fixed-mass constraint, directly in cell coordinates.

    theorem laplacian_deriv_normalized_solution
    {n : ℕ∞ω} (hn : n ≠ 0)
    (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)
    (m : ι → ℝ) (hm : ∑ 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 hsym hnonneg G hG hpos m hm).toContinuousLinearMap)
    (hzero : F (t, s t) = 0)
…

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

  37. def OAI.Problem358.CellLaplacian.zeroSumProjection line 541

    Source documentation

    A continuous linear projection onto zero-sum mass variations.

    def zeroSumProjection (m : ι → ℝ) (hm : ∑ i, m i = 1) :
    (ι → ℝ) →L[ℝ] normalizedSpace (fun _ : ι => 1) :=
…

    Mentions: OAI.Problem358.CellLaplacian.normalizedSpace

  38. theorem OAI.Problem358.CellLaplacian.zeroSumProjection_apply line 564
  39. theorem OAI.Problem358.CellLaplacian.zeroSumProjection_eq line 569

    Source documentation

    The projection fixes all genuine mass variations.

    theorem zeroSumProjection_eq (m : ι → ℝ) (hm : ∑ i, m i = 1)
    (z : ι → ℝ) (hz : ∑ i, z i = 0) :
    (zeroSumProjection m hm z : ι → ℝ) = z := by
…

    Mentions: OAI.Problem358.CellLaplacian.zeroSumProjection

  40. def OAI.Problem358.CellLaplacian.massResidual line 576

    Source documentation

    The mass residual for an ordinary coordinate-valued mass map.

    def massResidual {P : Type*} (m : ι → ℝ) (hm : ∑ i, m i = 1)
    (M : P × normalizedSpace m → (ι → ℝ)) :
    P × normalizedSpace m → normalizedSpace (fun _ : ι => 1) :=
…

    Mentions: OAI.Problem358.CellLaplacian.normalizedSpace

  41. theorem OAI.Problem358.CellLaplacian.massResidual_coe line 582

    Source documentation

    On probability mass vectors the projected residual is exactly the physical residual.

    theorem massResidual_coe {P : Type*} (m : ι → ℝ) (hm : ∑ i, m i = 1)
    (M : P × normalizedSpace m → (ι → ℝ)) (x : P × normalizedSpace m)
    (hM : ∑ i, M x i = 1) :
    (massResidual m hm M x : ι → ℝ) = M x - m := by
…

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

  42. theorem OAI.Problem358.CellLaplacian.massResidual_eq_zero_iff line 589
  43. theorem OAI.Problem358.CellLaplacian.contDiffAt_massResidual line 598
  44. theorem OAI.Problem358.CellLaplacian.hasFDerivAt_massResidual line 603
  45. theorem OAI.Problem358.CellLaplacian.zeroSumProjection_laplacian line 610

    Source documentation

    Projection does not alter a Laplacian derivative: its image already has zero sum.

    theorem zeroSumProjection_laplacian (m : ι → ℝ) (hm : ∑ i, m i = 1)
    (g : ι → ι → ℝ) (hsym : ∀ i j, g i j = g j i)
    (q : normalizedSpace m) :
    zeroSumProjection m hm (apply g q) = normalizedLinearMap g hsym m q := by
…

    Mentions: OAI.Problem358.CellLaplacian.normalizedSpace, OAI.Problem358.CellLaplacian.zeroSumProjection, OAI.Problem358.CellLaplacian.apply, OAI.Problem358.CellLaplacian.normalizedLinearMap

  46. theorem OAI.Problem358.CellLaplacian.massResidual_partial_eq line 619

    Source documentation

    An ordinary coordinate derivative with Laplacian intercept part induces precisely the normalized continuous linear equivalence used by the implicit function theorem.

    theorem massResidual_partial_eq
    (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)
    (m : ι → ℝ) (hm : ∑ i, m i = 1)
    (A : P × normalizedSpace m →L[ℝ] (ι → ℝ))
    (hA : ∀ q : normalizedSpace m, A (0, q) = apply g q) :
    ((zeroSumProjection m hm) ∘L A) ∘L
        ContinuousLinearMap.inr ℝ P (normalizedSpace m) =
      (normalizedEquiv g hsym hnonneg G hG hpos m hm).toContinuousLinearMap := by
…

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