Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Foundations.CubeDirichletH2.OddReflection

Coarse-graining support: Support.Sobolev.Foundations.CubeDirichletH2.OddReflection #

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Odd reflection data for cube Dirichlet H² #

This file contains the pointwise and H¹ one-cell vocabulary for the odd reflection argument. The analytic endpoint will assemble these cells across the full reflection block and then reuse the interior weak-Hessian estimate.

source
def HCPolySupport.cubeDirichletOddReflectionCellSign {d : ℕ} (choice : Fin d → Fin 3) :
ℝ

The scalar sign used for Dirichlet odd reflection on one reflection cell.

Each coordinate outside the original strip contributes a factor -1; each coordinate in the original strip contributes 1.

Equations
Instances For
    source
    @[simp]
    theorem HCPolySupport.cubeDirichletOddReflectionCellSign_center {d : ℕ} :
    (cubeDirichletOddReflectionCellSign fun (x : Fin d) => 1) = 1
    source
    @[simp]
    theorem HCPolySupport.cubeDirichletOddReflectionCellSign_mul_self {d : ℕ} (choice : Fin d → Fin 3) :
    cubeDirichletOddReflectionCellSign choice * cubeDirichletOddReflectionCellSign choice = 1
    source
    @[simp]
    theorem HCPolySupport.cubeDirichletOddReflectionCellSign_sq {d : ℕ} (choice : Fin d → Fin 3) :
    cubeDirichletOddReflectionCellSign choice ^ 2 = 1
    source
    theorem HCPolySupport.cubeDirichletOddReflectionCellSign_ne_zero {d : ℕ} (choice : Fin d → Fin 3) :
    cubeDirichletOddReflectionCellSign choice ≠ 0
    source
    noncomputable def HCPolySupport.cubeDirichletOddReflectionSign {d : ℕ} (Q : TriadicCube d) (x : Vec d) :
    ℝ

    The global odd-reflection sign induced by the coordinate fold.

    Equations
    Instances For
      source
      @[simp]
      theorem HCPolySupport.cubeDirichletOddReflectionSign_mul_self {d : ℕ} (Q : TriadicCube d) (x : Vec d) :
      cubeDirichletOddReflectionSign Q x * cubeDirichletOddReflectionSign Q x = 1
      source
      @[simp]
      theorem HCPolySupport.cubeDirichletOddReflectionSign_sq {d : ℕ} (Q : TriadicCube d) (x : Vec d) :
      cubeDirichletOddReflectionSign Q x ^ 2 = 1
      source
      theorem HCPolySupport.cubeDirichletOddReflectionSign_eq_cellSign_of_mem_cellCube {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) {x : Vec d} (hx : x ∈ openCubeSet (cubeFaceReflectionCellCube Q choice)) :
      cubeDirichletOddReflectionSign Q x = cubeDirichletOddReflectionCellSign choice

      On a reflection cell, the global odd sign is the cell sign.

      source
      noncomputable def HCPolySupport.cubeDirichletOddReflectionCellScalar {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) (F : Vec d → ℝ) :
      Vec d → ℝ

      Pointwise scalar odd reflection on one reflection cell.

      Equations
      Instances For
        source
        @[simp]
        theorem HCPolySupport.cubeDirichletOddReflectionCellScalar_apply {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) (F : Vec d → ℝ) (x : Vec d) :
        cubeDirichletOddReflectionCellScalar Q choice F x = cubeDirichletOddReflectionCellSign choice * F (cubeFaceReflectionCellFoldMap Q choice x)
        source
        noncomputable def HCPolySupport.cubeDirichletOddReflectionCellVectorField {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) (G : Vec d → Vec d) :
        Vec d → Vec d

        Pointwise reflected gradient profile corresponding to one scalar odd cell.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem HCPolySupport.cubeDirichletOddReflectionCellVectorField_apply {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) (G : Vec d → Vec d) (x : Vec d) :
          cubeDirichletOddReflectionCellVectorField Q choice G x = cubeDirichletOddReflectionCellSign choice • (cubeFaceReflectionCellFoldLinear choice) (G (cubeFaceReflectionCellFoldMap Q choice x))
          source
          noncomputable def HCPolySupport.cubeDirichletOddReflectionScalar {d : ℕ} (Q : TriadicCube d) (F : Vec d → ℝ) :
          Vec d → ℝ

          Global scalar odd reflection obtained from the coordinate fold.

          Equations
          Instances For
            source
            @[simp]
            theorem HCPolySupport.cubeDirichletOddReflectionScalar_apply {d : ℕ} (Q : TriadicCube d) (F : Vec d → ℝ) (x : Vec d) :
            cubeDirichletOddReflectionScalar Q F x = cubeDirichletOddReflectionSign Q x * F (cubeCoordinateFold Q x)
            source
            noncomputable def HCPolySupport.cubeDirichletOddReflectionVectorField {d : ℕ} (Q : TriadicCube d) (G : Vec d → Vec d) :
            Vec d → Vec d

            Global reflected gradient profile corresponding to the scalar odd reflection.

            Equations
            Instances For
              source
              @[simp]
              theorem HCPolySupport.cubeDirichletOddReflectionVectorField_apply {d : ℕ} (Q : TriadicCube d) (G : Vec d → Vec d) (x : Vec d) :
              cubeDirichletOddReflectionVectorField Q G x = cubeDirichletOddReflectionSign Q x • cubeCoordinateFoldReflectedVectorField Q G x
              source
              theorem HCPolySupport.cubeDirichletOddReflectionScalar_eq_cellScalar_of_mem_cellCube {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) (F : Vec d → ℝ) {x : Vec d} (hx : x ∈ openCubeSet (cubeFaceReflectionCellCube Q choice)) :
              cubeDirichletOddReflectionScalar Q F x = cubeDirichletOddReflectionCellScalar Q choice F x

              The global odd scalar agrees with the affine one-cell scalar on a reflection cell.

              source
              theorem HCPolySupport.cubeDirichletOddReflectionVectorField_eq_cellVectorField_of_mem_cellCube {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) (G : Vec d → Vec d) {x : Vec d} (hx : x ∈ openCubeSet (cubeFaceReflectionCellCube Q choice)) :
              cubeDirichletOddReflectionVectorField Q G x = cubeDirichletOddReflectionCellVectorField Q choice G x

              The global odd vector profile agrees with the affine one-cell vector profile on a reflection cell.

              source
              theorem HCPolySupport.cubeDirichletOddReflectionSign_eq_one_of_mem_openCubeSet {d : ℕ} (Q : TriadicCube d) {x : Vec d} (hx : x ∈ openCubeSet Q) :
              cubeDirichletOddReflectionSign Q x = 1

              On the original cube, the global odd-reflection sign is 1.

              source
              theorem HCPolySupport.cubeDirichletOddReflectionScalar_eq_self_of_mem_openCubeSet {d : ℕ} (Q : TriadicCube d) (F : Vec d → ℝ) {x : Vec d} (hx : x ∈ openCubeSet Q) :
              cubeDirichletOddReflectionScalar Q F x = F x

              On the original cube, the odd reflected scalar agrees with the original scalar.

              source
              theorem HCPolySupport.cubeDirichletOddReflectionVectorField_eq_self_of_mem_openCubeSet {d : ℕ} (Q : TriadicCube d) (G : Vec d → Vec d) {x : Vec d} (hx : x ∈ openCubeSet Q) :
              cubeDirichletOddReflectionVectorField Q G x = G x

              On the original cube, the odd reflected vector field agrees with the original vector field.

              source
              theorem HCPolySupport.cubeDirichletOddReflectionScalar_mul_self {d : ℕ} (Q : TriadicCube d) (F : Vec d → ℝ) (x : Vec d) :
              cubeDirichletOddReflectionScalar Q F x * cubeDirichletOddReflectionScalar Q F x = cubeCoordinateFoldReflectedScalar Q F x * cubeCoordinateFoldReflectedScalar Q F x

              Odd scalar reflection has the same square as the unsigned coordinate-fold scalar reflection.

              source
              theorem HCPolySupport.cubeDirichletOddReflectionVectorField_self_pairing {d : ℕ} (Q : TriadicCube d) (G : Vec d → Vec d) (x : Vec d) :
              vecDot (cubeDirichletOddReflectionVectorField Q G x) (cubeDirichletOddReflectionVectorField Q G x) = vecDot (cubeCoordinateFoldReflectedVectorField Q G x) (cubeCoordinateFoldReflectedVectorField Q G x)

              Odd vector reflection has the same self-pairing as the unsigned coordinate-fold vector reflection.

              source
              noncomputable def HCPolySupport.H1Function.cubeDirichletOddReflectionCellFold {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) (choice : Fin d → Fin 3) :
              H1Function (openCubeSet (cubeFaceReflectionCellCube Q choice))

              Odd scalar fold of an H¹ function from the original cube to one reflection cell.

              Equations
              Instances For
                source
                @[simp]
                theorem HCPolySupport.H1Function.cubeDirichletOddReflectionCellFold_toFun {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) (choice : Fin d → Fin 3) (x : Vec d) :
                (u.cubeDirichletOddReflectionCellFold choice).toFun x = cubeDirichletOddReflectionCellSign choice * u.toFun (cubeFaceReflectionCellFoldMap Q choice x)
                source
                @[simp]
                theorem HCPolySupport.H1Function.cubeDirichletOddReflectionCellFold_grad {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) (choice : Fin d → Fin 3) (x : Vec d) :
                (u.cubeDirichletOddReflectionCellFold choice).grad x = cubeDirichletOddReflectionCellSign choice • (cubeFaceReflectionCellFoldLinear choice) (u.grad (cubeFaceReflectionCellFoldMap Q choice x))
                source
                theorem HCPolySupport.H1Function.cubeDirichletOddReflectionCellFold_isPotentialOn {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) (choice : Fin d → Fin 3) :
                IsPotentialOn (openCubeSet (cubeFaceReflectionCellCube Q choice)) (cubeDirichletOddReflectionCellVectorField Q choice fun (y : Vec d) => u.grad y)