Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.FiniteAffineSuccessorDifference

High-contrast homogenization: Provider.Regularity.FiniteAffineSuccessorDifference #

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Successive finite affine solutions #

This module restricts a selected affine solution from one centered cube to its central child, transports the coefficient representative, and subtracts the selected solution on the child cube.

source
theorem HCPolySupport.HighContrast.originCube_mem_descendantsAtDepth_succ {d : ℕ} (m : ℤ) :
originCube d m ∈ descendantsAtDepth (originCube d (m + 1)) 1
source
noncomputable def HCPolySupport.HighContrast.finiteAffineSuccessorRestriction {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e : Vec d) :
Book.Ch03.CubeSolution (originCube d m) a

The scale-m + 1 selected affine solution, restricted to the scale-m centered cube and transported to its coefficient representative.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem HCPolySupport.HighContrast.finiteAffineSuccessorRestriction_toFun {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e : Vec d) :
    (finiteAffineSuccessorRestriction a m e).toH1.toFun = (finiteAffineCubeSolution a (m + 1) e).toH1.toFun

    Restriction preserves the selected outer solution's value representative.

    source
    @[simp]
    theorem HCPolySupport.HighContrast.finiteAffineSuccessorRestriction_grad {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e : Vec d) :
    (finiteAffineSuccessorRestriction a m e).toH1.grad = (finiteAffineCubeSolution a (m + 1) e).toH1.grad

    Restriction preserves the selected outer solution's gradient representative.

    source
    theorem HCPolySupport.HighContrast.cubeSolution_weakFluxIntegrable_finiteAffineSuccessorDifference {d : ℕ} {Q : TriadicCube d} {a : Book.Ch02.TriadicCoeffFamily d} (u : Book.Ch03.CubeSolution Q a) :
    weakFluxIntegrable (Book.Ch02.cubeDomain Q).carrier (a.coeffOn Q).toCoeffField u
    source
    noncomputable def HCPolySupport.HighContrast.finiteAffineSuccessorDifference {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e : Vec d) :
    Book.Ch03.CubeSolution (originCube d m) a

    The restricted scale-m + 1 affine solution minus the scale-m affine solution, as an actual harmonic solution on the scale-m centered cube.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem HCPolySupport.HighContrast.finiteAffineSuccessorDifference_toFun {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e : Vec d) :
      (finiteAffineSuccessorDifference a m e).toH1.toFun = fun (x : Vec d) => (finiteAffineCubeSolution a (m + 1) e).toH1.toFun x - (finiteAffineCubeSolution a m e).toH1.toFun x

      The successor difference has the literal outer-minus-inner value field.

      source
      @[simp]
      theorem HCPolySupport.HighContrast.finiteAffineSuccessorDifference_grad {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e : Vec d) :
      (finiteAffineSuccessorDifference a m e).toH1.grad = fun (x : Vec d) => (finiteAffineCubeSolution a (m + 1) e).toH1.grad x - (finiteAffineCubeSolution a m e).toH1.grad x

      The successor difference has the literal outer-minus-inner gradient field.