Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Foundations.CubeDirichletH2.ReflectionHessianRowFiniteP

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

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

Finite-p transport for mixed-parity Dirichlet reflections #

Differentiating an all-odd scalar reflection in coordinate i changes the cell parity from S to S * s_i. Differentiating once more in coordinate j gives the Hessian-row parity S * s_i * s_j. This file records those pointwise formulas and their exact finite-p norm transport. No weak derivative assertion is made here.

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

The mixed scalar sign S * s_i on one reflection cell.

Equations
Instances For
    source
    @[simp]
    theorem HCPolySupport.cubeDirichletOddReflectionMixedCellSign_apply {d : ℕ} (choice : Fin d → Fin 3) (i : Fin d) :
    cubeDirichletOddReflectionMixedCellSign choice i = cubeDirichletOddReflectionCellSign choice * if choice i = 1 then 1 else -1
    source
    theorem HCPolySupport.cubeDirichletOddReflectionMixedCellSign_mul_self {d : ℕ} (choice : Fin d → Fin 3) (i : Fin d) :
    cubeDirichletOddReflectionMixedCellSign choice i * cubeDirichletOddReflectionMixedCellSign choice i = 1
    source
    theorem HCPolySupport.norm_cubeDirichletOddReflectionMixedCellSign {d : ℕ} (choice : Fin d → Fin 3) (i : Fin d) :
    ‖cubeDirichletOddReflectionMixedCellSign choice i‖ = 1
    source
    noncomputable def HCPolySupport.cubeDirichletOddReflectionGradientCoordCellScalar {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) (i : Fin d) (v : Vec d → ℝ) :
    Vec d → ℝ

    The cellwise mixed reflection of a scalar gradient coordinate.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem HCPolySupport.cubeDirichletOddReflectionGradientCoordCellScalar_apply {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) (i : Fin d) (v : Vec d → ℝ) (x : Vec d) :
      cubeDirichletOddReflectionGradientCoordCellScalar Q choice i v x = (cubeDirichletOddReflectionCellSign choice * if choice i = 1 then 1 else -1) * v (cubeFaceReflectionCellFoldMap Q choice x)
      source
      noncomputable def HCPolySupport.cubeDirichletOddReflectionGradientCoordScalar {d : ℕ} (Q : TriadicCube d) (i : Fin d) (v : Vec d → ℝ) :
      Vec d → ℝ

      The global mixed reflection of a scalar gradient coordinate. Its parity is exactly S * s_i.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem HCPolySupport.cubeDirichletOddReflectionGradientCoordScalar_apply {d : ℕ} (Q : TriadicCube d) (i : Fin d) (v : Vec d → ℝ) (x : Vec d) :
        cubeDirichletOddReflectionGradientCoordScalar Q i v x = cubeDirichletOddReflectionSign Q x * cubeCoordinateFoldSign Q x i * v (cubeCoordinateFold Q x)
        source
        theorem HCPolySupport.cubeDirichletOddReflectionGradientCoordScalar_eq_vectorField_singleCoordinate {d : ℕ} (Q : TriadicCube d) (i : Fin d) (v : Vec d → ℝ) (x : Vec d) :
        cubeDirichletOddReflectionGradientCoordScalar Q i v x = cubeDirichletOddReflectionVectorField Q (fun (y : Vec d) (j : Fin d) => if j = i then v y else 0) x i

        The mixed scalar reflection is the ith coordinate of the odd reflection of the vector field supported in coordinate i.

        source
        noncomputable def HCPolySupport.cubeDirichletOddReflectionHessianRowCellVectorField {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) (i : Fin d) (R : Vec d → Vec d) :
        Vec d → Vec d

        The cellwise mixed reflection of one Hessian row. Its jth coordinate has parity S * s_i * s_j.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem HCPolySupport.cubeDirichletOddReflectionHessianRowCellVectorField_apply {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) (i j : Fin d) (R : Vec d → Vec d) (x : Vec d) :
          cubeDirichletOddReflectionHessianRowCellVectorField Q choice i R x j = ((cubeDirichletOddReflectionCellSign choice * if choice i = 1 then 1 else -1) * if choice j = 1 then 1 else -1) * R (cubeFaceReflectionCellFoldMap Q choice x) j
          source
          noncomputable def HCPolySupport.cubeDirichletOddReflectionHessianRowVectorField {d : ℕ} (Q : TriadicCube d) (i : Fin d) (R : Vec d → Vec d) :
          Vec d → Vec d

          The global mixed reflection of one Hessian row.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem HCPolySupport.cubeDirichletOddReflectionHessianRowVectorField_apply {d : ℕ} (Q : TriadicCube d) (i j : Fin d) (R : Vec d → Vec d) (x : Vec d) :
            cubeDirichletOddReflectionHessianRowVectorField Q i R x j = cubeDirichletOddReflectionSign Q x * cubeCoordinateFoldSign Q x i * cubeCoordinateFoldSign Q x j * R (cubeCoordinateFold Q x) j

            The global Hessian-row formula exposes the exact chain-rule parity S * s_i * s_j.

            source
            theorem HCPolySupport.cubeDirichletOddReflectionGradientCoordScalar_eq_cell_of_mem {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) (i : Fin d) (v : Vec d → ℝ) {x : Vec d} (hx : x ∈ openCubeSet (cubeFaceReflectionCellCube Q choice)) :
            cubeDirichletOddReflectionGradientCoordScalar Q i v x = cubeDirichletOddReflectionGradientCoordCellScalar Q choice i v x

            The global mixed scalar agrees with its affine formula on each reflection cell.

            source
            theorem HCPolySupport.cubeDirichletOddReflectionHessianRowVectorField_eq_cell_of_mem {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) (i : Fin d) (R : Vec d → Vec d) {x : Vec d} (hx : x ∈ openCubeSet (cubeFaceReflectionCellCube Q choice)) :
            cubeDirichletOddReflectionHessianRowVectorField Q i R x = cubeDirichletOddReflectionHessianRowCellVectorField Q choice i R x

            The global mixed Hessian row agrees with its affine formula on each reflection cell.

            source
            theorem HCPolySupport.cubeDirichletOddReflectionGradientCoordScalar_eq_self_of_mem_openCubeSet {d : ℕ} (Q : TriadicCube d) (i : Fin d) (v : Vec d → ℝ) {x : Vec d} (hx : x ∈ openCubeSet Q) :
            cubeDirichletOddReflectionGradientCoordScalar Q i v x = v x

            The mixed scalar is unchanged on the source cube.

            source
            theorem HCPolySupport.cubeDirichletOddReflectionHessianRowVectorField_eq_self_of_mem_openCubeSet {d : ℕ} (Q : TriadicCube d) (i : Fin d) (R : Vec d → Vec d) {x : Vec d} (hx : x ∈ openCubeSet Q) :
            cubeDirichletOddReflectionHessianRowVectorField Q i R x = R x

            The mixed Hessian row is unchanged on the source cube.

            source
            theorem HCPolySupport.norm_cubeDirichletOddReflectionGradientCoordScalar_eq_oddReflection {d : ℕ} (Q : TriadicCube d) (i : Fin d) (v : Vec d → ℝ) (x : Vec d) :
            ‖cubeDirichletOddReflectionGradientCoordScalar Q i v x‖ = ‖cubeDirichletOddReflectionScalar Q v x‖

            The mixed scalar has the same pointwise norm as the all-odd scalar reflection.

            source
            theorem HCPolySupport.norm_hilbertVec_cubeDirichletOddReflectionHessianRowVectorField_eq_oddReflection {d : ℕ} (Q : TriadicCube d) (i : Fin d) (R : Vec d → Vec d) (x : Vec d) :
            ‖HilbertVec.ofVec (cubeDirichletOddReflectionHessianRowVectorField Q i R x)‖ = ‖HilbertVec.ofVec (cubeDirichletOddReflectionVectorField Q R x)‖

            The mixed Hessian row has the same pointwise Euclidean norm as the all-odd vector reflection.

            source
            theorem HCPolySupport.norm_cubeDirichletOddReflectionGradientCoordCellScalar {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) (i : Fin d) (v : Vec d → ℝ) (x : Vec d) :
            ‖cubeDirichletOddReflectionGradientCoordCellScalar Q choice i v x‖ = ‖v (cubeFaceReflectionCellFoldMap Q choice x)‖

            The mixed scalar has the norm of the pulled-back scalar on each cell.

            source
            theorem HCPolySupport.norm_hilbertVec_cubeDirichletOddReflectionHessianRowCellVectorField {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) (i : Fin d) (R : Vec d → Vec d) (x : Vec d) :
            ‖HilbertVec.ofVec (cubeDirichletOddReflectionHessianRowCellVectorField Q choice i R x)‖ = ‖HilbertVec.ofVec (R (cubeFaceReflectionCellFoldMap Q choice x))‖

            The mixed Hessian-row cell formula is a Euclidean isometry.

            Scalar-coordinate finite-p transport #

            source
            theorem HCPolySupport.eLpNorm_cubeFaceReflectionBlockSet_gradientCoordScalar {d : ℕ} (Q : TriadicCube d) (i : Fin d) (v : Vec d → ℝ) (p : FiniteLpExponent) :
            MeasureTheory.eLpNorm (cubeDirichletOddReflectionGradientCoordScalar Q i v) p.exponent (MeasureTheory.volume.restrict (cubeFaceReflectionBlockSet Q)) = (3 ^ d) ^ (1 / p.exponent.toReal) * MeasureTheory.eLpNorm v p.exponent (MeasureTheory.volume.restrict (openCubeSet Q))

            Exact finite-p norm transport for a mixed scalar on the full reflection block.

            source
            theorem HCPolySupport.memLp_cubeFaceReflectionBlockSet_gradientCoordScalar {d : ℕ} {v : Vec d → ℝ} (Q : TriadicCube d) (i : Fin d) (p : FiniteLpExponent) (hv : MeasureTheory.MemLp v p.exponent (MeasureTheory.volume.restrict (openCubeSet Q))) :
            MeasureTheory.MemLp (cubeDirichletOddReflectionGradientCoordScalar Q i v) p.exponent (MeasureTheory.volume.restrict (cubeFaceReflectionBlockSet Q))

            MemLp transport for a mixed scalar on the full reflection block.

            source
            theorem HCPolySupport.eLpNorm_openCubeSet_succ_originCube_gradientCoordScalar {d : ℕ} {m : ℤ} (i : Fin d) (v : Vec d → ℝ) (p : FiniteLpExponent) :
            MeasureTheory.eLpNorm (cubeDirichletOddReflectionGradientCoordScalar (originCube d m) i v) p.exponent (MeasureTheory.volume.restrict (openCubeSet (originCube d (m + 1)))) = (3 ^ d) ^ (1 / p.exponent.toReal) * MeasureTheory.eLpNorm v p.exponent (MeasureTheory.volume.restrict (openCubeSet (originCube d m)))

            Exact unnormalized mixed-scalar norm transport from an origin cube to its centered parent.

            source
            theorem HCPolySupport.memLp_openCubeSet_succ_originCube_gradientCoordScalar {d : ℕ} {m : ℤ} {v : Vec d → ℝ} (i : Fin d) (p : FiniteLpExponent) (hv : MeasureTheory.MemLp v p.exponent (MeasureTheory.volume.restrict (openCubeSet (originCube d m)))) :
            MeasureTheory.MemLp (cubeDirichletOddReflectionGradientCoordScalar (originCube d m) i v) p.exponent (MeasureTheory.volume.restrict (openCubeSet (originCube d (m + 1))))

            MemLp transport for a mixed scalar from an origin cube to its centered parent.

            source
            theorem HCPolySupport.eLpNorm_normalizedCubeMeasure_succ_originCube_gradientCoordScalar {d : ℕ} {m : ℤ} (i : Fin d) (v : Vec d → ℝ) (p : FiniteLpExponent) :
            MeasureTheory.eLpNorm (cubeDirichletOddReflectionGradientCoordScalar (originCube d m) i v) p.exponent (normalizedCubeMeasure (originCube d (m + 1))) = MeasureTheory.eLpNorm v p.exponent (normalizedCubeMeasure (originCube d m))

            Normalized mixed-scalar finite-p norms are exactly preserved from an origin cube to its centered parent.

            source
            theorem HCPolySupport.memLp_normalizedCubeMeasure_succ_originCube_gradientCoordScalar {d : ℕ} {m : ℤ} {v : Vec d → ℝ} (i : Fin d) (p : FiniteLpExponent) (hv : MeasureTheory.MemLp v p.exponent (normalizedCubeMeasure (originCube d m))) :
            MeasureTheory.MemLp (cubeDirichletOddReflectionGradientCoordScalar (originCube d m) i v) p.exponent (normalizedCubeMeasure (originCube d (m + 1)))

            Normalized MemLp is preserved by the mixed-scalar origin-cube reflection.

            Hessian-row finite-p transport #

            source
            theorem HCPolySupport.eLpNorm_cubeFaceReflectionBlockSet_hessianRowVectorField {d : ℕ} (Q : TriadicCube d) (i : Fin d) (R : Vec d → Vec d) (p : FiniteLpExponent) :
            MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (cubeDirichletOddReflectionHessianRowVectorField Q i R x)) p.exponent (MeasureTheory.volume.restrict (cubeFaceReflectionBlockSet Q)) = (3 ^ d) ^ (1 / p.exponent.toReal) * MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (R x)) p.exponent (MeasureTheory.volume.restrict (openCubeSet Q))

            Exact Euclidean finite-p norm transport for a mixed Hessian row on the full reflection block.

            source
            theorem HCPolySupport.memLp_cubeFaceReflectionBlockSet_hessianRowVectorField {d : ℕ} {R : Vec d → Vec d} (Q : TriadicCube d) (i : Fin d) (p : FiniteLpExponent) (hR : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (R x)) p.exponent (MeasureTheory.volume.restrict (openCubeSet Q))) :
            MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (cubeDirichletOddReflectionHessianRowVectorField Q i R x)) p.exponent (MeasureTheory.volume.restrict (cubeFaceReflectionBlockSet Q))

            Euclidean MemLp transport for a mixed Hessian row on the full reflection block.

            source
            theorem HCPolySupport.eLpNorm_openCubeSet_succ_originCube_hessianRowVectorField {d : ℕ} {m : ℤ} (i : Fin d) (R : Vec d → Vec d) (p : FiniteLpExponent) :
            MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (cubeDirichletOddReflectionHessianRowVectorField (originCube d m) i R x)) p.exponent (MeasureTheory.volume.restrict (openCubeSet (originCube d (m + 1)))) = (3 ^ d) ^ (1 / p.exponent.toReal) * MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (R x)) p.exponent (MeasureTheory.volume.restrict (openCubeSet (originCube d m)))

            Exact unnormalized Euclidean norm transport for a mixed Hessian row from an origin cube to its centered parent.

            source
            theorem HCPolySupport.memLp_openCubeSet_succ_originCube_hessianRowVectorField {d : ℕ} {m : ℤ} {R : Vec d → Vec d} (i : Fin d) (p : FiniteLpExponent) (hR : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (R x)) p.exponent (MeasureTheory.volume.restrict (openCubeSet (originCube d m)))) :
            MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (cubeDirichletOddReflectionHessianRowVectorField (originCube d m) i R x)) p.exponent (MeasureTheory.volume.restrict (openCubeSet (originCube d (m + 1))))

            Euclidean MemLp transport for a mixed Hessian row from an origin cube to its centered parent.

            source
            theorem HCPolySupport.eLpNorm_normalizedCubeMeasure_succ_originCube_hessianRowVectorField {d : ℕ} {m : ℤ} (i : Fin d) (R : Vec d → Vec d) (p : FiniteLpExponent) :
            MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (cubeDirichletOddReflectionHessianRowVectorField (originCube d m) i R x)) p.exponent (normalizedCubeMeasure (originCube d (m + 1))) = MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (R x)) p.exponent (normalizedCubeMeasure (originCube d m))

            Normalized Euclidean finite-p Hessian-row norms are exactly preserved from an origin cube to its centered parent.

            source
            theorem HCPolySupport.memLp_normalizedCubeMeasure_succ_originCube_hessianRowVectorField {d : ℕ} {m : ℤ} {R : Vec d → Vec d} (i : Fin d) (p : FiniteLpExponent) (hR : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (R x)) p.exponent (normalizedCubeMeasure (originCube d m))) :
            MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (cubeDirichletOddReflectionHessianRowVectorField (originCube d m) i R x)) p.exponent (normalizedCubeMeasure (originCube d (m + 1)))

            Normalized Euclidean MemLp is preserved by the mixed Hessian-row origin-cube reflection.