CanonicalLaplacian.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

The normalized cell Laplacian with its actual intrinsic geometric weights.

All graph hypotheses in the algebraic inverse theorem are discharged here for positive-mass convex affine cells. No analytic differentiability assertion is made: the resulting equivalence is ready to identify with the mass Jacobian.

def OAI.Problem358.PositiveFacet.canonicalFaceWeight line 26
Source documentation
Canonical normalized intrinsic area of the common closed cell face.
```
def canonicalFaceWeight (K : Set (E d)) (y : ι → E d) (c : ι → ℝ)
    (i j : ι) : ℝ :=
…
```
theorem OAI.Problem358.PositiveFacet.canonicalFaceWeight_symm line 32
theorem OAI.Problem358.PositiveFacet.canonicalFaceWeight_nonneg line 39
theorem OAI.Problem358.PositiveFacet.canonicalFaceWeight_self line 43

theorem OAI.Problem358.PositiveFacet.canonicalFaceWeight_eq_chart line 48

Source documentation

An arbitrary tie-plane chart computes the canonical coefficient.

theorem canonicalFaceWeight_eq_chart [Finite ι]
    (K : Set (E d)) (hK : IsCompact K) (y : ι → E d) (c : ι → ℝ)
    {i j : ι} (hy : y i ≠ y j) (base : E d)
    (hbase : TripleCell.score (y i) (c i) base = TripleCell.score (y j) (c j) base) :
    canonicalFaceWeight K y c i j =
      (volume (surfaceFace K y c i j base)).toReal /
        ((volume K).toReal * ‖y i - y j‖) := by
…

Mentions: OAI.Problem358.TripleCell.score, OAI.Problem358.PositiveFacet.canonicalFaceWeight, OAI.Problem358.PositiveFacet.surfaceFace

theorem OAI.Problem358.PositiveFacet.strictTieGraph_adj_canonicalFaceWeight_pos line 68

Source documentation

Every strict geometric facet has genuinely positive canonical weight.

theorem strictTieGraph_adj_canonicalFaceWeight_pos [Finite ι]
    (K : Set (E d)) (hK : IsCompact K) (hvol : volume K ≠ 0)
    (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y) {i j : ι}
    (hedge : (strictTieGraph K (fun k => TripleCell.score (y k) (c k))).Adj i j) :
    0 < canonicalFaceWeight K y c i j := by
…

Mentions: OAI.Problem358.PositiveFacet.strictTieGraph, OAI.Problem358.TripleCell.score, OAI.Problem358.PositiveFacet.canonicalFaceWeight

theorem OAI.Problem358.PositiveFacet.canonicalFaceWeight_connected line 79

Source documentation

Positive cell masses supply all conditions required by the abstract connected weighted-graph Laplacian API.

theorem canonicalFaceWeight_connected [Finite ι] [Nonempty ι]
    (ρ : Measure (E d)) (hρ : ρ ≪ volume)
    (K : Set (E d)) (hK : IsCompact K) (hconv : Convex ℝ K)
    (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
    (hpos : ∀ i, ρ (CellGeometry.closedCell K y c i) ≠ 0) :
    ∃ G : SimpleGraph ι, G.Connected ∧
      ∀ i j, G.Adj i j → 0 < canonicalFaceWeight K y c i j := by
…

Mentions: OAI.Problem358.CellGeometry.closedCell, OAI.Problem358.PositiveFacet.canonicalFaceWeight

theorem OAI.Problem358.PositiveFacet.canonicalLaplacian_eq_zero_iff_constant line 95

Source documentation

The actual geometric cell Laplacian has exactly the constant kernel.

theorem canonicalLaplacian_eq_zero_iff_constant [Fintype ι] [Nonempty ι]
    (ρ : Measure (E d)) (hρ : ρ ≪ volume)
    (K : Set (E d)) (hK : IsCompact K) (hconv : Convex ℝ K)
    (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
    (hpos : ∀ i, ρ (CellGeometry.closedCell K y c i) ≠ 0) (q : ι → ℝ) :
    CellLaplacian.apply (canonicalFaceWeight K y c) q = 0 ↔
      ∃ a : ℝ, ∀ i, q i = a := by
…

Mentions: OAI.Problem358.CellGeometry.closedCell, OAI.Problem358.CellLaplacian.apply, OAI.Problem358.PositiveFacet.canonicalFaceWeight

theorem OAI.Problem358.PositiveFacet.canonicalLaplacian_existsUnique_normalized_solution line 108

Source documentation

Every zero-sum mass variation has one and only one normalized geometric intercept variation.

theorem canonicalLaplacian_existsUnique_normalized_solution [Fintype ι] [Nonempty ι]
    (ρ : Measure (E d)) (hρ : ρ ≪ volume)
    (K : Set (E d)) (hK : IsCompact K) (hconv : Convex ℝ K)
    (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
    (hpos : ∀ i, ρ (CellGeometry.closedCell K y c i) ≠ 0)
    (m z : ι → ℝ) (hm : ∑ i, m i = 1) (hz : ∑ i, z i = 0) :
    ∃! q : ι → ℝ, CellLaplacian.apply (canonicalFaceWeight K y c) q = z ∧
      ∑ i, m i * q i = 0 := by
…

Mentions: OAI.Problem358.CellGeometry.closedCell, OAI.Problem358.CellLaplacian.apply, OAI.Problem358.PositiveFacet.canonicalFaceWeight

def OAI.Problem358.PositiveFacet.canonicalNormalizedEquiv line 123

Source documentation

The canonical normalized geometric cell Laplacian is a continuous linear isomorphism, with all positivity and connectivity consequences proved.

def canonicalNormalizedEquiv [Fintype ι] [Nonempty ι]
    (ρ : Measure (E d)) (hρ : ρ ≪ volume)
    (K : Set (E d)) (hK : IsCompact K) (hconv : Convex ℝ K)
    (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
    (hpos : ∀ i, ρ (CellGeometry.closedCell K y c i) ≠ 0)
    (m : ι → ℝ) (hm : ∑ i, m i = 1) :
    CellLaplacian.normalizedSpace m ≃L[ℝ]
      CellLaplacian.normalizedSpace (fun _ : ι => 1) := by
…

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

theorem OAI.Problem358.PositiveFacet.canonicalNormalizedEquiv_apply line 135

theorem OAI.Problem358.CellGeometry.intrinsicCutCoefficient_eq_faceIntegral line 158

Source documentation

The global intrinsic cut integral is the actual common-face integral.

theorem intrinsicCutCoefficient_eq_faceIntegral
    {K : Set (E d)} (hK : IsClosed K)
    (y : ι → E d) (c : ι → ℝ) {i j : ι} (hy : y i ≠ y j)
    (w : E d → ℝ) :
    AffinePlaneGraph.intrinsicCutCoefficient K ((Finset.univ.erase i).erase j) i j w
      (y, c) =
      (∫ x in closedCell K y c i ∩ closedCell K y c j, w x
        ∂IntrinsicSurface.interfaceMeasure (y i) (y j) (c i) (c j)) / ‖y i - y j‖ := by
…

Mentions: OAI.Problem358.AffinePlaneGraph.intrinsicCutCoefficient, OAI.Problem358.CellGeometry.closedCell, OAI.Problem358.IntrinsicSurface.interfaceMeasure

theorem OAI.Problem358.CellGeometry.continuousAt_normalizedFaceIntegral line 180

Source documentation

Continuity of an arbitrary continuous scalar common-face integral, with the actual source and normal normalization.

theorem continuousAt_normalizedFaceIntegral
    {ρ : 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 j : ι} (hij : i ≠ j) {w : E d → ℝ} (hw : Continuous w) :
    ContinuousAt (fun p : (ι → E d) × (ι → ℝ) =>
      (∫ x in closedCell K p.1 p.2 i ∩ closedCell K p.1 p.2 j, w x
        ∂IntrinsicSurface.interfaceMeasure (p.1 i) (p.1 j) (p.2 i) (p.2 j)) /
          ((volume K).toReal * ‖p.1 i - p.1 j‖)) (y, c) := by
…

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

theorem OAI.Problem358.CellGeometry.continuousAt_canonicalFaceWeight line 202

Source documentation

Canonical normalized face areas vary continuously at positive cells.

theorem continuousAt_canonicalFaceWeight
    {ρ : 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 j : ι) :
    ContinuousAt (fun p : (ι → E d) × (ι → ℝ) =>
      PositiveFacet.canonicalFaceWeight K p.1 p.2 i j) (y, c) := by
…

Mentions: OAI.Problem358.CellGeometry.closedCell, OAI.Problem358.PositiveFacet.canonicalFaceWeight

theorem OAI.Problem358.CellGeometry.continuousAt_faceMoment line 219

Source documentation

Canonical normalized first face moments also vary continuously.

theorem continuousAt_faceMoment
    {ρ : 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 j : ι) :
    ContinuousAt (fun p : (ι → E d) × (ι → ℝ) => faceMoment K p.1 p.2 i j) (y, c) := by
…

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