Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Foundations.CubeCalderonZygmund.ReflectionHessianRowCellH1

Coarse-graining support: #

Support.Sobolev.Foundations.CubeCalderonZygmund.ReflectionHessianRowCellH1

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

Cellwise H¹ reflection of a weak Hessian row #

On a reflection cell, folding the ith weak-gradient coordinate and multiplying it by the mixed sign S * s_i produces an H¹ function. Its weak gradient is exactly the mixed-parity reflection S * s_i * s_j of the ith Hessian row. This file makes only a cellwise assertion; it does not assert that the global mixed reflection belongs to H¹.

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

The mixed-parity reflection of the ith weak-gradient coordinate on one reflection cell.

Equations
Instances For
    source
    @[simp]
    theorem HCPolySupport.HasWeakHessianOn.cubeDirichletOddReflectionGradientCoordCellH1Function_toFun {d : ℕ} {Q : TriadicCube d} {u : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) u) (choice : Fin d → Fin 3) (i : Fin d) :
    (H.cubeDirichletOddReflectionGradientCoordCellH1Function choice i).toFun = cubeDirichletOddReflectionGradientCoordCellScalar Q choice i fun (y : Vec d) => u.grad y i

    The scalar representative is exactly the cellwise mixed reflection of the source weak-gradient coordinate.

    source
    @[simp]
    theorem HCPolySupport.HasWeakHessianOn.cubeDirichletOddReflectionGradientCoordCellH1Function_grad {d : ℕ} {Q : TriadicCube d} {u : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) u) (choice : Fin d → Fin 3) (i : Fin d) :
    (H.cubeDirichletOddReflectionGradientCoordCellH1Function choice i).grad = cubeDirichletOddReflectionHessianRowCellVectorField Q choice i fun (y : Vec d) (j : Fin d) => H.hess i j y

    The weak gradient is exactly the cellwise mixed reflection of the ith Hessian row.

    source
    theorem HCPolySupport.HasWeakHessianOn.cubeDirichletOddReflectionGradientCoordCell_hasWeakGradientOn {d : ℕ} {Q : TriadicCube d} {u : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) u) (choice : Fin d → Fin 3) (i : Fin d) :
    HasWeakGradientOn (openCubeSet (cubeFaceReflectionCellCube Q choice)) (cubeDirichletOddReflectionGradientCoordCellScalar Q choice i fun (y : Vec d) => u.grad y i) (cubeDirichletOddReflectionHessianRowCellVectorField Q choice i fun (y : Vec d) (j : Fin d) => H.hess i j y)

    The exact cellwise scalar and Hessian-row representatives satisfy the weak-gradient identity.

    source
    theorem HCPolySupport.HasWeakHessianOn.cubeDirichletOddReflectionHessianRowCellVectorField_isPotentialOn {d : ℕ} {Q : TriadicCube d} {u : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) u) (choice : Fin d → Fin 3) (i : Fin d) :
    IsPotentialOn (openCubeSet (cubeFaceReflectionCellCube Q choice)) (cubeDirichletOddReflectionHessianRowCellVectorField Q choice i fun (y : Vec d) (j : Fin d) => H.hess i j y)

    The cellwise reflected Hessian row is a potential field.

    source
    theorem HCPolySupport.HasWeakHessianOn.cubeDirichletOddReflectionGradientCoordCellH1Function_eq_global_of_mem {d : ℕ} {Q : TriadicCube d} {u : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) u) (choice : Fin d → Fin 3) (i : Fin d) {x : Vec d} (hx : x ∈ openCubeSet (cubeFaceReflectionCellCube Q choice)) :
    (H.cubeDirichletOddReflectionGradientCoordCellH1Function choice i).toFun x = cubeDirichletOddReflectionGradientCoordScalar Q i (fun (y : Vec d) => u.grad y i) x

    On its reflection cell, the constructed scalar agrees pointwise with the global mixed scalar representative.

    source
    theorem HCPolySupport.HasWeakHessianOn.cubeDirichletOddReflectionGradientCoordCellH1Function_grad_eq_global_of_mem {d : ℕ} {Q : TriadicCube d} {u : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) u) (choice : Fin d → Fin 3) (i : Fin d) {x : Vec d} (hx : x ∈ openCubeSet (cubeFaceReflectionCellCube Q choice)) :
    (H.cubeDirichletOddReflectionGradientCoordCellH1Function choice i).grad x = cubeDirichletOddReflectionHessianRowVectorField Q i (fun (y : Vec d) (j : Fin d) => H.hess i j y) x

    On its reflection cell, the constructed weak gradient agrees pointwise with the global mixed Hessian-row representative.

    source
    theorem HCPolySupport.HasWeakHessianOn.cubeDirichletOddReflectionGradientCoord_hasWeakGradientOn_cell {d : ℕ} {Q : TriadicCube d} {u : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) u) (choice : Fin d → Fin 3) (i : Fin d) :
    HasWeakGradientOn (openCubeSet (cubeFaceReflectionCellCube Q choice)) (cubeDirichletOddReflectionGradientCoordScalar Q i fun (y : Vec d) => u.grad y i) (cubeDirichletOddReflectionHessianRowVectorField Q i fun (y : Vec d) (j : Fin d) => H.hess i j y)

    The global mixed scalar and Hessian-row representatives satisfy the weak gradient identity when both are restricted to one reflection cell.

    source
    theorem HCPolySupport.HasWeakHessianOn.cubeDirichletOddReflectionHessianRowVectorField_isPotentialOn_cell {d : ℕ} {Q : TriadicCube d} {u : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) u) (choice : Fin d → Fin 3) (i : Fin d) :
    IsPotentialOn (openCubeSet (cubeFaceReflectionCellCube Q choice)) (cubeDirichletOddReflectionHessianRowVectorField Q i fun (y : Vec d) (j : Fin d) => H.hess i j y)

    The global mixed Hessian-row representative is potential on each reflection cell.