Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Parabolic.FourierGalerkin.LimitRepresentation

Physical representatives of weak scalar paths #

Pulling a torus L² class back to the Euclidean covering space gives a periodic representative with the exact unit-cell L² norm. These bridges are the pointwise-in-time part of the eventual IsWeakSolutionGrad assembly.

source
@[instance_reducible]
noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.representationMeasureSpaceUnitAddCircle :
MeasureTheory.MeasureSpace UnitAddCircle

Use normalized Haar measure on the unit circle for periodic integrals.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem AVenhance.Infra.Parabolic.FourierGalerkin.representationMeasureIsAddHaarUnitAddCircle :
    MeasureTheory.volume.IsAddHaarMeasure
    source
    theorem AVenhance.Infra.Parabolic.FourierGalerkin.representationProbabilityUnitAddCircle :
    MeasureTheory.IsProbabilityMeasure MeasureTheory.volume
    source
    def AVenhance.Infra.Parabolic.FourierGalerkin.LimitRepresentation.representationClosedCell :
    Set (Homogenization.Vec 2)

    Closed spatial unit cell used for compactness and periodic integration.

    Equations
    Instances For
      source
      theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitRepresentation.representationClosedCell_compact :
      IsCompact representationClosedCell
      source
      theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitRepresentation.unitCube_subset_representationClosedCell :
      unitCube ⊆ representationClosedCell
      source
      theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitRepresentation.smoothPeriodicTest_memL2On {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) :
      Homogenization.MemL2On unitCube ψ
      source
      noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.smoothPeriodicTestL2 {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (_hperiodic : IsZ2Periodic ψ) :
      ↥ScalarTorusL2

      The torus L² class associated with a smooth periodic Euclidean test function.

      Equations
      Instances For
        source
        noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.scalarTorusRepresentative (f : ↥ScalarTorusL2) :
        Homogenization.Vec 2 → ℝ

        The canonical periodic representative of a real torus L² class.

        Equations
        Instances For
          source
          theorem AVenhance.Infra.Parabolic.FourierGalerkin.scalarTorusRepresentative_periodic (f : ↥ScalarTorusL2) :
          IsZ2Periodic (scalarTorusRepresentative f)
          source
          theorem AVenhance.Infra.Parabolic.FourierGalerkin.scalarTorusRepresentative_memL2On (f : ↥ScalarTorusL2) :
          Homogenization.MemL2On unitCube (scalarTorusRepresentative f)

          A torus L² class pulls back to the open-cell L² carrier.

          source
          theorem AVenhance.Infra.Parabolic.FourierGalerkin.scalarTorusRepresentative_l2NormSq (f : ↥ScalarTorusL2) :
          l2NormSq (scalarTorusRepresentative f) = ‖f‖ ^ 2

          The l2NormSq of a pulled-back torus class is its Hilbert norm squared.

          source
          noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.weakPathRepresentative (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) :
          ℝ → Homogenization.Vec 2 → ℝ

          The weakly continuous torus path, represented periodically at every real time. Outside the closed solution interval its representative is set to zero.

          Equations
          Instances For
            source
            theorem AVenhance.Infra.Parabolic.FourierGalerkin.weakPathRepresentative_isPeriodic (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (t : ℝ) :
            IsZ2Periodic (weakPathRepresentative u t)
            source
            theorem AVenhance.Infra.Parabolic.FourierGalerkin.weakPathRepresentative_memL2On (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (t : ↑(Set.Icc 0 1)) :
            Homogenization.MemL2On unitCube (weakPathRepresentative u ↑t)
            source
            theorem AVenhance.Infra.Parabolic.FourierGalerkin.weakPathRepresentative_l2NormSq (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (t : ↑(Set.Icc 0 1)) :
            l2NormSq (weakPathRepresentative u ↑t) = ‖u t‖ ^ 2
            source
            theorem AVenhance.Infra.Parabolic.FourierGalerkin.weakPathRepresentative_pairing_eq_inner (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (t : ↑(Set.Icc 0 1)) {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hperiodic : IsZ2Periodic ψ) :
            ∫ (x : Homogenization.Vec 2) in unitCube, weakPathRepresentative u (↑t) x * ψ x = inner ℝ (u t) (smoothPeriodicTestL2 hψ hperiodic)

            Pairing the physical representative with a smooth periodic test is exactly the torus Hilbert pairing.

            source
            theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.initial_pairing_eq_cell_integral (P : FrozenDriftProblem) {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hperiodic : IsZ2Periodic ψ) :
            inner ℝ P.initialTorusL2 (smoothPeriodicTestL2 hψ hperiodic) = ∫ (x : Homogenization.Vec 2) in unitCube, P.θ₀ x * ψ x

            The datum and its torus L² class have the same pairing with every smooth periodic test.

            source
            theorem AVenhance.Infra.Parabolic.FourierGalerkin.weakPathRepresentative_testPairing_continuous (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (hweakContinuous : ∀ (v : ↥ScalarTorusL2), Continuous fun (t : ↑(Set.Icc 0 1)) => inner ℝ (u t) v) {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hperiodic : IsZ2Periodic ψ) :
            ContinuousOn (fun (t : ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, weakPathRepresentative u t x * ψ x) (Set.Icc 0 1)

            Smooth-test pairings of the physical weak path are continuous on the closed time interval.