duhamelRemainderOfGalerkin_kernel

proof body

Body contains sorry. Scaffold only; not proved.

 530    (hint :
 531      IntervalIntegrable (fun s : ℝ =>
 532        (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero (B (u s) (u s)) k))
 533        MeasureTheory.volume 0 t) :
 534    duhamelRemainderOfGalerkin (N := N) ν u t k
 535      =
 536        -∫ s in (0 : ℝ)..t, (heatFactor ν (t - s) k) • (extendByZero (B (u s) (u s)) k) := by
 537  -- Start from the integrating-factor identity.
 538  have hIF :=
 539    duhamelRemainderOfGalerkin_integratingFactor (N := N) (ν := ν) (B := B) (u := u) (k := k) (t := t) hu hint
 540
 541  -- Multiply both sides by the heat factor at time `t` to cancel the integrating factor.
 542  have hmul : (heatFactor ν t k) • ((Real.exp (-(ν * (-kSq k)) * t)) • duhamelRemainderOfGalerkin (N := N) ν u t k)
 543      =
 544        (heatFactor ν t k) • (-∫ s in (0 : ℝ)..t,
 545          (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero (B (u s) (u s)) k)) := by
 546    simpa using congrArg (fun v => (heatFactor ν t k) • v) hIF
 547
 548  -- Simplify the left-hand side: `heatFactor(t) * exp(ν|k|^2 t) = 1`.
 549  have hcancel :
 550      (heatFactor ν t k) • ((Real.exp (-(ν * (-kSq k)) * t)) • duhamelRemainderOfGalerkin (N := N) ν u t k)
 551        = duhamelRemainderOfGalerkin (N := N) ν u t k := by
 552    -- turn nested smul into product scalar
 553    have hprod : (heatFactor ν t k) * (Real.exp (-(ν * (-kSq k)) * t)) = 1 := by
 554      calc
 555        (heatFactor ν t k) * (Real.exp (-(ν * (-kSq k)) * t))
 556            = Real.exp (-ν * kSq k * t) * Real.exp (ν * kSq k * t) := by
 557                simp [heatFactor]
 558        _ = Real.exp ((-ν * kSq k * t) + (ν * kSq k * t)) := (Real.exp_add _ _).symm
 559        _ = Real.exp 0 := by ring_nf
 560        _ = 1 := by simp
 561    calc
 562      (heatFactor ν t k) • ((Real.exp (-(ν * (-kSq k)) * t)) • duhamelRemainderOfGalerkin (N := N) ν u t k)
 563          = ((heatFactor ν t k) * (Real.exp (-(ν * (-kSq k)) * t))) • duhamelRemainderOfGalerkin (N := N) ν u t k := by
 564              simp [smul_smul]
 565      _ = (1 : ℝ) • duhamelRemainderOfGalerkin (N := N) ν u t k := by
 566            -- avoid `simp` rewriting the exponential before applying `hprod`
 567            rw [hprod]
 568      _ = duhamelRemainderOfGalerkin (N := N) ν u t k := by simp
 569
 570  -- Move the scalar inside the integral, then combine the exponentials into `heatFactor ν (t - s) k`.
 571  have hRHS :
 572      (heatFactor ν t k) • (-∫ s in (0 : ℝ)..t,
 573          (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero (B (u s) (u s)) k))
 574        =
 575        -∫ s in (0 : ℝ)..t, (heatFactor ν (t - s) k) • (extendByZero (B (u s) (u s)) k) := by
 576    -- Let `f(s)` be the integrand in the integrating-factor identity.
 577    let f : ℝ → VelCoeff :=
 578      fun s => (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero (B (u s) (u s)) k)
 579    -- First move the scalar inside the integral.
 580    have hsmul :
 581        (heatFactor ν t k) • (∫ s in (0 : ℝ)..t, f s) =
 582          ∫ s in (0 : ℝ)..t, (heatFactor ν t k) • (f s) := by
 583      simp [f]
 584    -- Rewrite `heatFactor ν t k • (-∫ f)` as `-∫ (heatFactor ν t k • f)`.
 585    have hneg :
 586        (heatFactor ν t k) • (-∫ s in (0 : ℝ)..t, f s)
 587          = -∫ s in (0 : ℝ)..t, (heatFactor ν t k) • (f s) := by
 588      calc
 589        (heatFactor ν t k) • (-∫ s in (0 : ℝ)..t, f s)
 590            = -((heatFactor ν t k) • (∫ s in (0 : ℝ)..t, f s)) := by simp [smul_neg]
 591        _ = -(∫ s in (0 : ℝ)..t, (heatFactor ν t k) • (f s)) := by rw [hsmul]
 592        _ = -∫ s in (0 : ℝ)..t, (heatFactor ν t k) • (f s) := rfl
 593    -- Now simplify the integrand pointwise on the integration interval.
 594    have hEqOn :
 595        Set.EqOn (fun s => (heatFactor ν t k) • (f s))
 596          (fun s => (heatFactor ν (t - s) k) • (extendByZero (B (u s) (u s)) k)) (Set.uIcc (0 : ℝ) t) := by
 597      intro s _hs
 598      -- combine scalar factors into `heatFactor ν (t - s) k`
 599      have hscalar :
 600          (heatFactor ν t k) * (Real.exp (-(ν * (-kSq k)) * s)) = heatFactor ν (t - s) k := by
 601        calc
 602          (heatFactor ν t k) * (Real.exp (-(ν * (-kSq k)) * s))
 603              = Real.exp (-ν * kSq k * t) * Real.exp (ν * kSq k * s) := by
 604                  simp [heatFactor]
 605          _ = Real.exp ((-ν * kSq k * t) + (ν * kSq k * s)) := (Real.exp_add _ _).symm
 606          _ = Real.exp (-ν * kSq k * (t - s)) := by ring_nf
 607          _ = heatFactor ν (t - s) k := by simp [heatFactor]
 608      -- use the scalar identity to rewrite the smul
 609      calc
 610-- ... 46 more lines elided ...