CellFaces.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Canonical first-moment coefficients of common affine-cell faces.

theorem OAI.Problem358.CellGeometry.mem_commonFace_iff line 18

Source documentation

A common cell face is exactly one closed cell restricted to the tie plane.

theorem mem_commonFace_iff (K : Set (E d)) (y : ι → E d) (c : ι → ℝ)
    (i j : ι) (x : E d) :
    x ∈ closedCell K y c i ∩ closedCell K y c j ↔
      x ∈ closedCell K y c i ∧ ⟪x, y i⟫ + c i = ⟪x, y j⟫ + c j := by
…

Mentions: OAI.Problem358.CellGeometry.closedCell

theorem OAI.Problem358.CellGeometry.mem_commonFace_iff_of_tie line 29

Source documentation

On the tie plane only the other branches constrain the common face.

theorem mem_commonFace_iff_of_tie (K : Set (E d)) (y : ι → E d)
    (c : ι → ℝ) (i j : ι) {x : E d}
    (htie : ⟪x, y i⟫ + c i = ⟪x, y j⟫ + c j) :
    x ∈ closedCell K y c i ∩ closedCell K y c j ↔
      x ∈ K ∧ ∀ k, k ≠ i → k ≠ j → ⟪x, y k⟫ + c k ≤ ⟪x, y i⟫ + c i := by
…

Mentions: OAI.Problem358.CellGeometry.closedCell

def OAI.Problem358.CellGeometry.faceMoment line 50
Source documentation
The vector face coefficient used by both mass site-motion and stationary first-moment differentiation. The diagonal is zero by the normal-length factor.
```
def faceMoment (K : Set (E d)) (y : ι → E d) (c : ι → ℝ) (i j : ι) : E d :=
…
```
theorem OAI.Problem358.CellGeometry.faceMoment_symm line 55
theorem OAI.Problem358.CellGeometry.faceMoment_self line 61

theorem OAI.Problem358.CellGeometry.faceMoment_eq_chart line 66

Source documentation

A tie-plane chart gives the same canonical normalized first moment.

theorem faceMoment_eq_chart (K : Set (E d)) (y : ι → E d) (c : ι → ℝ)
    {i j : ι} (hy : y i ≠ y j) {z : E d}
    (htie : ⟪z, y i⟫ + c i = ⟪z, y j⟫ + c j) :
    faceMoment K y c i j = ((volume K).toReal * ‖y i - y j‖)⁻¹ •
      ∫ w : (ℝ ∙ (y i - y j))ᗮ in
        {w : (ℝ ∙ (y i - y j))ᗮ |
          z + (w : E d) ∈ closedCell K y c i ∩ closedCell K y c j},
        z + (w : E d) := by
…

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

theorem OAI.Problem358.CellGeometry.commonFace_indicator_eq_cut_product line 95

Source documentation

On an equality plane the remaining cut indicators describe exactly the common face, including its boundary.

theorem commonFace_indicator_eq_cut_product (K : Set (E d))
    (y : ι → E d) (c : ι → ℝ) (i j : ι) (J : Finset ι)
    (hJ : ∀ k, k ∈ J ↔ k ≠ i ∧ k ≠ j) (f : E d → ℝ) {x : E d}
    (htie : ⟪x, y i⟫ + c i = ⟪x, y j⟫ + c j) :
    (closedCell K y c i ∩ closedCell K y c j).indicator f x =
      K.indicator f x * ∏ k ∈ J,
        MovingCellTrace.cutIndicator (⟪x, y i - y k⟫ + (c i - c k)) := by
…

Mentions: OAI.Problem358.CellGeometry.closedCell, OAI.Problem358.MovingCellTrace.cutIndicator

theorem OAI.Problem358.CellGeometry.tie_on_tangent_chart line 135

Source documentation

Translating a tangent vector preserves the affine equality.

theorem tie_on_tangent_chart (y : ι → E d) (c : ι → ℝ) (i j : ι)
    {z : E d} (htie : ⟪z, y i⟫ + c i = ⟪z, y j⟫ + c j)
    (w : (ℝ ∙ (y i - y j))ᗮ) :
    ⟪z + (w : E d), y i⟫ + c i = ⟪z + (w : E d), y j⟫ + c j := by
…

theorem OAI.Problem358.CellGeometry.interface_integral_eq_cut_trace line 150

Source documentation

The scalar face integral in a moving-cut formula is the canonical intrinsic integral over the common cell face. No boundary or third-tie exception is needed for this exact identification.

theorem interface_integral_eq_cut_trace {K : Set (E d)} (hK : IsClosed K)
    (y : ι → E d) (c : ι → ℝ) {i j : ι} (hy : y i ≠ y j)
    (J : Finset ι) (hJ : ∀ k, k ∈ J ↔ k ≠ i ∧ k ≠ j)
    (f : E d → ℝ) {z : E d}
    (htie : ⟪z, y i⟫ + c i = ⟪z, y j⟫ + c j) :
    (∫ x in closedCell K y c i ∩ closedCell K y c j, f x
      ∂IntrinsicSurface.interfaceMeasure (y i) (y j) (c i) (c j)) =
      ∫ w : (ℝ ∙ (y i - y j))ᗮ,
        K.indicator f (z + (w : E d)) * ∏ k ∈ J,
          MovingCellTrace.cutIndicator
            (⟪z + (w : E d), y i - y k⟫ + (c i - c k)) := by
…

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

theorem OAI.Problem358.PositiveCellFullDerivative.faceVariation_eq_intrinsic line 188

Source documentation

The cut derivative is intrinsically defined and independent of the chosen tie-plane basepoint. This identity holds for every scalar weight.

theorem faceVariation_eq_intrinsic {K : Set (E d)} (hK : IsClosed K)
    (y v : ι → E d) (c r : ι → ℝ) (w : E d → ℝ)
    {i j : ι} (hy : y i ≠ y j) {z : E d}
    (htie : ⟪z, y i⟫ + c i = ⟪z, y j⟫ + c j) :
    faceVariation K y v c r w i j z =
      ∫ x in closedCell K y c i ∩ closedCell K y c j,
        ((r i - r j + ⟪v i - v j, x⟫) / ‖y i - y j‖) * w x
        ∂IntrinsicSurface.interfaceMeasure (y i) (y j) (c i) (c j) := by
…

Mentions: OAI.Problem358.PositiveCellFullDerivative.faceVariation, OAI.Problem358.IntrinsicSurface.interfaceMeasure

theorem OAI.Problem358.PositiveCellFullDerivative.normalized_faceVariation_one line 217

Source documentation

The mass face contribution equals the scalar and first-moment coefficients with the exact source-volume normalization. No positive-volume cancellation is needed in this algebraic identity.

theorem normalized_faceVariation_one {K : Set (E d)} (hK : IsCompact K)
    (y v : ι → E d) (c r : ι → ℝ) {i j : ι} (hy : y i ≠ y j)
    {z : E d} (htie : ⟪z, y i⟫ + c i = ⟪z, y j⟫ + c j) :
    (volume K).toReal⁻¹ * faceVariation K y v c r (fun _ => 1) i j z =
      (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⟫ := by
…

Mentions: OAI.Problem358.PositiveCellFullDerivative.faceVariation, OAI.Problem358.IntrinsicSurface.interfaceMeasure