import KN.SourceSurplus

set_option linter.unusedSectionVars false

/-!
# Projection, overlap, and fixed-minimum inequality for an arbitrary source

This module proves the arbitrary-source projection and overlap lemmas and assembles the
set-source fixed-minimum inequality used by Question 9.
-/

noncomputable section

namespace KNAll.Guarded

open MeasureTheory Set Percolation.Literature.LatticeModels Percolation.Literature
open Percolation.Continuity Percolation.Continuity.CSH
open scoped Classical

variable {V : Type*} [Fintype V]

/-- The arbitrary finite-source fixed-minimizer integral. -/
def sourceFixedMinGap (w : Sym2 V → unitInterval) (A S : Finset V)
    (a : V) (F : Set V → ℝ) : ℝ :=
  ∫ omega in sourceAvoid (↑S : Set V) ({a} : Set V) ∩
      sourceConn (↑S : Set V) (↑(A.erase a) : Set V),
    (F (sourceCluster omega (↑S : Set V)) - F (openCluster omega a))
      ∂(prodBernoulli w)

/-! ## Complete-source-cluster projection -/

private theorem sourceCluster_eq_setCl_span_local (omega : BondConfig V) (O : Set V) :
    sourceCluster omega O =
      {x | x ∈ O ∨ ∃ e ∈ BHK2006.setCl omega O, x ∈ e} := by
  ext x
  simp only [sourceCluster, mem_iUnion,
    KNPreFKG.openCluster_eq_setOf_openEdgeCluster, mem_setOf_eq,
    BHK2006.mem_setCl_iff]
  constructor
  · rintro ⟨r, hrO, rfl | ⟨e, he, hxe⟩⟩
    · exact Or.inl hrO
    · exact Or.inr ⟨e, ⟨r, hrO, he⟩, hxe⟩
  · rintro (hxO | ⟨e, ⟨r, hrO, he⟩, hxe⟩)
    · exact ⟨x, hxO, Or.inl rfl⟩
    · exact ⟨r, hrO, Or.inr ⟨e, he, hxe⟩⟩

private theorem barOf_source_eq_bar (omega : BondConfig V) (O : Set V) :
    BHK2006.barOf O (BHK2006.setCl omega O) =
      bar (sourceCluster omega O) := by
  rw [BHK2006.barOf_setCl_eq]
  ext e
  simp only [bar, sourceCluster, mem_setOf_eq, mem_iUnion]
  constructor
  · rintro ⟨x, hxe, r, hrO, hrx⟩
    exact ⟨x, hxe, r, hrO, hrx⟩
  · rintro ⟨x, hxe, r, hrO, hrx⟩
    exact ⟨x, hxe, r, hrO, hrx⟩

/-- Tower property after exploring the complete edge cluster generated by an arbitrary
source. -/
private theorem tower_sourceCluster (w : Sym2 V → unitInterval) (O : Set V) (a : V)
    (F : Set V → ℝ) (calS : Set (Set (Sym2 V))) :
    (∫ omega in sourceAvoid O ({a} : Set V) ∩
          {omega | BHK2006.setCl omega O ∈ calS},
        F (openCluster omega a) ∂(prodBernoulli w)) =
      ∫ omega in sourceAvoid O ({a} : Set V) ∩
          {omega | BHK2006.setCl omega O ∈ calS},
        (∫ eta, F (openCluster (eta \ bar (sourceCluster omega O)) a)
          ∂(prodBernoulli w)) ∂(prodBernoulli w) := by
  classical
  set mu := prodBernoulli w with hmu
  set D : Set (BondConfig V) := sourceAvoid O ({a} : Set V) with hD
  have hDiff : ∀ omega : BondConfig V, omega ∈ D ↔
      ∀ s ∈ O, ∀ t ∈ ({a} : Set V),
        ¬ (openGraph omega).Reachable s t := by
    intro omega
    rw [hD]
    rfl
  have hm : ∑ omega : Set (Sym2 V),
      BHK2006.weight (fun e => (w e : ℝ)) omega = 1 := by
    have h1 := BHK2006.integral_prodBernoulli_eq_sum w fun _ => (1 : ℝ)
    simp only [integral_const, probReal_univ, smul_eq_mul, mul_one] at h1
    exact h1.symm
  have key := BHK2006.set_sum_cond_cluster (fun e => (w e : ℝ)) hm
    O ({a} : Set V)
    (fun K L => Percolation.Literature.DecisionTree.ind calS K *
      F {z | z = a ∨ ∃ e ∈ L, z ∈ e}) hDiff
  simp only [BHK2006.setCl_singleton] at key
  have hvert : ∀ eta : BondConfig V,
      F {z | z = a ∨ ∃ e ∈ openEdgeCluster eta a, z ∈ e} =
        F (openCluster eta a) :=
    fun eta => KNPreFKG.clusterFun_openEdgeCluster F eta a
  simp only [hvert] at key
  rw [← integral_indicator (MeasurableSet.of_discrete),
    ← integral_indicator (MeasurableSet.of_discrete),
    BHK2006.integral_prodBernoulli_eq_sum,
    BHK2006.integral_prodBernoulli_eq_sum]
  have hL : ∀ omega : BondConfig V,
      (D ∩ {omega | BHK2006.setCl omega O ∈ calS}).indicator
          (fun omega => F (openCluster omega a)) omega =
        Percolation.Literature.DecisionTree.ind calS
            (BHK2006.setCl omega O) *
          F (openCluster omega a) *
            Percolation.Literature.DecisionTree.ind D omega := by
    intro omega
    by_cases h1 : omega ∈ D
    · by_cases h2 : BHK2006.setCl omega O ∈ calS
      · rw [indicator_of_mem (show omega ∈ D ∩
            {omega | BHK2006.setCl omega O ∈ calS} from ⟨h1, h2⟩),
          Percolation.Literature.DecisionTree.ind_of_mem h1,
          Percolation.Literature.DecisionTree.ind_of_mem h2]
        ring
      · rw [indicator_of_notMem (fun h => h2 h.2),
          Percolation.Literature.DecisionTree.ind_of_not_mem h2]
        ring
    · rw [indicator_of_notMem (fun h => h1 h.1),
        Percolation.Literature.DecisionTree.ind_of_not_mem h1]
      ring
  have hR : ∀ omega : BondConfig V,
      (D ∩ {omega | BHK2006.setCl omega O ∈ calS}).indicator
          (fun omega => ∫ eta,
            F (openCluster (eta \ BHK2006.barOf O
              (BHK2006.setCl omega O)) a) ∂mu) omega =
        (∑ eta : Set (Sym2 V), BHK2006.weight (fun e => (w e : ℝ)) eta *
          (Percolation.Literature.DecisionTree.ind calS
              (BHK2006.setCl omega O) *
            F (openCluster (eta \ BHK2006.barOf O
              (BHK2006.setCl omega O)) a))) *
          Percolation.Literature.DecisionTree.ind D omega := by
    intro omega
    have hint : (∫ eta,
          F (openCluster (eta \ BHK2006.barOf O
            (BHK2006.setCl omega O)) a) ∂mu) =
        ∑ eta : Set (Sym2 V), BHK2006.weight (fun e => (w e : ℝ)) eta *
          F (openCluster (eta \ BHK2006.barOf O
            (BHK2006.setCl omega O)) a) :=
      BHK2006.integral_prodBernoulli_eq_sum w _
    by_cases h1 : omega ∈ D
    · by_cases h2 : BHK2006.setCl omega O ∈ calS
      · rw [indicator_of_mem (show omega ∈ D ∩
            {omega | BHK2006.setCl omega O ∈ calS} from ⟨h1, h2⟩),
          Percolation.Literature.DecisionTree.ind_of_mem h1,
          Percolation.Literature.DecisionTree.ind_of_mem h2, hint]
        simp only [one_mul, mul_one]
      · rw [indicator_of_notMem (fun h => h2 h.2),
          Percolation.Literature.DecisionTree.ind_of_not_mem h2]
        simp only [zero_mul, mul_zero, Finset.sum_const_zero]
    · rw [indicator_of_notMem (fun h => h1 h.1),
        Percolation.Literature.DecisionTree.ind_of_not_mem h1]
      ring
  simp_rw [← barOf_source_eq_bar]
  simp only [hL, hR]
  exact key

private theorem setIntegral_sub_eq_projFunA_source_setCl
    (w : Sym2 V → unitInterval) (O : Set V) (a : V)
    (F : Set V → ℝ) (calS : Set (Set (Sym2 V))) :
    (∫ omega in sourceAvoid O ({a} : Set V) ∩
          {omega | BHK2006.setCl omega O ∈ calS},
        (F (sourceCluster omega O) - F (openCluster omega a))
          ∂(prodBernoulli w)) =
      ∫ omega in sourceAvoid O ({a} : Set V) ∩
          {omega | BHK2006.setCl omega O ∈ calS},
        projFunA w a F (sourceCluster omega O) ∂(prodBernoulli w) := by
  simp only [projFunA]
  rw [integral_sub (Integrable.of_finite).integrableOn
      (Integrable.of_finite).integrableOn,
    integral_sub (Integrable.of_finite).integrableOn
      (Integrable.of_finite).integrableOn,
    tower_sourceCluster]

/-- Projection identity on source avoidance plus source contact. -/
theorem setIntegral_sub_eq_projFunA_source_conn
    (w : Sym2 V → unitInterval) (O : Set V) (a : V)
    (F : Set V → ℝ) (T : Finset V) :
    (∫ omega in sourceAvoid O ({a} : Set V) ∩
        sourceConn O (↑T : Set V),
      (F (sourceCluster omega O) - F (openCluster omega a))
        ∂(prodBernoulli w)) =
      ∫ omega in sourceAvoid O ({a} : Set V) ∩
          sourceConn O (↑T : Set V),
        projFunA w a F (sourceCluster omega O) ∂(prodBernoulli w) := by
  let calS : Set (Set (Sym2 V)) :=
    {K | ∃ t ∈ T, t ∈ O ∨ ∃ e ∈ K, t ∈ e}
  have hcluster : {omega : BondConfig V |
      BHK2006.setCl omega O ∈ calS} = sourceConn O (↑T : Set V) := by
    ext omega
    simp only [calS, sourceConn, mem_setOf_eq, Finset.mem_coe]
    constructor
    · rintro ⟨t, htT, htO | ⟨e, he, hte⟩⟩
      · exact ⟨t, htO, t, htT, SimpleGraph.Reachable.refl t⟩
      · obtain ⟨s, hsO, hse⟩ := (BHK2006.mem_setCl_iff omega O e).1 he
        exact ⟨s, hsO, t, htT,
          (reachable_iff_exists_mem_openEdgeCluster omega s t).2
            (Or.inr ⟨e, hse, hte⟩)⟩
    · rintro ⟨s, hsO, t, htT, hst⟩
      rcases (reachable_iff_exists_mem_openEdgeCluster omega s t).1 hst with
        hts | ⟨e, he, hte⟩
      · exact ⟨t, htT, Or.inl (hts ▸ hsO)⟩
      · exact ⟨t, htT, Or.inr ⟨e,
          (BHK2006.mem_setCl_iff omega O e).2 ⟨s, hsO, he⟩, hte⟩⟩
  rw [← hcluster]
  exact setIntegral_sub_eq_projFunA_source_setCl w O a F calS

/-! ## Source overlap -/

/-- Conditional-positive-association overlap lemma for an arbitrary source containing `s`. -/
theorem source_overlap (w : Sym2 V → unitInterval) (O : Set V)
    (s a : V) (F : Set V → ℝ) (hsO : s ∈ O) (hF : Monotone F)
    (hmin : (∫ omega, F (openCluster omega a) ∂(prodBernoulli w)) ≤
      ∫ omega, F (openCluster omega s) ∂(prodBernoulli w)) :
    0 ≤ ∫ omega in sourceAvoid O ({a} : Set V),
      (F (sourceCluster omega O) - F (openCluster omega a))
        ∂(prodBernoulli w) := by
  classical
  by_cases has : a = s
  · subst a
    have hempty : sourceAvoid O ({s} : Set V) =
        (∅ : Set (BondConfig V)) := by
      ext omega
      constructor
      · intro homega
        exact False.elim (homega s hsO s (by simp)
          (SimpleGraph.Reachable.refl s))
      · simp
    rw [hempty]
    simp
  set mu := prodBernoulli w with hmu
  set D : Set (BondConfig V) := sourceAvoid ({s} : Set V) ({a} : Set V)
    with hD
  set J : Set (BondConfig V) := sourceAvoid O ({a} : Set V) with hJ
  let p : Set (Sym2 V) → ℝ := fun K =>
    projFunA w a F (insert s {u | ∃ e ∈ K, u ∈ e})
  let q : Set (Sym2 V) → ℝ := fun K =>
    sourceKernel w Set.univ O ({a} : Set V)
      (insert s {u | ∃ e ∈ K, u ∈ e})
  have hpmono : Monotone p := by
    exact KNPreFKG.monotone_clusterFun s (projFunA w a F)
      (monotone_projFunA w a F hF)
  have hqmono : Monotone q := by
    intro K K' hKK'
    apply KNAll.Guarded.sourceKernel_mono_cluster w Set.univ O ({a} : Set V)
    · intro u hu
      rcases hu with rfl | ⟨e, he, hue⟩
      · exact Or.inl rfl
      · exact Or.inr ⟨e, hKK' he, hue⟩
    · exact Set.subset_univ _
  have hBHK := BHK2006_clusterConditionalPositiveAssociation_holds
    V w s ({a} : Set V) p q hpmono hqmono (by simpa using Ne.symm has)
  have hDset : {omega : BondConfig V |
      ∀ x ∈ ({a} : Set V), ¬ (openGraph omega).Reachable s x} = D := by
    ext omega
    simp [D, sourceAvoid]
  rw [hDset] at hBHK
  have hpcluster : ∀ omega : BondConfig V,
      p (openEdgeCluster omega s) =
        projFunA w a F (openCluster omega s) := by
    intro omega
    change projFunA w a F
        (insert s {u | ∃ e ∈ openEdgeCluster omega s, u ∈ e}) =
      projFunA w a F (openCluster omega s)
    rw [← CSH.openCluster_eq_insert_span]
  have hqcluster : ∀ omega : BondConfig V,
      q (openEdgeCluster omega s) =
        sourceKernel w Set.univ O ({a} : Set V) (openCluster omega s) := by
    intro omega
    exact congrArg (sourceKernel w Set.univ O ({a} : Set V))
      (CSH.openCluster_eq_insert_span omega s).symm
  simp_rw [hpcluster] at hBHK
  simp_rw [hqcluster] at hBHK
  have hiw : inducedWeight w (Set.univ : Set V) = w := by
    funext e
    simp [inducedWeight]
  have hguard : guardEv O ({s} : Set V) ({a} : Set V) = J := by
    ext omega
    constructor
    · intro homega
      exact homega.1
    · intro homega
      exact ⟨homega, s, hsO, s, by simp, SimpleGraph.Reachable.refl s⟩
  have htowerP :
      (∫ omega in D,
        projFunA w a F (openCluster omega s) *
          sourceKernel w Set.univ O ({a} : Set V) (openCluster omega s) ∂mu) =
        ∫ omega in J, projFunA w a F (openCluster omega s) ∂mu := by
    have hinside : insert s (O ∪ ({a} : Set V)) ⊆
        (Set.univ : Set V) := Set.subset_univ _
    have htower := KNAll.Guarded.sourceKernel_tower_mul w Set.univ O
      ({a} : Set V) s (projFunA w a F) hinside
    rw [hiw, hguard] at htower
    simpa [D, J, mu] using htower
  have htowerOne :
      (∫ omega in D,
        sourceKernel w Set.univ O ({a} : Set V) (openCluster omega s) ∂mu) =
        mu.real J := by
    have hinside : insert s (O ∪ ({a} : Set V)) ⊆
        (Set.univ : Set V) := Set.subset_univ _
    have htower := KNAll.Guarded.sourceKernel_tower_mul w Set.univ O
      ({a} : Set V) s (fun _ => (1 : ℝ)) hinside
    rw [hiw, hguard] at htower
    simpa [D, J, mu] using htower
  change (∫ omega in D, projFunA w a F (openCluster omega s) ∂mu) *
      (∫ omega in D,
        sourceKernel w Set.univ O ({a} : Set V) (openCluster omega s) ∂mu) ≤
    mu.real D *
      ∫ omega in D, projFunA w a F (openCluster omega s) *
        sourceKernel w Set.univ O ({a} : Set V) (openCluster omega s) ∂mu at hBHK
  rw [htowerOne, htowerP] at hBHK
  have hpint : 0 ≤ ∫ omega in D,
      projFunA w a F (openCluster omega s) ∂mu := by
    have hproj := setIntegral_projFunA_avoid w a s F
    have hsingle : {omega : BondConfig V |
        ∀ y ∈ ({a} : Set V), ¬ (openGraph omega).Reachable s y} = D := by
      ext omega
      simp [D, sourceAvoid]
    rw [hsingle] at hproj
    rw [hproj]
    exact sub_nonneg.2 hmin
  have hJp : 0 ≤ ∫ omega in J,
      projFunA w a F (openCluster omega s) ∂mu := by
    by_cases hD0 : mu.real D = 0
    · have hsub : J ⊆ D := by
        intro omega homega r hr y hy hry
        have hrs : r = s := by simpa using hr
        subst r
        exact homega s hsO y hy hry
      have hreal0 : mu.real J = 0 :=
        le_antisymm ((measureReal_mono hsub).trans hD0.le) measureReal_nonneg
      have hnull : mu J = 0 :=
        (measureReal_eq_zero_iff (measure_ne_top _ _)).1 hreal0
      rw [setIntegral_measure_zero _ hnull]
    · have hDpos : 0 < mu.real D :=
        lt_of_le_of_ne measureReal_nonneg (Ne.symm hD0)
      have hleft : 0 ≤
          (∫ omega in D, projFunA w a F (openCluster omega s) ∂mu) *
            mu.real J := mul_nonneg hpint measureReal_nonneg
      have hprod : 0 ≤ mu.real D *
          ∫ omega in J, projFunA w a F (openCluster omega s) ∂mu :=
        hleft.trans hBHK
      by_contra hneg
      have hmul := mul_neg_of_pos_of_neg hDpos (lt_of_not_ge hneg)
      linarith
  have hmonoInt :
      (∫ omega in J, projFunA w a F (openCluster omega s) ∂mu) ≤
        ∫ omega in J, projFunA w a F (sourceCluster omega O) ∂mu := by
    refine setIntegral_mono_on (Integrable.of_finite).integrableOn
      (Integrable.of_finite).integrableOn MeasurableSet.of_discrete ?_
    intro omega _
    apply monotone_projFunA w a F hF
    intro x hsx
    exact Set.mem_iUnion₂.2 ⟨s, hsO, hsx⟩
  have hsourceProj : 0 ≤ ∫ omega in J,
      projFunA w a F (sourceCluster omega O) ∂mu := hJp.trans hmonoInt
  have hconn : sourceConn O ({s} : Set V) =
      (Set.univ : Set (BondConfig V)) := by
    apply eq_univ_of_forall
    intro omega
    exact ⟨s, hsO, s, by simp, SimpleGraph.Reachable.refl s⟩
  have hproj := setIntegral_sub_eq_projFunA_source_conn
    w O a F ({s} : Finset V)
  have hconn' : sourceConn O (↑({s} : Finset V) : Set V) =
      (Set.univ : Set (BondConfig V)) := by simpa using hconn
  rw [hconn', inter_univ] at hproj
  rw [hproj]
  simpa [J, mu] using hsourceProj


/-- Proof candidate for SourceDefs item 47. -/
theorem source_fixedMin_disjoint {n : ℕ}
    (w : Sym2 (Fin n) → unitInterval) (A S : Finset (Fin n))
    (a : Fin n) (F : Set (Fin n) → ℝ) (ha : a ∈ A)
    (hdis : Disjoint (↑S : Set (Fin n)) (↑A : Set (Fin n)))
    (hF : Monotone F)
    (hmin : ∀ x ∈ A,
      (∫ omega, F (openCluster omega a) ∂(prodBernoulli w)) ≤
        ∫ omega, F (openCluster omega x) ∂(prodBernoulli w)) :
    0 ≤ KNAll.Guarded.sourceFixedMinGap w A S a F := by
  letI : DecidableEq (Fin n) := Classical.decEq _
  set mu := prodBernoulli w with hmu
  have hmeas : ∀ U : Set (BondConfig (Fin n)), MeasurableSet U :=
    fun _ ↦ MeasurableSet.of_discrete
  have hn := fun (U : Set (BondConfig (Fin n))) ↦
    (measureReal_nonneg : 0 ≤ mu.real U)
  have hint : ∀ (g : BondConfig (Fin n) → ℝ) (U : Set (BondConfig (Fin n))),
      IntegrableOn g U mu := fun _ _ ↦ (Integrable.of_finite).integrableOn
  set Phi : Set (Fin n) → ℝ := projFunA w a F with hPhi
  have hPhiMono : Monotone Phi := monotone_projFunA w a F hF
  set T : Finset (Fin n) := (A.erase a).filter (fun x ↦
    0 < mu.real {omega : BondConfig (Fin n) |
      ∀ y ∈ ({a} : Set (Fin n)), ¬ (openGraph omega).Reachable x y}) with hT
  have hTA : ∀ x ∈ T, x ∈ A.erase a :=
    fun x hx ↦ (Finset.mem_filter.1 hx).1
  have hTY : Disjoint (↑T : Set (Fin n)) ({a} : Set (Fin n)) := by
    rw [Set.disjoint_left]
    intro x hxT hxa
    exact Finset.ne_of_mem_erase (hTA x hxT) (mem_singleton_iff.1 hxa)
  have hactRaw : ∀ x ∈ T, 0 < mu.real
      {omega : BondConfig (Fin n) |
        ∀ y ∈ ({a} : Set (Fin n)), ¬ (openGraph omega).Reachable x y} :=
    fun x hx ↦ (Finset.mem_filter.1 hx).2
  have hact : ∀ x ∈ T, 0 < mu.real
      (sourceAvoid ({x} : Set (Fin n)) ({a} : Set (Fin n))) := by
    intro x hx
    have heq : sourceAvoid ({x} : Set (Fin n)) ({a} : Set (Fin n)) =
        {omega : BondConfig (Fin n) |
          ∀ y ∈ ({a} : Set (Fin n)), ¬ (openGraph omega).Reachable x y} := by
      ext omega
      simp [sourceAvoid]
    rw [heq]
    exact hactRaw x hx
  have hmean : ∀ x ∈ T, 0 ≤ condMean w ({a} : Set (Fin n)) Phi x := by
    intro x hx
    unfold condMean
    refine div_nonneg ?_ (hn _)
    rw [hPhi, KNAll.setIntegral_projFunA_avoid w a x F]
    exact sub_nonneg.2 (hmin x (Finset.mem_of_mem_erase (hTA x hx)))
  obtain ⟨r, hr, hcompat⟩ :=
    AGloc.exists_rank_compat T (condMean w ({a} : Set (Fin n)) Phi)
  have hsource : Disjoint (↑S : Set (Fin n))
      (({a} : Set (Fin n)) ∪ (↑T : Set (Fin n))) := by
    apply hdis.mono_right
    intro x hx
    rcases hx with hxa | hxT
    · have hxa' : x = a := by simpa using hxa
      simpa [hxa'] using ha
    · exact Finset.mem_coe.2 (Finset.mem_of_mem_erase (hTA x hxT))
  have hsag := KNAll.Guarded.sourceSurplusY_all_disjoint
    w ({a} : Set (Fin n)) T r (↑S : Set (Fin n)) Phi
    hsource hTY hact hPhiMono hr hcompat
  have hsum0 : 0 ≤ ∑ x ∈ T, mu.real
      (sourceFirstPattern (↑S : Set (Fin n)) ({a} : Set (Fin n)) T r x) *
        condMean w ({a} : Set (Fin n)) Phi x :=
    Finset.sum_nonneg fun x hx ↦ mul_nonneg (hn _) (hmean x hx)
  have hproj : 0 ≤ ∫ omega in
      sourceAvoid (↑S : Set (Fin n)) ({a} : Set (Fin n)) ∩
        sourceConn (↑S : Set (Fin n)) (↑T : Set (Fin n)),
      Phi (sourceCluster omega (↑S : Set (Fin n))) ∂mu := by
    unfold sourceSurplusY at hsag
    linarith
  have hactive : 0 ≤ ∫ omega in
      sourceAvoid (↑S : Set (Fin n)) ({a} : Set (Fin n)) ∩
        sourceConn (↑S : Set (Fin n)) (↑T : Set (Fin n)),
      (F (sourceCluster omega (↑S : Set (Fin n))) -
        F (openCluster omega a)) ∂mu := by
    rw [KNAll.Guarded.setIntegral_sub_eq_projFunA_source_conn
      w (↑S : Set (Fin n)) a F T]
    simpa [hPhi] using hproj
  set E : Set (BondConfig (Fin n)) :=
    sourceAvoid (↑S : Set (Fin n)) ({a} : Set (Fin n)) ∩
      sourceConn (↑S : Set (Fin n)) (↑(A.erase a) : Set (Fin n)) with hE
  set ET : Set (BondConfig (Fin n)) :=
    sourceAvoid (↑S : Set (Fin n)) ({a} : Set (Fin n)) ∩
      sourceConn (↑S : Set (Fin n)) (↑T : Set (Fin n)) with hET
  set g : BondConfig (Fin n) → ℝ := fun omega ↦
    F (sourceCluster omega (↑S : Set (Fin n))) - F (openCluster omega a) with hg
  have hETE : ET ⊆ E := by
    intro omega homega
    refine ⟨homega.1, ?_⟩
    obtain ⟨s, hsS, x, hxT, hsx⟩ := homega.2
    exact ⟨s, hsS, x, Finset.mem_coe.2 (hTA x hxT), hsx⟩
  have hnull : mu (E \ ET) = 0 := by
    have hsub : E \ ET ⊆ ⋃ x ∈ (A.erase a).filter (fun x ↦
        ¬ 0 < mu.real {omega : BondConfig (Fin n) |
          ∀ y ∈ ({a} : Set (Fin n)), ¬ (openGraph omega).Reachable x y}),
        {omega : BondConfig (Fin n) |
          ∀ y ∈ ({a} : Set (Fin n)), ¬ (openGraph omega).Reachable x y} := by
      intro omega homega
      obtain ⟨⟨havoid, hconn⟩, hnot⟩ := homega
      obtain ⟨s, hsS, x, hxA, hsx⟩ := hconn
      have hxT : x ∉ T := fun hxT ↦ hnot
        ⟨havoid, ⟨s, hsS, x, hxT, hsx⟩⟩
      have hinact : ¬ 0 < mu.real {omega : BondConfig (Fin n) |
          ∀ y ∈ ({a} : Set (Fin n)), ¬ (openGraph omega).Reachable x y} :=
        fun hp ↦ hxT (Finset.mem_filter.2 ⟨hxA, hp⟩)
      refine mem_iUnion₂.2 ⟨x, Finset.mem_filter.2 ⟨hxA, hinact⟩, ?_⟩
      intro y hy hxy
      have hya : y = a := by simpa using hy
      subst y
      exact havoid s hsS a (by simp) (hsx.trans hxy)
    refine measure_mono_null hsub
      (measure_biUnion_null_iff (Finset.countable_toSet _) |>.2 fun x hx ↦ ?_)
    have h0 : mu.real {omega : BondConfig (Fin n) |
        ∀ y ∈ ({a} : Set (Fin n)), ¬ (openGraph omega).Reachable x y} = 0 :=
      le_antisymm (not_lt.1 (Finset.mem_filter.1 hx).2) (hn _)
    rwa [Measure.real, ENNReal.toReal_eq_zero_iff,
      or_iff_left (measure_ne_top _ _)] at h0
  have hsplit : ∫ omega in E, g omega ∂mu = ∫ omega in ET, g omega ∂mu := by
    rw [← integral_inter_add_sdiff (hmeas ET) (hint g E),
      inter_eq_right.2 hETE, Measure.restrict_eq_zero.2 hnull,
      integral_zero_measure, add_zero]
  have hEpos : 0 ≤ ∫ omega in E, g omega ∂mu := by
    rw [hsplit]
    exact hactive
  rw [hE, hg, hmu] at hEpos
  simpa only [KNAll.Guarded.sourceFixedMinGap] using hEpos

/-- Proof candidate for SourceDefs item 48. -/
theorem source_fixedMin_of_minimizer_mem {n : ℕ}
    (w : Sym2 (Fin n) → unitInterval) (A S : Finset (Fin n))
    (a : Fin n) (F : Set (Fin n) → ℝ) (haS : a ∈ S) :
    KNAll.Guarded.sourceFixedMinGap w A S a F = 0 := by
  have hzero : sourceAvoid (↑S : Set (Fin n)) ({a} : Set (Fin n)) =
      (∅ : Set (BondConfig (Fin n))) := by
    ext omega
    constructor
    · intro homega
      exact False.elim (homega a (Finset.mem_coe.2 haS) a (by simp)
        (SimpleGraph.Reachable.refl a))
    · simp
  simp [KNAll.Guarded.sourceFixedMinGap, hzero]

/-- Proof candidate for SourceDefs section 3.2. -/
theorem source_fixedMin_empty {n : ℕ}
    (w : Sym2 (Fin n) → unitInterval) (A : Finset (Fin n))
    (a : Fin n) (F : Set (Fin n) → ℝ) :
    KNAll.Guarded.sourceFixedMinGap w A ∅ a F = 0 := by
  have hzero : sourceConn (∅ : Set (Fin n))
      ((↑A : Set (Fin n)) \ {a}) = (∅ : Set (BondConfig (Fin n))) := by
    ext omega
    simp [sourceConn]
  unfold KNAll.Guarded.sourceFixedMinGap
  rw [show (↑(∅ : Finset (Fin n)) : Set (Fin n)) = ∅ by simp]
  rw [show (↑(@Finset.erase (Fin n) (Classical.decEq (Fin n)) A a) : Set (Fin n)) =
      (↑A : Set (Fin n)) \ {a} by ext; simp]
  rw [hzero]
  simp

/-- Proof candidate for SourceDefs item 49. -/
theorem source_fixedMin_overlap {n : ℕ}
    (w : Sym2 (Fin n) → unitInterval) (A S : Finset (Fin n))
    (a : Fin n) (F : Set (Fin n) → ℝ)
    (hover : ∃ s ∈ S, s ∈ A.erase a) (hF : Monotone F)
    (hmin : ∀ x ∈ A,
      (∫ omega, F (openCluster omega a) ∂(prodBernoulli w)) ≤
        ∫ omega, F (openCluster omega x) ∂(prodBernoulli w)) :
    0 ≤ KNAll.Guarded.sourceFixedMinGap w A S a F := by
  obtain ⟨s, hsS, hsA⟩ := hover
  have hsNe : s ≠ a := Finset.ne_of_mem_erase hsA
  have hsMem : s ∈ A := Finset.mem_of_mem_erase hsA
  have hconn : sourceConn (↑S : Set (Fin n))
      ((↑A : Set (Fin n)) \ {a}) =
        (Set.univ : Set (BondConfig (Fin n))) := by
    apply eq_univ_of_forall
    intro omega
    exact ⟨s, Finset.mem_coe.2 hsS, s, ⟨Finset.mem_coe.2 hsMem, by simpa⟩,
      SimpleGraph.Reachable.refl s⟩
  have hoverlap := KNAll.Guarded.source_overlap w (↑S : Set (Fin n))
    s a F (Finset.mem_coe.2 hsS) hF
      (hmin s hsMem)
  unfold KNAll.Guarded.sourceFixedMinGap
  rw [show (↑(@Finset.erase (Fin n) (Classical.decEq (Fin n)) A a) : Set (Fin n)) =
      (↑A : Set (Fin n)) \ {a} by ext; simp]
  rw [hconn, inter_univ]
  exact hoverlap

/-- Proof candidate for SourceDefs item 50. -/
theorem source_fixedMin {n : ℕ}
    (w : Sym2 (Fin n) → unitInterval) (A S : Finset (Fin n))
    (a : Fin n) (F : Set (Fin n) → ℝ) (ha : a ∈ A)
    (hF : Monotone F)
    (hmin : ∀ x ∈ A,
      (∫ omega, F (openCluster omega a) ∂(prodBernoulli w)) ≤
        ∫ omega, F (openCluster omega x) ∂(prodBernoulli w)) :
    0 ≤ KNAll.Guarded.sourceFixedMinGap w A S a F := by
  by_cases hS : S = ∅
  · subst S
    rw [source_fixedMin_empty]
  by_cases haS : a ∈ S
  · rw [source_fixedMin_of_minimizer_mem w A S a F haS]
  by_cases hover : ∃ s ∈ S, s ∈ A.erase a
  · exact source_fixedMin_overlap w A S a F hover hF hmin
  apply source_fixedMin_disjoint w A S a F ha
  · rw [Set.disjoint_left]
    intro x hxS hxA
    have hxS' : x ∈ S := Finset.mem_coe.1 hxS
    have hxA' : x ∈ A := Finset.mem_coe.1 hxA
    by_cases hxa : x = a
    · subst x
      exact haS hxS'
    · exact hover ⟨x, hxS', Finset.mem_erase.2 ⟨hxa, hxA'⟩⟩
  · exact hF
  · exact hmin

end KNAll.Guarded

end

#print axioms KNAll.Guarded.setIntegral_sub_eq_projFunA_source_conn
#print axioms KNAll.Guarded.source_overlap
#print axioms KNAll.Guarded.source_fixedMin