Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section5.LeftToShow.TimeIBP.EntryBound

Entrywise integration by parts in time #

Source: enhance.tex 8780–8830. For each pair (i,j) the function A_ij(t) = ∫_{𝕋²} βˆ‚_iT βˆ‚_jT is continuous on [0,1], differentiable on (0,1) with derivative ∫ (D_tβˆ‚_iT βˆ‚_jT + βˆ‚_iT D_tβˆ‚_jT), and ∫_0^1 |A_ij'| ≀ 2 β€–βˆ‡Tβ€–_{LΒ²} β€–D_tβˆ‡Tβ€–_{LΒ²}. Combined with the abstract time integration by parts this bounds |∫_0^1 G A_ij| for mean-zero periodic G.

source
noncomputable def AVenhance.Infra.Section5.LeftToShow.gradProd (T : ℝ β†’ Homogenization.Vec 2 β†’ ℝ) (i j : Fin 2) (t : ℝ) :
ℝ

A_ij(t) = ∫_{𝕋²} βˆ‚_iT βˆ‚_jT.

Equations
Instances For
    source
    noncomputable def AVenhance.Infra.Section5.LeftToShow.gradProdDeriv (b : ℝ β†’ Homogenization.Vec 2 β†’ Homogenization.Vec 2) (T : ℝ β†’ Homogenization.Vec 2 β†’ ℝ) (i j : Fin 2) (t : ℝ) :
    ℝ

    The derivative ∫ (D_tβˆ‚_iT βˆ‚_jT + βˆ‚_iT D_tβˆ‚_jT) of A_ij (with the continuous extension of D_tβˆ‡T to t = 0).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def AVenhance.Infra.Section5.LeftToShow.matGradVec (b : ℝ β†’ Homogenization.Vec 2 β†’ Homogenization.Vec 2) (T : ℝ β†’ Homogenization.Vec 2 β†’ ℝ) (t : ℝ) (x : Homogenization.Vec 2) :
      Homogenization.Vec 2

      The vector field D_tβˆ‡T extended continuously to t = 0.

      Equations
      Instances For
        source
        theorem AVenhance.Infra.Section5.LeftToShow.icc_prod_subset_halfSpace :
        Set.Icc 0 1 Γ—Λ’ Set.univ βŠ† halfSpace
        source
        theorem AVenhance.Infra.Section5.LeftToShow.gradCoord_continuousOn_Icc {T : ℝ β†’ Homogenization.Vec 2 β†’ ℝ} (hT : ContDiffOn ℝ (β†‘βŠ€) (fun (p : ℝ Γ— Homogenization.Vec 2) => T p.1 p.2) halfSpace) (i : Fin 2) :
        ContinuousOn (gradCoord T i) (Set.Icc 0 1 Γ—Λ’ Set.univ)
        source
        theorem AVenhance.Infra.Section5.LeftToShow.matGradVec_continuousOn {b : ℝ β†’ Homogenization.Vec 2 β†’ Homogenization.Vec 2} {T : ℝ β†’ Homogenization.Vec 2 β†’ ℝ} (hb : Flow.SmoothPeriodicField b) (hT : ContDiffOn ℝ (β†‘βŠ€) (fun (p : ℝ Γ— Homogenization.Vec 2) => T p.1 p.2) halfSpace) :
        ContinuousOn (fun (p : ℝ Γ— Homogenization.Vec 2) => matGradVec b T p.1 p.2) (Set.Icc 0 1 Γ—Λ’ Set.univ)
        source
        theorem AVenhance.Infra.Section5.LeftToShow.EntryBound.timeCube_measurable :
        MeasurableSet timeCube
        source
        theorem AVenhance.Infra.Section5.LeftToShow.spaceTimeGradNormSq_materialGrad_eq {b : ℝ β†’ Homogenization.Vec 2 β†’ Homogenization.Vec 2} {T : ℝ β†’ Homogenization.Vec 2 β†’ ℝ} :
        spaceTimeGradNormSq (materialGrad b T) = spaceTimeGradNormSq (matGradVec b T)

        The norm of D_tβˆ‡T equals that of its continuous extension.

        source
        theorem AVenhance.Infra.Section5.LeftToShow.abs_apply_le_sqrt_vecNormSq (v : Homogenization.Vec 2) (i : Fin 2) :
        |v i| ≀ √(Homogenization.vecNormSq v)
        source
        theorem AVenhance.Infra.Section5.LeftToShow.continuousOn_energy {V : ℝ β†’ Homogenization.Vec 2 β†’ Homogenization.Vec 2} (hV : ContinuousOn (fun (p : ℝ Γ— Homogenization.Vec 2) => V p.1 p.2) (Set.Icc 0 1 Γ—Λ’ Set.univ)) :
        ContinuousOn (fun (t : ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (V t x)) (Set.Icc 0 1)

        Continuity in time of the spatial energy of a jointly continuous field.

        source
        theorem AVenhance.Infra.Section5.LeftToShow.integral_sqrt_mul_sqrt_le {a c : ℝ β†’ ℝ} (ha : ContinuousOn a (Set.Icc 0 1)) (hc : ContinuousOn c (Set.Icc 0 1)) (ha0 : βˆ€ t ∈ Set.Icc 0 1, 0 ≀ a t) (hc0 : βˆ€ t ∈ Set.Icc 0 1, 0 ≀ c t) :
        ∫ (t : ℝ) in 0..1, √(a t) * √(c t) ≀ √(∫ (t : ℝ) in 0..1, a t) * √(∫ (t : ℝ) in 0..1, c t)

        Cauchy–Schwarz in time for continuous nonnegative energies.

        source
        theorem AVenhance.Infra.Section5.LeftToShow.integral_unitCube_mul_le {f g : Homogenization.Vec 2 β†’ ℝ} (hf : Continuous f) (hg : Continuous g) :
        ∫ (x : Homogenization.Vec 2) in unitCube, f x * g x ≀ √(∫ (x : Homogenization.Vec 2) in unitCube, f x ^ 2) * √(∫ (x : Homogenization.Vec 2) in unitCube, g x ^ 2)

        Cauchy–Schwarz on the unit cube for continuous functions.

        source
        theorem AVenhance.Infra.Section5.LeftToShow.vecNormSq_nonneg' (v : Homogenization.Vec 2) :
        0 ≀ Homogenization.vecNormSq v
        source
        theorem AVenhance.Infra.Section5.LeftToShow.abs_gradProdDeriv_le {b : ℝ β†’ Homogenization.Vec 2 β†’ Homogenization.Vec 2} {T : ℝ β†’ Homogenization.Vec 2 β†’ ℝ} (hb : Flow.SmoothPeriodicField b) (hT : ContDiffOn ℝ (β†‘βŠ€) (fun (p : ℝ Γ— Homogenization.Vec 2) => T p.1 p.2) halfSpace) {t : ℝ} (ht : t ∈ Set.Icc 0 1) (i j : Fin 2) :
        |gradProdDeriv b T i j t| ≀ 2 * (√(∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (matGradVec b T t x)) * √(∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad (T t) x)))

        Time-slice bound |A_ij'(t)| ≀ 2 β€–D_tβˆ‡T(t)β€–_{LΒ²(𝕋²)} β€–βˆ‡T(t)β€–_{LΒ²(𝕋²)}.

        source
        theorem AVenhance.Infra.Section5.LeftToShow.gradProdDeriv_continuousOn {b : ℝ β†’ Homogenization.Vec 2 β†’ Homogenization.Vec 2} {T : ℝ β†’ Homogenization.Vec 2 β†’ ℝ} (hb : Flow.SmoothPeriodicField b) (hT : ContDiffOn ℝ (β†‘βŠ€) (fun (p : ℝ Γ— Homogenization.Vec 2) => T p.1 p.2) halfSpace) (i j : Fin 2) :
        ContinuousOn (gradProdDeriv b T i j) (Set.Icc 0 1)
        source
        theorem AVenhance.Infra.Section5.LeftToShow.intervalIntegral_abs_gradProdDeriv_le {b : ℝ β†’ Homogenization.Vec 2 β†’ Homogenization.Vec 2} {T : ℝ β†’ Homogenization.Vec 2 β†’ ℝ} (hb : Flow.SmoothPeriodicField b) (hT : ContDiffOn ℝ (β†‘βŠ€) (fun (p : ℝ Γ— Homogenization.Vec 2) => T p.1 p.2) halfSpace) (i j : Fin 2) :
        ∫ (t : ℝ) in 0..1, |gradProdDeriv b T i j t| ≀ 2 * (√(spaceTimeGradNormSq (materialGrad b T)) * √(spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (T t) x))

        ∫_0^1 |A_ij'| ≀ 2 β€–D_tβˆ‡Tβ€–_{LΒ²((0,1)×𝕋²)} β€–βˆ‡Tβ€–_{LΒ²((0,1)×𝕋²)}.